    -- | Free variable check that reduces the subject to make certain variables not
    --   free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.
    module Agda.TypeChecking.Free.Reduce
      ( ForceNotFree
      , forceNotFree
      , IsFree(..)
      ) where

    import Control.Monad.Reader
    import Control.Monad.State

    import qualified Data.IntMap as IntMap
    import Data.IntMap (IntMap)
    import qualified Data.IntSet as IntSet
    import Data.IntSet (IntSet)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Free.Precompute
    import Agda.Utils.Monad

    -- | A variable can either not occur (`NotFree`) or it does occur
    --   (`MaybeFree`).  In the latter case, the occurrence may disappear
    --   depending on the instantiation of some set of metas.
    data IsFree
      = MaybeFree MetaSet
      | NotFree
      deriving (IsFree -> IsFree -> Bool
    (IsFree -> IsFree -> Bool)
    -> (IsFree -> IsFree -> Bool) -> Eq IsFree
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: IsFree -> IsFree -> Bool
    $c/= :: IsFree -> IsFree -> Bool
    == :: IsFree -> IsFree -> Bool
    $c== :: IsFree -> IsFree -> Bool
    Eq, Int -> IsFree -> ShowS
    [IsFree] -> ShowS
    IsFree -> String
    (Int -> IsFree -> ShowS)
    -> (IsFree -> String) -> ([IsFree] -> ShowS) -> Show IsFree
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [IsFree] -> ShowS
    $cshowList :: [IsFree] -> ShowS
    show :: IsFree -> String
    $cshow :: IsFree -> String
    showsPrec :: Int -> IsFree -> ShowS
    $cshowsPrec :: Int -> IsFree -> ShowS
    Show)

    -- | Try to enforce a set of variables not occurring in a given
    --   type. Returns a possibly reduced version of the type and for each
    --   of the given variables whether it is either not free, or
    --   maybe free depending on some metavariables.
    forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m)
                 => IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree :: forall a (m :: * -> *).
    (ForceNotFree a, Reduce a, MonadReduce m) =>
    IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree IntSet
    xs a
    a = do
      -- Initially, all variables are marked as `NotFree`. This is changed
      -- to `MaybeFree` when we find an occurrence.
      let mxs :: IntMap IsFree
    mxs = (Int -> IsFree) -> IntSet -> IntMap IsFree
    forall a. (Int -> a) -> IntSet -> IntMap a
    IntMap.fromSet (IsFree -> Int -> IsFree
    forall a b. a -> b -> a
    const IsFree
    NotFree) IntSet
    xs
      (a
    a, IntMap IsFree
    mxs) <- StateT (IntMap IsFree) m a -> IntMap IsFree -> m (a, IntMap IsFree)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ReaderT MetaSet (StateT (IntMap IsFree) m) a
    -> MetaSet -> StateT (IntMap IsFree) m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (a -> ReaderT MetaSet (StateT (IntMap IsFree) m) a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR (a -> ReaderT MetaSet (StateT (IntMap IsFree) m) a)
    -> a -> ReaderT MetaSet (StateT (IntMap IsFree) m) a
    forall a b. (a -> b) -> a -> b
    $ a -> a
    forall a. PrecomputeFreeVars a => a -> a
    precomputeFreeVars_ a
    a) MetaSet
    forall a. Monoid a => a
    mempty) IntMap IsFree
    mxs
      (IntMap IsFree, a) -> m (IntMap IsFree, a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntMap IsFree
    mxs, a
    a)

    type MonadFreeRed m =
      ( MonadReader MetaSet m
      , MonadState (IntMap IsFree) m
      , MonadReduce m
      )

    class (PrecomputeFreeVars a, Subst a) => ForceNotFree a where
      -- Reduce the argument if necessary, to make as many as possible of
      -- the variables in the state not free. Updates the state, marking
      -- the variables that couldn't be make not free as `MaybeFree`. By
      -- updating the state as soon as a variable can not be reduced away,
      -- we avoid trying to get rid of it in other places.
      forceNotFree' :: (MonadFreeRed m) => a -> m a

    -- Return the set of variables for which there is still hope that they
    -- may not occur.
    varsToForceNotFree :: (MonadFreeRed m) => m IntSet
    varsToForceNotFree :: forall (m :: * -> *). MonadFreeRed m => m IntSet
    varsToForceNotFree = (IntMap IsFree -> IntSet) -> m IntSet
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets (IntMap IsFree -> IntSet
    forall a. IntMap a -> IntSet
    IntMap.keysSet (IntMap IsFree -> IntSet)
    -> (IntMap IsFree -> IntMap IsFree) -> IntMap IsFree -> IntSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((IsFree -> Bool) -> IntMap IsFree -> IntMap IsFree
    forall a. (a -> Bool) -> IntMap a -> IntMap a
    IntMap.filter (IsFree -> IsFree -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFree
    NotFree)))

    -- Reduce the argument if there are offending free variables. Doesn't call the
    -- continuation when no reduction is required.
    reduceIfFreeVars :: (Reduce a, ForceNotFree a, MonadFreeRed m)
                     => (a -> m a) -> a -> m a
    reduceIfFreeVars :: forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    (a -> m a) -> a -> m a
    reduceIfFreeVars a -> m a
    k a
    a = do
      IntSet
    xs <- m IntSet
    forall (m :: * -> *). MonadFreeRed m => m IntSet
    varsToForceNotFree
      let fvs :: IntSet
    fvs     = a -> IntSet
    forall a. PrecomputeFreeVars a => a -> IntSet
    precomputedFreeVars a
    a
          notfree :: Bool
    notfree = IntSet -> IntSet -> Bool
    IntSet.disjoint IntSet
    xs IntSet
    fvs
      if Bool
    notfree
        then a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a
        else a -> m a
    k (a -> m a) -> (a -> a) -> a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> a
    forall a. PrecomputeFreeVars a => a -> a
    precomputeFreeVars_ (a -> m a) -> m a -> m a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< a -> m a
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce a
    a

    -- Careful not to define forceNotFree' = forceNotFreeR since that would loop.
    forceNotFreeR :: (Reduce a, ForceNotFree a, MonadFreeRed m)
                  => a -> m a
    forceNotFreeR :: forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR = (a -> m a) -> a -> m a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    (a -> m a) -> a -> m a
    reduceIfFreeVars a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree'

    instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where
      -- Precomputed free variables are stored in the Arg so reduceIf outside the
      -- traverse.
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Arg a -> m (Arg a)
    forceNotFree' = (Arg a -> m (Arg a)) -> Arg a -> m (Arg a)
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    (a -> m a) -> a -> m a
    reduceIfFreeVars ((a -> m a) -> Arg a -> m (Arg a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree')

    instance (Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) where
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Dom a -> m (Dom a)
    forceNotFree' = (a -> m a) -> Dom a -> m (Dom a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR

    instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where
      -- Reduction stops at abstractions (lambda/pi) so do reduceIf/forceNotFreeR here.
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Abs a -> m (Abs a)
    forceNotFree' a :: Abs a
    a@NoAbs{} = (a -> m a) -> Abs a -> m (Abs a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR Abs a
    a
      forceNotFree' a :: Abs a
    a@Abs{} =
        -- Shift variables up when going under the abstraction and back down when
        -- coming out of it. Since we never add new indices to the state
        -- there's no danger of getting negative indices.
        (Abs a -> m (Abs a)) -> Abs a -> m (Abs a)
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    (a -> m a) -> a -> m a
    reduceIfFreeVars (m () -> (() -> m ()) -> m (Abs a) -> m (Abs a)
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ ((IntMap IsFree -> IntMap IsFree) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((IntMap IsFree -> IntMap IsFree) -> m ())
    -> (IntMap IsFree -> IntMap IsFree) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> IntMap IsFree -> IntMap IsFree
    forall a. (Int -> Int) -> IntMap a -> IntMap a
    IntMap.mapKeys Int -> Int
    forall a. Enum a => a -> a
    succ) (\ ()
    _ -> (IntMap IsFree -> IntMap IsFree) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((IntMap IsFree -> IntMap IsFree) -> m ())
    -> (IntMap IsFree -> IntMap IsFree) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> IntMap IsFree -> IntMap IsFree
    forall a. (Int -> Int) -> IntMap a -> IntMap a
    IntMap.mapKeys Int -> Int
    forall a. Enum a => a -> a
    pred) (m (Abs a) -> m (Abs a))
    -> (Abs a -> m (Abs a)) -> Abs a -> m (Abs a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                          (a -> m a) -> Abs a -> m (Abs a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree') Abs a
    a

    instance ForceNotFree a => ForceNotFree [a] where
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => [a] -> m [a]
    forceNotFree' = (a -> m a) -> [a] -> m [a]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree'

    instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where
      -- There's an Arg inside Elim' which stores precomputed free vars, so let's
      -- not skip over that.
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Elim' a -> m (Elim' a)
    forceNotFree' (Apply Arg a
    arg)    = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a) -> m (Arg a) -> m (Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg a -> m (Arg a)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Arg a
    arg
      forceNotFree' e :: Elim' a
    e@Proj{}       = Elim' a -> m (Elim' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elim' a
    e
      forceNotFree' (IApply a
    x a
    y a
    r) = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply (a -> a -> a -> Elim' a) -> m a -> m (a -> a -> Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR a
    x m (a -> a -> Elim' a) -> m a -> m (a -> Elim' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR a
    y m (a -> Elim' a) -> m a -> m (Elim' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m a
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR a
    r

    instance ForceNotFree Type where
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Type -> m Type
    forceNotFree' (El Sort' Term
    s Term
    t) = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Sort' Term
    s m (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Term
    t

    instance ForceNotFree Term where
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Term -> m Term
    forceNotFree' = \case
        Var Int
    x Elims
    es   -> do
          MetaSet
    metas <- m MetaSet
    forall r (m :: * -> *). MonadReader r m => m r
    ask
          (IntMap IsFree -> IntMap IsFree) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((IntMap IsFree -> IntMap IsFree) -> m ())
    -> (IntMap IsFree -> IntMap IsFree) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (IsFree -> IsFree) -> Int -> IntMap IsFree -> IntMap IsFree
    forall a. (a -> a) -> Int -> IntMap a -> IntMap a
    IntMap.adjust (IsFree -> IsFree -> IsFree
    forall a b. a -> b -> a
    const (IsFree -> IsFree -> IsFree) -> IsFree -> IsFree -> IsFree
    forall a b. (a -> b) -> a -> b
    $ MetaSet -> IsFree
    MaybeFree MetaSet
    metas) Int
    x
          Int -> Elims -> Term
    Var Int
    x (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Elims
    es
        Def QName
    f Elims
    es   -> QName -> Elims -> Term
    Def QName
    f    (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Elims
    es
        Con ConHead
    c ConInfo
    h Elims
    es -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    h  (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Elims
    es
        MetaV MetaId
    x Elims
    es -> (MetaSet -> MetaSet) -> m Term -> m Term
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (MetaId -> MetaSet -> MetaSet
    insertMetaSet MetaId
    x) (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $
                      MetaId -> Elims -> Term
    MetaV MetaId
    x  (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Elims
    es
        Lam ArgInfo
    h Abs Term
    b    -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    h    (Abs Term -> Term) -> m (Abs Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Term -> m (Abs Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Abs Term
    b
        Pi Dom Type
    a Abs Type
    b     -> Dom Type -> Abs Type -> Term
    Pi       (Dom Type -> Abs Type -> Term)
    -> m (Dom Type) -> m (Abs Type -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> m (Dom Type)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Dom Type
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs Type -> m (Abs Type)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Abs Type
    b  -- Dom and Abs do reduceIf so not needed here
        Sort Sort' Term
    s     -> Sort' Term -> Term
    Sort     (Sort' Term -> Term) -> m (Sort' Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Sort' Term
    s
        Level Level
    l    -> Level -> Term
    Level    (Level -> Term) -> m Level -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m Level
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Level
    l
        DontCare Term
    t -> Term -> Term
    DontCare (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    forall a (m :: * -> *).
    (Reduce a, ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFreeR Term
    t  -- Reduction stops at DontCare so reduceIf
        t :: Term
    t@Lit{}    -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t
        t :: Term
    t@Dummy{}  -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t

    instance ForceNotFree Level where
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Level -> m Level
    forceNotFree' (Max Integer
    m [PlusLevel' Term]
    as) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    m ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> m [PlusLevel' Term]
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' [PlusLevel' Term]
    as

    instance ForceNotFree PlusLevel where
      forceNotFree' :: forall (m :: * -> *).
    MonadFreeRed m =>
    PlusLevel' Term -> m (PlusLevel' Term)
    forceNotFree' (Plus Integer
    k Term
    a) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    k (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Term
    a

    instance ForceNotFree Sort where
      -- Reduce for sorts already goes under all sort constructors, so we can get
      -- away without forceNotFreeR here.
      forceNotFree' :: forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    forceNotFree' = \case
        Type Level
    l     -> Level -> Sort' Term
    forall t. Level' t -> Sort' t
    Type     (Level -> Sort' Term) -> m Level -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m Level
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Level
    l
        Prop Level
    l     -> Level -> Sort' Term
    forall t. Level' t -> Sort' t
    Prop     (Level -> Sort' Term) -> m Level -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m Level
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Level
    l
        SSet Level
    l     -> Level -> Sort' Term
    forall t. Level' t -> Sort' t
    SSet     (Level -> Sort' Term) -> m Level -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m Level
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Level
    l
        PiSort Dom' Term Term
    a Sort' Term
    b Abs (Sort' Term)
    c -> Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term)
    -> m (Dom' Term Term)
    -> m (Sort' Term -> Abs (Sort' Term) -> Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Term -> m (Dom' Term Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Dom' Term Term
    a m (Sort' Term -> Abs (Sort' Term) -> Sort' Term)
    -> m (Sort' Term) -> m (Abs (Sort' Term) -> Sort' Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Sort' Term
    b m (Abs (Sort' Term) -> Sort' Term)
    -> m (Abs (Sort' Term)) -> m (Sort' Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs (Sort' Term) -> m (Abs (Sort' Term))
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Abs (Sort' Term)
    c
        FunSort Sort' Term
    a Sort' Term
    b -> Sort' Term -> Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort (Sort' Term -> Sort' Term -> Sort' Term)
    -> m (Sort' Term) -> m (Sort' Term -> Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Sort' Term
    a m (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Sort' Term
    b
        UnivSort Sort' Term
    s -> Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t
    UnivSort (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Sort' Term
    s
        MetaS MetaId
    x Elims
    es -> MetaId -> Elims -> Sort' Term
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x  (Elims -> Sort' Term) -> m Elims -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Elims
    es
        DefS QName
    d Elims
    es  -> QName -> Elims -> Sort' Term
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d   (Elims -> Sort' Term) -> m Elims -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forceNotFree' Elims
    es
        s :: Sort' Term
    s@(Inf IsFibrant
    _ Integer
    _)-> Sort' Term -> m (Sort' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s
        s :: Sort' Term
    s@Sort' Term
    SizeUniv -> Sort' Term -> m (Sort' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s
        s :: Sort' Term
    s@Sort' Term
    LockUniv -> Sort' Term -> m (Sort' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s
        s :: Sort' Term
    s@DummyS{} -> Sort' Term -> m (Sort' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s