    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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
      , reallyFree
      , IsFree(..)
      ) where

    import Prelude hiding (null)

    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
    import Agda.Utils.Null

    -- | 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
    $c== :: IsFree -> IsFree -> Bool
    == :: IsFree -> IsFree -> Bool
    $c/= :: IsFree -> IsFree -> Bool
    /= :: 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
    $cshowsPrec :: Int -> IsFree -> ShowS
    showsPrec :: Int -> IsFree -> ShowS
    $cshow :: IsFree -> String
    show :: IsFree -> String
    $cshowList :: [IsFree] -> ShowS
    showList :: [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, 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
      return (mxs, a)

    -- | Checks if the given term contains any free variables that are in
    --   the given set of variables, possibly reducing the term in the
    --   process.  Returns `Right Nothing` if there are such variables,
    --   `Right (Just v')` if there are none (where v' is the possibly
    --   reduced version of the given term) or `Left b` if the problem is
    --   blocked on a meta.
    reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a)
               => IntSet -> a -> m (Either Blocked_ (Maybe a))
    reallyFree :: forall (m :: * -> *) a.
    (MonadReduce m, Reduce a, ForceNotFree a) =>
    IntSet -> a -> m (Either Blocked_ (Maybe a))
    reallyFree IntSet
    xs a
    v = do
      (mxs , v') <- IntSet -> a -> m (IntMap IsFree, a)
    forall a (m :: * -> *).
    (ForceNotFree a, Reduce a, MonadReduce m) =>
    IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree IntSet
    xs a
    v
      case IntMap.foldr pickFree NotFree mxs of
        MaybeFree MetaSet
    ms
          | MetaSet -> Bool
    forall a. Null a => a -> Bool
    null MetaSet
    ms   -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
    -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocked_ (Maybe a)
    forall a b. b -> Either a b
    Right Maybe a
    forall a. Maybe a
    Nothing
          | Bool
    otherwise -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
    -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Either Blocked_ (Maybe a)
    forall a b. a -> Either a b
    Left (Blocked_ -> Either Blocked_ (Maybe a))
    -> Blocked_ -> Either Blocked_ (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    blocker ()
          where blocker :: Blocker
    blocker = MetaSet -> Blocker
    metaSetToBlocker MetaSet
    ms
        IsFree
    NotFree -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
    -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocked_ (Maybe a)
    forall a b. b -> Either a b
    Right (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    v')

      where
        -- Check if any of the variables occur freely.
        -- Prefer occurrences that do not depend on any metas.
        pickFree :: IsFree -> IsFree -> IsFree
        pickFree :: IsFree -> IsFree -> IsFree
    pickFree f1 :: IsFree
    f1@(MaybeFree MetaSet
    ms1) IsFree
    f2
          | MetaSet -> Bool
    forall a. Null a => a -> Bool
    null MetaSet
    ms1  = IsFree
    f1
        pickFree f1 :: IsFree
    f1@(MaybeFree MetaSet
    ms1) f2 :: IsFree
    f2@(MaybeFree MetaSet
    ms2)
          | MetaSet -> Bool
    forall a. Null a => a -> Bool
    null MetaSet
    ms2  = IsFree
    f2
          | Bool
    otherwise = IsFree
    f1
        pickFree f1 :: IsFree
    f1@(MaybeFree MetaSet
    ms1) IsFree
    NotFree = IsFree
    f1
        pickFree IsFree
    NotFree IsFree
    f2 = IsFree
    f2

    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
      xs <- m IntSet
    forall (m :: * -> *). MonadFreeRed m => m IntSet
    varsToForceNotFree
      let fvs     = a -> IntSet
    forall a. PrecomputeFreeVars a => a -> IntSet
    precomputedFreeVars a
    a
          notfree = IntSet -> IntSet -> Bool
    IntSet.disjoint IntSet
    xs IntSet
    fvs
      if notfree
        then return a
        else k . precomputeFreeVars_ =<< reduce 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
    forall (m :: * -> *). 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forall (m :: * -> *). 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' Term a -> f (Dom' Term 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Abs a -> f (Abs 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Abs a -> f (Abs b)
    traverse a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forall (m :: * -> *). 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse a -> m a
    forall a (m :: * -> *).
    (ForceNotFree a, MonadFreeRed m) =>
    a -> m a
    forall (m :: * -> *). 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
    forall (m :: * -> *). MonadFreeRed m => Arg a -> m (Arg a)
    forceNotFree' Arg a
    arg
      forceNotFree' e :: Elim' a
    e@Proj{}       = Elim' a -> m (Elim' a)
    forall a. a -> m 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 a b. m (a -> b) -> m a -> m b
    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 a b. m (a -> b) -> m a -> m b
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    forceNotFree' Sort' Term
    s m (Term -> Type) -> m Term -> m Type
    forall a b. m (a -> b) -> m a -> m b
    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
    forall (m :: * -> *). MonadFreeRed m => Term -> m Term
    forceNotFree' Term
    t

    instance ForceNotFree Term where
      forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Term -> m Term
    forceNotFree' = \case
        Var Int
    x Elims
    es   -> do
          metas <- m MetaSet
    forall r (m :: * -> *). MonadReader r m => m r
    ask
          modify $ IntMap.adjust (const $ MaybeFree metas) x
          Var x <$> forceNotFree' 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
    forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
    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
    forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
    forceNotFree' Elims
    es
        MetaV MetaId
    x Elims
    es -> (MetaSet -> MetaSet) -> m Term -> m Term
    forall a. (MetaSet -> MetaSet) -> m a -> m a
    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
    forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
    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
    forall (m :: * -> *). MonadFreeRed m => Abs Term -> m (Abs Term)
    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
    forall (m :: * -> *). MonadFreeRed m => Dom Type -> m (Dom Type)
    forceNotFree' Dom Type
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    forall a b. m (a -> b) -> m a -> m b
    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
    forall (m :: * -> *). MonadFreeRed m => Abs Type -> m (Abs Type)
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    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
    forall (m :: * -> *). MonadFreeRed m => Level -> m Level
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t
        t :: Term
    t@Dummy{}  -> Term -> m Term
    forall a. a -> m a
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    [PlusLevel' Term] -> m [PlusLevel' Term]
    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
    forall (m :: * -> *). MonadFreeRed m => Term -> m Term
    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
        Univ Univ
    u Level
    l     -> Univ -> Level -> Sort' Term
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (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
    forall (m :: * -> *). MonadFreeRed m => Level -> m Level
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Dom' Term Term -> m (Dom' Term Term)
    forceNotFree' Dom' Term Term
    a m (Sort' Term -> Abs (Sort' Term) -> Sort' Term)
    -> m (Sort' Term) -> m (Abs (Sort' Term) -> Sort' Term)
    forall a b. m (a -> b) -> m a -> m b
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    forceNotFree' Sort' Term
    b m (Abs (Sort' Term) -> Sort' Term)
    -> m (Abs (Sort' Term)) -> m (Sort' Term)
    forall a b. m (a -> b) -> m a -> m b
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Abs (Sort' Term) -> m (Abs (Sort' Term))
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    forceNotFree' Sort' Term
    a m (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
    forall a b. m (a -> b) -> m a -> m b
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    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
    forall (m :: * -> *).
    MonadFreeRed m =>
    Sort' Term -> m (Sort' Term)
    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
    forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
    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
    forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
    forceNotFree' Elims
    es
        s :: Sort' Term
    s@(Inf Univ
    _ Integer
    _)-> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s
        s :: Sort' Term
    s@Sort' Term
    LevelUniv -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s
        s :: Sort' Term
    s@Sort' Term
    IntervalUniv -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s
        s :: Sort' Term
    s@DummyS{} -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    s