    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Precompute free variables in a term (and store in 'ArgInfo').
    module Agda.TypeChecking.Free.Precompute
      ( PrecomputeFreeVars, precomputeFreeVars
      , precomputedFreeVars, precomputeFreeVars_ ) where

    import Control.Monad.Writer ( Writer, runWriter, censor, listen, tell )

    import Agda.Utils.VarSet (VarSet)
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    type FV = Writer VarSet

    precomputeFreeVars_ :: PrecomputeFreeVars a => a -> a
    precomputeFreeVars_ :: forall a. PrecomputeFreeVars a => a -> a
    precomputeFreeVars_ = (a, VarSet) -> a
    forall a b. (a, b) -> a
    fst ((a, VarSet) -> a) -> (a -> (a, VarSet)) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Writer VarSet a -> (a, VarSet)
    forall w a. Writer w a -> (a, w)
    runWriter (Writer VarSet a -> (a, VarSet))
    -> (a -> Writer VarSet a) -> a -> (a, VarSet)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Writer VarSet a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars

    precomputedFreeVars :: PrecomputeFreeVars a => a -> VarSet
    precomputedFreeVars :: forall a. PrecomputeFreeVars a => a -> VarSet
    precomputedFreeVars = (a, VarSet) -> VarSet
    forall a b. (a, b) -> b
    snd ((a, VarSet) -> VarSet) -> (a -> (a, VarSet)) -> a -> VarSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Writer VarSet a -> (a, VarSet)
    forall w a. Writer w a -> (a, w)
    runWriter (Writer VarSet a -> (a, VarSet))
    -> (a -> Writer VarSet a) -> a -> (a, VarSet)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Writer VarSet a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars

    class PrecomputeFreeVars a where
      precomputeFreeVars :: a -> FV a

      default precomputeFreeVars :: (Traversable c, PrecomputeFreeVars x, a ~ c x) => a -> FV a
      precomputeFreeVars = (x -> WriterT VarSet Identity x)
    -> c x -> WriterT VarSet Identity (c x)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> c a -> f (c b)
    traverse x -> WriterT VarSet Identity x
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars

    -- The instances where things actually happen: Arg, Abs and Term.

    maybePrecomputed :: PrecomputeFreeVars a => ArgInfo -> a -> FV (ArgInfo, a)
    maybePrecomputed :: forall a. PrecomputeFreeVars a => ArgInfo -> a -> FV (ArgInfo, a)
    maybePrecomputed ArgInfo
    i a
    x =
      case ArgInfo -> FreeVariables
    forall a. LensFreeVariables a => a -> FreeVariables
    getFreeVariables ArgInfo
    i of
        KnownFVs VarSet
    fv -> (ArgInfo
    i, a
    x) (ArgInfo, a) -> WriterT VarSet Identity () -> FV (ArgInfo, a)
    forall a b.
    a -> WriterT VarSet Identity b -> WriterT VarSet Identity a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ VarSet -> WriterT VarSet Identity ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell VarSet
    fv
        FreeVariables
    UnknownFVs -> do
          (x', fv) <- WriterT VarSet Identity a -> WriterT VarSet Identity (a, VarSet)
    forall a.
    WriterT VarSet Identity a -> WriterT VarSet Identity (a, VarSet)
    forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
    listen (WriterT VarSet Identity a -> WriterT VarSet Identity (a, VarSet))
    -> WriterT VarSet Identity a -> WriterT VarSet Identity (a, VarSet)
    forall a b. (a -> b) -> a -> b
    $ a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    x
          return (setFreeVariables (KnownFVs fv) i, x')

    instance PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) where
      precomputeFreeVars :: Arg a -> FV (Arg a)
    precomputeFreeVars arg :: Arg a
    arg@(Arg ArgInfo
    i a
    x) = (ArgInfo -> a -> Arg a) -> (ArgInfo, a) -> Arg a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg ((ArgInfo, a) -> Arg a)
    -> WriterT VarSet Identity (ArgInfo, a) -> FV (Arg a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgInfo -> a -> WriterT VarSet Identity (ArgInfo, a)
    forall a. PrecomputeFreeVars a => ArgInfo -> a -> FV (ArgInfo, a)
    maybePrecomputed ArgInfo
    i a
    x

    -- Note that we don't store free variables in the Dom. The reason is that the
    -- ArgInfo in the Dom tends to get reused during type checking for the argument
    -- of that domain type, and it would be tedious and error prone to ensure that
    -- we don't accidentally inherit also the free variables. Moreover we don't
    -- really need the free variables of the Dom.
    instance PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) where

    instance PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) where
      precomputeFreeVars :: Abs a -> FV (Abs a)
    precomputeFreeVars (NoAbs ArgName
    x a
    b) = ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    x (a -> Abs a) -> WriterT VarSet Identity a -> FV (Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    b
      precomputeFreeVars (Abs ArgName
    x a
    b) =
        (VarSet -> VarSet) -> FV (Abs a) -> FV (Abs a)
    forall w (m :: * -> *) a. MonadWriter w m => (w -> w) -> m a -> m a
    censor (Int -> VarSet -> VarSet
    VarSet.subtract Int
    1 (VarSet -> VarSet) -> (VarSet -> VarSet) -> VarSet -> VarSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> VarSet -> VarSet
    VarSet.delete Int
    0) (FV (Abs a) -> FV (Abs a)) -> FV (Abs a) -> FV (Abs a)
    forall a b. (a -> b) -> a -> b
    $
          ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x (a -> Abs a) -> WriterT VarSet Identity a -> FV (Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    b

    instance PrecomputeFreeVars Term where
      precomputeFreeVars :: Term -> FV Term
    precomputeFreeVars Term
    t =
        case Term
    t of
          Var Int
    x Elims
    es -> do
            VarSet -> WriterT VarSet Identity ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Int -> VarSet
    VarSet.singleton Int
    x)
            Int -> Elims -> Term
    Var Int
    x (Elims -> Term) -> WriterT VarSet Identity Elims -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> WriterT VarSet Identity Elims
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Elims
    es
          Lam ArgInfo
    i Abs Term
    b    -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i      (Abs Term -> Term) -> WriterT VarSet Identity (Abs Term) -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Term -> WriterT VarSet Identity (Abs Term)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Abs Term
    b
          Lit{}      -> Term -> FV Term
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    t
          Def QName
    f Elims
    es   -> QName -> Elims -> Term
    Def QName
    f      (Elims -> Term) -> WriterT VarSet Identity Elims -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> WriterT VarSet Identity Elims
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Elims
    es
          Con ConHead
    c ConInfo
    i Elims
    es -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    i    (Elims -> Term) -> WriterT VarSet Identity Elims -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> WriterT VarSet Identity Elims
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Elims
    es
          Pi Dom Type
    a Abs Type
    b     -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> Term
    Pi ((Dom Type, Abs Type) -> Term)
    -> WriterT VarSet Identity (Dom Type, Abs Type) -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Dom Type, Abs Type)
    -> WriterT VarSet Identity (Dom Type, Abs Type)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars (Dom Type
    a, Abs Type
    b)
          Sort Sort
    s     -> Sort -> Term
    Sort       (Sort -> Term) -> WriterT VarSet Identity Sort -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> WriterT VarSet Identity Sort
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Sort
    s
          Level Level
    l    -> Level -> Term
    Level      (Level -> Term) -> WriterT VarSet Identity Level -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> WriterT VarSet Identity Level
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Level
    l
          MetaV MetaId
    x Elims
    es -> MetaId -> Elims -> Term
    MetaV MetaId
    x    (Elims -> Term) -> WriterT VarSet Identity Elims -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> WriterT VarSet Identity Elims
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Elims
    es
          DontCare Term
    t -> Term -> Term
    DontCare   (Term -> Term) -> FV Term -> FV Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> FV Term
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Term
    t
          Dummy{}    -> Term -> FV Term
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    t

    -- The other instances are boilerplate.

    instance PrecomputeFreeVars Sort where
      precomputeFreeVars :: Sort -> WriterT VarSet Identity Sort
    precomputeFreeVars Sort
    s =
        case Sort
    s of
          Univ Univ
    u Level
    a   -> Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (Level -> Sort)
    -> WriterT VarSet Identity Level -> WriterT VarSet Identity Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> WriterT VarSet Identity Level
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Level
    a
          Inf Univ
    _ Integer
    _    -> Sort -> WriterT VarSet Identity Sort
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
          Sort
    SizeUniv   -> Sort -> WriterT VarSet Identity Sort
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
          Sort
    LockUniv   -> Sort -> WriterT VarSet Identity Sort
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
          Sort
    LevelUniv  -> Sort -> WriterT VarSet Identity Sort
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
          Sort
    IntervalUniv -> Sort -> WriterT VarSet Identity Sort
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort (Dom' Term Term -> Sort -> Abs Sort -> Sort)
    -> WriterT VarSet Identity (Dom' Term Term)
    -> WriterT VarSet Identity (Sort -> Abs Sort -> Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Term -> WriterT VarSet Identity (Dom' Term Term)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Dom' Term Term
    a WriterT VarSet Identity (Sort -> Abs Sort -> Sort)
    -> WriterT VarSet Identity Sort
    -> WriterT VarSet Identity (Abs Sort -> Sort)
    forall a b.
    WriterT VarSet Identity (a -> b)
    -> WriterT VarSet Identity a -> WriterT VarSet Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> WriterT VarSet Identity Sort
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Sort
    s1 WriterT VarSet Identity (Abs Sort -> Sort)
    -> WriterT VarSet Identity (Abs Sort)
    -> WriterT VarSet Identity Sort
    forall a b.
    WriterT VarSet Identity (a -> b)
    -> WriterT VarSet Identity a -> WriterT VarSet Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs Sort -> WriterT VarSet Identity (Abs Sort)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Abs Sort
    s2
          FunSort Sort
    s1 Sort
    s2 -> (Sort -> Sort -> Sort) -> (Sort, Sort) -> Sort
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort ((Sort, Sort) -> Sort)
    -> WriterT VarSet Identity (Sort, Sort)
    -> WriterT VarSet Identity Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Sort, Sort) -> WriterT VarSet Identity (Sort, Sort)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars (Sort
    s1, Sort
    s2)
          UnivSort Sort
    s -> Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort (Sort -> Sort)
    -> WriterT VarSet Identity Sort -> WriterT VarSet Identity Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> WriterT VarSet Identity Sort
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Sort
    s
          MetaS MetaId
    x Elims
    es -> MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x (Elims -> Sort)
    -> WriterT VarSet Identity Elims -> WriterT VarSet Identity Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> WriterT VarSet Identity Elims
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Elims
    es
          DefS QName
    d Elims
    es  -> QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d (Elims -> Sort)
    -> WriterT VarSet Identity Elims -> WriterT VarSet Identity Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> WriterT VarSet Identity Elims
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Elims
    es
          DummyS{}   -> Sort -> WriterT VarSet Identity Sort
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s

    instance PrecomputeFreeVars Level where
      precomputeFreeVars :: Level -> WriterT VarSet Identity Level
    precomputeFreeVars (Max Integer
    n [PlusLevel' Term]
    ls) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' Term] -> Level)
    -> WriterT VarSet Identity [PlusLevel' Term]
    -> WriterT VarSet Identity Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> WriterT VarSet Identity [PlusLevel' Term]
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars [PlusLevel' Term]
    ls

    instance PrecomputeFreeVars PlusLevel where
      precomputeFreeVars :: PlusLevel' Term -> FV (PlusLevel' Term)
    precomputeFreeVars (Plus Integer
    n Term
    l) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel' Term) -> FV Term -> FV (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> FV Term
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Term
    l

    instance PrecomputeFreeVars Type where
      precomputeFreeVars :: Type -> FV Type
    precomputeFreeVars (El Sort
    s Term
    t) = (Sort -> Term -> Type) -> (Sort, Term) -> Type
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El ((Sort, Term) -> Type)
    -> WriterT VarSet Identity (Sort, Term) -> FV Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Sort, Term) -> WriterT VarSet Identity (Sort, Term)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars (Sort
    s, Term
    t)

    -- Note: don't use default instance, since that bypasses the 'Arg' in 'Apply'.
    instance PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) where
      precomputeFreeVars :: Elim' a -> FV (Elim' a)
    precomputeFreeVars Elim' a
    e =
        case Elim' a
    e of
          Apply Arg a
    x      -> Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a)
    -> WriterT VarSet Identity (Arg a) -> FV (Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg a -> WriterT VarSet Identity (Arg a)
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars Arg a
    x
          IApply a
    a a
    x a
    y -> a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply (a -> a -> a -> Elim' a)
    -> WriterT VarSet Identity a
    -> WriterT VarSet Identity (a -> a -> Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    a WriterT VarSet Identity (a -> a -> Elim' a)
    -> WriterT VarSet Identity a
    -> WriterT VarSet Identity (a -> Elim' a)
    forall a b.
    WriterT VarSet Identity (a -> b)
    -> WriterT VarSet Identity a -> WriterT VarSet Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    x WriterT VarSet Identity (a -> Elim' a)
    -> WriterT VarSet Identity a -> FV (Elim' a)
    forall a b.
    WriterT VarSet Identity (a -> b)
    -> WriterT VarSet Identity a -> WriterT VarSet Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    y
          Proj{}       -> Elim' a -> FV (Elim' a)
    forall a. a -> WriterT VarSet Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Elim' a
    e

    -- The very boilerplate instances

    instance PrecomputeFreeVars a => PrecomputeFreeVars [a] where
    instance PrecomputeFreeVars a => PrecomputeFreeVars (Maybe a) where

    instance (PrecomputeFreeVars a, PrecomputeFreeVars b) => PrecomputeFreeVars (a, b) where
      precomputeFreeVars :: (a, b) -> FV (a, b)
    precomputeFreeVars (a
    x, b
    y) = (,) (a -> b -> (a, b))
    -> WriterT VarSet Identity a
    -> WriterT VarSet Identity (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> WriterT VarSet Identity a
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars a
    x WriterT VarSet Identity (b -> (a, b))
    -> WriterT VarSet Identity b -> FV (a, b)
    forall a b.
    WriterT VarSet Identity (a -> b)
    -> WriterT VarSet Identity a -> WriterT VarSet Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> WriterT VarSet Identity b
    forall a. PrecomputeFreeVars a => a -> FV a
    precomputeFreeVars b
    y