    -- | Computing the free variables of a term lazily.
    --
    -- We implement a reduce (traversal into monoid) over internal syntax
    -- for a generic collection (monoid with singletons).  This should allow
    -- a more efficient test for the presence of a particular variable.
    --
    -- Worst-case complexity does not change (i.e. the case when a variable
    -- does not occur), but best case-complexity does matter.  For instance,
    -- see 'Agda.TypeChecking.Substitute.mkAbs': each time we construct
    -- a dependent function type, we check whether it is actually dependent.
    --
    -- The distinction between rigid and strongly rigid occurrences comes from:
    --   Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)
    --
    -- The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly
    -- in t.  It might have a solution if the occurrence is not strongly rigid, e.g.
    --
    --   x = \f -> suc (f (x (\ y -> k)))  has  x = \f -> suc (f (suc k))
    --
    -- [Jason C. Reed, PhD thesis, page 106]
    --
    -- Under coinductive constructors, occurrences are never strongly rigid.
    -- Also, function types and lambdas do not establish strong rigidity.
    -- Only inductive constructors do so.
    -- (See issue 1271).
    --
    -- For further reading on semirings and semimodules for variable occurrence,
    -- see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016).
    -- There, he treats the "quantity" dimension of variable occurrences.
    --
    -- The semiring has an additive operation for combining occurrences of subterms,
    -- and a multiplicative operation of representing function composition.  E.g.
    -- if variable @x@ appears @o@ in term @u@, but @u@ appears in context @q@ in
    -- term @t@ then occurrence of variable @x@ coming from @u@ is accounted for
    -- as @q o@ in @t@.
    --
    -- Consider example @(λ{ x → (x,x)}) y@:
    --
    --   * Variable @x@ occurs once unguarded in @x@.
    --
    --   * It occurs twice unguarded in the aggregation @x@ @x@
    --
    --   * Inductive constructor @,@ turns this into two strictly rigid occurrences.
    --
    --     If @,@ is a record constructor, then we stay unguarded.
    --
    --   * The function @({λ x → (x,x)})@ provides a context for variable @y@.
    --     This context can be described as weakly rigid with quantity two.
    --
    --   * The final occurrence of @y@ is obtained as composing the context with
    --     the occurrence of @y@ in itself (which is the unit for composition).
    --     Thus, @y@ occurs weakly rigid with quantity two.
    --
    -- It is not a given that the context can be described in the same way
    -- as the variable occurrence.  However, for quantity it is the case
    -- and we obtain a semiring of occurrences with 0, 1, and even ω, which
    -- is an absorptive element for addition.

    module Agda.TypeChecking.Free.Lazy where

    import Control.Applicative hiding (empty)
    import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, Reader, runReader )

    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.HashSet (HashSet)
    import qualified Data.HashSet as HashSet
    import Data.Set (Set)
    import qualified Data.Set as Set

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

    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List1 (List1)
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Semigroup
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    ---------------------------------------------------------------------------
    -- * Set of meta variables.

    -- | A set of meta variables.  Forms a monoid under union.

    newtype MetaSet = MetaSet { MetaSet -> HashSet MetaId
    theMetaSet :: HashSet MetaId }
      deriving (MetaSet -> MetaSet -> Bool
    (MetaSet -> MetaSet -> Bool)
    -> (MetaSet -> MetaSet -> Bool) -> Eq MetaSet
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: MetaSet -> MetaSet -> Bool
    == :: MetaSet -> MetaSet -> Bool
    $c/= :: MetaSet -> MetaSet -> Bool
    /= :: MetaSet -> MetaSet -> Bool
    Eq, Variable -> MetaSet -> ShowS
    [MetaSet] -> ShowS
    MetaSet -> String
    (Variable -> MetaSet -> ShowS)
    -> (MetaSet -> String) -> ([MetaSet] -> ShowS) -> Show MetaSet
    forall a.
    (Variable -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Variable -> MetaSet -> ShowS
    showsPrec :: Variable -> MetaSet -> ShowS
    $cshow :: MetaSet -> String
    show :: MetaSet -> String
    $cshowList :: [MetaSet] -> ShowS
    showList :: [MetaSet] -> ShowS
    Show, MetaSet
    MetaSet -> Bool
    MetaSet -> (MetaSet -> Bool) -> Null MetaSet
    forall a. a -> (a -> Bool) -> Null a
    $cempty :: MetaSet
    empty :: MetaSet
    $cnull :: MetaSet -> Bool
    null :: MetaSet -> Bool
    Null, NonEmpty MetaSet -> MetaSet
    MetaSet -> MetaSet -> MetaSet
    (MetaSet -> MetaSet -> MetaSet)
    -> (NonEmpty MetaSet -> MetaSet)
    -> (forall b. Integral b => b -> MetaSet -> MetaSet)
    -> Semigroup MetaSet
    forall b. Integral b => b -> MetaSet -> MetaSet
    forall a.
    (a -> a -> a)
    -> (NonEmpty a -> a)
    -> (forall b. Integral b => b -> a -> a)
    -> Semigroup a
    $c<> :: MetaSet -> MetaSet -> MetaSet
    <> :: MetaSet -> MetaSet -> MetaSet
    $csconcat :: NonEmpty MetaSet -> MetaSet
    sconcat :: NonEmpty MetaSet -> MetaSet
    $cstimes :: forall b. Integral b => b -> MetaSet -> MetaSet
    stimes :: forall b. Integral b => b -> MetaSet -> MetaSet
    Semigroup, Semigroup MetaSet
    MetaSet
    Semigroup MetaSet =>
    MetaSet
    -> (MetaSet -> MetaSet -> MetaSet)
    -> ([MetaSet] -> MetaSet)
    -> Monoid MetaSet
    [MetaSet] -> MetaSet
    MetaSet -> MetaSet -> MetaSet
    forall a.
    Semigroup a =>
    a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
    $cmempty :: MetaSet
    mempty :: MetaSet
    $cmappend :: MetaSet -> MetaSet -> MetaSet
    mappend :: MetaSet -> MetaSet -> MetaSet
    $cmconcat :: [MetaSet] -> MetaSet
    mconcat :: [MetaSet] -> MetaSet
    Monoid)

    instance Singleton MetaId MetaSet where
      singleton :: MetaId -> MetaSet
    singleton = HashSet MetaId -> MetaSet
    MetaSet (HashSet MetaId -> MetaSet)
    -> (MetaId -> HashSet MetaId) -> MetaId -> MetaSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> HashSet MetaId
    forall el coll. Singleton el coll => el -> coll
    singleton

    insertMetaSet :: MetaId -> MetaSet -> MetaSet
    insertMetaSet :: MetaId -> MetaSet -> MetaSet
    insertMetaSet MetaId
    m (MetaSet HashSet MetaId
    ms) = HashSet MetaId -> MetaSet
    MetaSet (HashSet MetaId -> MetaSet) -> HashSet MetaId -> MetaSet
    forall a b. (a -> b) -> a -> b
    $ MetaId -> HashSet MetaId -> HashSet MetaId
    forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
    HashSet.insert MetaId
    m HashSet MetaId
    ms

    foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
    foldrMetaSet :: forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
    foldrMetaSet MetaId -> a -> a
    f a
    e MetaSet
    ms = (MetaId -> a -> a) -> a -> HashSet MetaId -> a
    forall b a. (b -> a -> a) -> a -> HashSet b -> a
    HashSet.foldr MetaId -> a -> a
    f a
    e (HashSet MetaId -> a) -> HashSet MetaId -> a
    forall a b. (a -> b) -> a -> b
    $ MetaSet -> HashSet MetaId
    theMetaSet MetaSet
    ms

    metaSetToBlocker :: MetaSet -> Blocker
    metaSetToBlocker :: MetaSet -> Blocker
    metaSetToBlocker MetaSet
    ms = Set Blocker -> Blocker
    unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set Blocker -> Set Blocker)
    -> Set Blocker -> MetaSet -> Set Blocker
    forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
    foldrMetaSet (Blocker -> Set Blocker -> Set Blocker
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (Blocker -> Set Blocker -> Set Blocker)
    -> (MetaId -> Blocker) -> MetaId -> Set Blocker -> Set Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Blocker
    unblockOnMeta) Set Blocker
    forall a. Set a
    Set.empty MetaSet
    ms

    ---------------------------------------------------------------------------
    -- * Flexible and rigid occurrences (semigroup)

    -- | Depending on the surrounding context of a variable,
    --   it's occurrence can be classified as flexible or rigid,
    --   with finer distinctions.
    --
    --   The constructors are listed in increasing order (wrt. information content).
    data FlexRig' a
      = Flexible a        -- ^ In arguments of metas.
                          --   The set of metas is used by ''Agda.TypeChecking.Rewriting.NonLinMatch''
                          --   to generate the right blocking information.
                          --   The semantics is that the status of a variable occurrence may change
                          --   if one of the metas in the set gets solved.  We may say the occurrence
                          --   is tainted by the meta variables in the set.
      | WeaklyRigid       -- ^ In arguments to variables and definitions.
      | Unguarded         -- ^ In top position, or only under inductive record constructors (unit).
      | StronglyRigid     -- ^ Under at least one and only inductive constructors.
      deriving (FlexRig' a -> FlexRig' a -> Bool
    (FlexRig' a -> FlexRig' a -> Bool)
    -> (FlexRig' a -> FlexRig' a -> Bool) -> Eq (FlexRig' a)
    forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
    == :: FlexRig' a -> FlexRig' a -> Bool
    $c/= :: forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
    /= :: FlexRig' a -> FlexRig' a -> Bool
    Eq, Variable -> FlexRig' a -> ShowS
    [FlexRig' a] -> ShowS
    FlexRig' a -> String
    (Variable -> FlexRig' a -> ShowS)
    -> (FlexRig' a -> String)
    -> ([FlexRig' a] -> ShowS)
    -> Show (FlexRig' a)
    forall a. Show a => Variable -> FlexRig' a -> ShowS
    forall a. Show a => [FlexRig' a] -> ShowS
    forall a. Show a => FlexRig' a -> String
    forall a.
    (Variable -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Variable -> FlexRig' a -> ShowS
    showsPrec :: Variable -> FlexRig' a -> ShowS
    $cshow :: forall a. Show a => FlexRig' a -> String
    show :: FlexRig' a -> String
    $cshowList :: forall a. Show a => [FlexRig' a] -> ShowS
    showList :: [FlexRig' a] -> ShowS
    Show, (forall a b. (a -> b) -> FlexRig' a -> FlexRig' b)
    -> (forall a b. a -> FlexRig' b -> FlexRig' a) -> Functor FlexRig'
    forall a b. a -> FlexRig' b -> FlexRig' a
    forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
    fmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
    $c<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
    <$ :: forall a b. a -> FlexRig' b -> FlexRig' a
    Functor, (forall m. Monoid m => FlexRig' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> FlexRig' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> FlexRig' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> FlexRig' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> FlexRig' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FlexRig' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FlexRig' a -> b)
    -> (forall a. (a -> a -> a) -> FlexRig' a -> a)
    -> (forall a. (a -> a -> a) -> FlexRig' a -> a)
    -> (forall a. FlexRig' a -> [a])
    -> (forall a. FlexRig' a -> Bool)
    -> (forall a. FlexRig' a -> Variable)
    -> (forall a. Eq a => a -> FlexRig' a -> Bool)
    -> (forall a. Ord a => FlexRig' a -> a)
    -> (forall a. Ord a => FlexRig' a -> a)
    -> (forall a. Num a => FlexRig' a -> a)
    -> (forall a. Num a => FlexRig' a -> a)
    -> Foldable FlexRig'
    forall a. Eq a => a -> FlexRig' a -> Bool
    forall a. Num a => FlexRig' a -> a
    forall a. Ord a => FlexRig' a -> a
    forall m. Monoid m => FlexRig' m -> m
    forall a. FlexRig' a -> Bool
    forall a. FlexRig' a -> Variable
    forall a. FlexRig' a -> [a]
    forall a. (a -> a -> a) -> FlexRig' a -> a
    forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
    forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
    forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Variable)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => FlexRig' m -> m
    fold :: forall m. Monoid m => FlexRig' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    foldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    foldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    $ctoList :: forall a. FlexRig' a -> [a]
    toList :: forall a. FlexRig' a -> [a]
    $cnull :: forall a. FlexRig' a -> Bool
    null :: forall a. FlexRig' a -> Bool
    $clength :: forall a. FlexRig' a -> Variable
    length :: forall a. FlexRig' a -> Variable
    $celem :: forall a. Eq a => a -> FlexRig' a -> Bool
    elem :: forall a. Eq a => a -> FlexRig' a -> Bool
    $cmaximum :: forall a. Ord a => FlexRig' a -> a
    maximum :: forall a. Ord a => FlexRig' a -> a
    $cminimum :: forall a. Ord a => FlexRig' a -> a
    minimum :: forall a. Ord a => FlexRig' a -> a
    $csum :: forall a. Num a => FlexRig' a -> a
    sum :: forall a. Num a => FlexRig' a -> a
    $cproduct :: forall a. Num a => FlexRig' a -> a
    product :: forall a. Num a => FlexRig' a -> a
    Foldable)

    type FlexRig = FlexRig' MetaSet

    class LensFlexRig o a | o -> a where
      lensFlexRig :: Lens' o (FlexRig' a)

    instance LensFlexRig (FlexRig' a) a where
      lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)
    lensFlexRig = (FlexRig' a -> f (FlexRig' a)) -> FlexRig' a -> f (FlexRig' a)
    forall a. a -> a
    id

    isFlexible :: LensFlexRig o a => o -> Bool
    isFlexible :: forall o a. LensFlexRig o a => o -> Bool
    isFlexible o
    o = case o
    o o -> Lens' o (FlexRig' a) -> FlexRig' a
    forall o i. o -> Lens' o i -> i
    ^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' o (FlexRig' a)
    lensFlexRig of
      Flexible {} -> Bool
    True
      FlexRig' a
    _ -> Bool
    False

    isUnguarded :: LensFlexRig o a => o -> Bool
    isUnguarded :: forall o a. LensFlexRig o a => o -> Bool
    isUnguarded o
    o = case o
    o o -> Lens' o (FlexRig' a) -> FlexRig' a
    forall o i. o -> Lens' o i -> i
    ^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' o (FlexRig' a)
    lensFlexRig of
      FlexRig' a
    Unguarded -> Bool
    True
      FlexRig' a
    _ -> Bool
    False

    isWeaklyRigid :: LensFlexRig o a => o -> Bool
    isWeaklyRigid :: forall o a. LensFlexRig o a => o -> Bool
    isWeaklyRigid o
    o = case o
    o o -> Lens' o (FlexRig' a) -> FlexRig' a
    forall o i. o -> Lens' o i -> i
    ^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' o (FlexRig' a)
    lensFlexRig of
       FlexRig' a
    WeaklyRigid -> Bool
    True
       FlexRig' a
    _ -> Bool
    False

    isStronglyRigid :: LensFlexRig o a => o -> Bool
    isStronglyRigid :: forall o a. LensFlexRig o a => o -> Bool
    isStronglyRigid o
    o = case o
    o o -> Lens' o (FlexRig' a) -> FlexRig' a
    forall o i. o -> Lens' o i -> i
    ^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' o (FlexRig' a)
    lensFlexRig of
      FlexRig' a
    StronglyRigid -> Bool
    True
      FlexRig' a
    _ -> Bool
    False

    -- | 'FlexRig' aggregation (additive operation of the semiring).
    --   For combining occurrences of the same variable in subterms.
    --   This is a refinement of the 'max' operation for 'FlexRig'
    --   which would work if 'Flexible' did not have the 'MetaSet' as an argument.
    --   Now, to aggregate two 'Flexible' occurrences, we union the involved 'MetaSet's.

    addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    addFlexRig :: forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    addFlexRig = ((FlexRig' a, FlexRig' a) -> FlexRig' a)
    -> FlexRig' a -> FlexRig' a -> FlexRig' a
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((FlexRig' a, FlexRig' a) -> FlexRig' a)
     -> FlexRig' a -> FlexRig' a -> FlexRig' a)
    -> ((FlexRig' a, FlexRig' a) -> FlexRig' a)
    -> FlexRig' a
    -> FlexRig' a
    -> FlexRig' a
    forall a b. (a -> b) -> a -> b
    $ \case
      -- StronglyRigid is dominant
      (FlexRig' a
    StronglyRigid, FlexRig' a
    _) -> FlexRig' a
    forall a. FlexRig' a
    StronglyRigid
      (FlexRig' a
    _, FlexRig' a
    StronglyRigid) -> FlexRig' a
    forall a. FlexRig' a
    StronglyRigid
      -- Next is Unguarded
      (FlexRig' a
    Unguarded, FlexRig' a
    _) -> FlexRig' a
    forall a. FlexRig' a
    Unguarded
      (FlexRig' a
    _, FlexRig' a
    Unguarded) -> FlexRig' a
    forall a. FlexRig' a
    Unguarded
      -- Then WeaklyRigid
      (FlexRig' a
    WeaklyRigid, FlexRig' a
    _) -> FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
      (FlexRig' a
    _, FlexRig' a
    WeaklyRigid) -> FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
      -- Least is Flexible.  We union the meta sets, as the variable
      -- is tainted by all of the involved meta variable.
      (Flexible a
    ms1, Flexible a
    ms2) -> a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible (a -> FlexRig' a) -> a -> FlexRig' a
    forall a b. (a -> b) -> a -> b
    $ a
    ms1 a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    ms2

    -- | Unit for 'addFlexRig'.
    zeroFlexRig :: Monoid a => FlexRig' a
    zeroFlexRig :: forall a. Monoid a => FlexRig' a
    zeroFlexRig = a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible a
    forall a. Monoid a => a
    mempty

    -- | Absorptive for 'addFlexRig'.
    omegaFlexRig :: FlexRig' a
    omegaFlexRig :: forall a. FlexRig' a
    omegaFlexRig = FlexRig' a
    forall a. FlexRig' a
    StronglyRigid

    -- | 'FlexRig' composition (multiplicative operation of the semiring).
    --   For accumulating the context of a variable.
    --
    --   'Flexible' is dominant.  Once we are under a meta, we are flexible
    --   regardless what else comes.  We taint all variable occurrences
    --   under a meta by this meta.
    --
    --   'WeaklyRigid' is next in strength.  Destroys strong rigidity.
    --
    --   'StronglyRigid' is still dominant over 'Unguarded'.
    --
    --   'Unguarded' is the unit.  It is the top (identity) context.
    --
    composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    composeFlexRig :: forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    composeFlexRig = ((FlexRig' a, FlexRig' a) -> FlexRig' a)
    -> FlexRig' a -> FlexRig' a -> FlexRig' a
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((FlexRig' a, FlexRig' a) -> FlexRig' a)
     -> FlexRig' a -> FlexRig' a -> FlexRig' a)
    -> ((FlexRig' a, FlexRig' a) -> FlexRig' a)
    -> FlexRig' a
    -> FlexRig' a
    -> FlexRig' a
    forall a b. (a -> b) -> a -> b
    $ \case
        (Flexible a
    ms1, Flexible a
    ms2) -> a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible (a -> FlexRig' a) -> a -> FlexRig' a
    forall a b. (a -> b) -> a -> b
    $ a
    ms1 a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    ms2
        (Flexible a
    ms1, FlexRig' a
    _) -> a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible a
    ms1
        (FlexRig' a
    _, Flexible a
    ms2) -> a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible a
    ms2
        (FlexRig' a
    WeaklyRigid, FlexRig' a
    _) -> FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
        (FlexRig' a
    _, FlexRig' a
    WeaklyRigid) -> FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
        (FlexRig' a
    StronglyRigid, FlexRig' a
    _) -> FlexRig' a
    forall a. FlexRig' a
    StronglyRigid
        (FlexRig' a
    _, FlexRig' a
    StronglyRigid) -> FlexRig' a
    forall a. FlexRig' a
    StronglyRigid
        (FlexRig' a
    Unguarded, FlexRig' a
    Unguarded) -> FlexRig' a
    forall a. FlexRig' a
    Unguarded

    -- | Unit for 'composeFlexRig'.
    oneFlexRig :: FlexRig' a
    oneFlexRig :: forall a. FlexRig' a
    oneFlexRig = FlexRig' a
    forall a. FlexRig' a
    Unguarded

    ---------------------------------------------------------------------------
    -- * Multi-dimensional feature vector for variable occurrence (semigroup)

    -- | Occurrence of free variables is classified by several dimensions.
    --   Currently, we have 'FlexRig' and 'Modality'.
    data VarOcc' a = VarOcc
      { forall a. VarOcc' a -> FlexRig' a
    varFlexRig   :: FlexRig' a
      , forall a. VarOcc' a -> Modality
    varModality  :: Modality
      }
      deriving (Variable -> VarOcc' a -> ShowS
    [VarOcc' a] -> ShowS
    VarOcc' a -> String
    (Variable -> VarOcc' a -> ShowS)
    -> (VarOcc' a -> String)
    -> ([VarOcc' a] -> ShowS)
    -> Show (VarOcc' a)
    forall a. Show a => Variable -> VarOcc' a -> ShowS
    forall a. Show a => [VarOcc' a] -> ShowS
    forall a. Show a => VarOcc' a -> String
    forall a.
    (Variable -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Variable -> VarOcc' a -> ShowS
    showsPrec :: Variable -> VarOcc' a -> ShowS
    $cshow :: forall a. Show a => VarOcc' a -> String
    show :: VarOcc' a -> String
    $cshowList :: forall a. Show a => [VarOcc' a] -> ShowS
    showList :: [VarOcc' a] -> ShowS
    Show)
    type VarOcc = VarOcc' MetaSet

    -- | Equality up to origin.
    instance Eq a => Eq (VarOcc' a) where
      VarOcc FlexRig' a
    fr Modality
    m == :: VarOcc' a -> VarOcc' a -> Bool
    == VarOcc FlexRig' a
    fr' Modality
    m' = FlexRig' a
    fr FlexRig' a -> FlexRig' a -> Bool
    forall a. Eq a => a -> a -> Bool
    == FlexRig' a
    fr' Bool -> Bool -> Bool
    && Modality -> Modality -> Bool
    forall a b. (LensModality a, LensModality b) => a -> b -> Bool
    sameModality Modality
    m Modality
    m'

    instance LensModality (VarOcc' a) where
      getModality :: VarOcc' a -> Modality
    getModality = VarOcc' a -> Modality
    forall a. VarOcc' a -> Modality
    varModality
      mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a
    mapModality Modality -> Modality
    f (VarOcc FlexRig' a
    x Modality
    r) = FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc FlexRig' a
    x (Modality -> VarOcc' a) -> Modality -> VarOcc' a
    forall a b. (a -> b) -> a -> b
    $ Modality -> Modality
    f Modality
    r

    instance LensRelevance (VarOcc' a) where
    instance LensQuantity (VarOcc' a) where

    -- | Access to 'varFlexRig' in 'VarOcc'.
    instance LensFlexRig (VarOcc' a) a where
      lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)
    lensFlexRig FlexRig' a -> f (FlexRig' a)
    f (VarOcc FlexRig' a
    fr Modality
    m) = FlexRig' a -> f (FlexRig' a)
    f FlexRig' a
    fr f (FlexRig' a) -> (FlexRig' a -> VarOcc' a) -> f (VarOcc' a)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ FlexRig' a
    fr' -> FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc FlexRig' a
    fr' Modality
    m
    -- lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)
    -- lensFlexRig f (VarOcc fr m) = f fr <&> \ fr' -> VarOcc fr' m

    -- | The default way of aggregating free variable info from subterms is by adding
    --   the variable occurrences.  For instance, if we have a pair @(t₁,t₂)@ then
    --   and @t₁@ has @o₁@ the occurrences of a variable @x@
    --   and @t₂@ has @o₂@ the occurrences of the same variable, then
    --   @(t₁,t₂)@ has @mappend o₁ o₂@ occurrences of that variable.
    --
    --   From counting 'Quantity', we extrapolate this to 'FlexRig' and 'Relevance':
    --   we care most about about 'StronglyRigid' 'Relevant' occurrences.
    --   E.g., if @t₁@ has a 'StronglyRigid' occurrence and @t₂@ a 'Flexible' occurrence,
    --   then @(t₁,t₂)@ still has a 'StronglyRigid' occurrence.
    --   Analogously, @Relevant@ occurrences count most, as we wish e.g. to forbid
    --   relevant occurrences of variables that are declared to be irrelevant.
    --
    --   'VarOcc' forms a semiring, and this monoid is the addition of the semiring.

    instance Semigroup a => Semigroup (VarOcc' a) where
      VarOcc FlexRig' a
    o Modality
    m <> :: VarOcc' a -> VarOcc' a -> VarOcc' a
    <> VarOcc FlexRig' a
    o' Modality
    m' = FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc (FlexRig' a -> FlexRig' a -> FlexRig' a
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    addFlexRig FlexRig' a
    o FlexRig' a
    o') (Modality -> Modality -> Modality
    addModality Modality
    m Modality
    m')

    -- | The neutral element for variable occurrence aggregation is least serious
    --   occurrence: flexible, irrelevant.
    --   This is also the absorptive element for 'composeVarOcc', if we ignore
    --   the 'MetaSet' in 'Flexible'.
    instance (Semigroup a, Monoid a) => Monoid (VarOcc' a) where
      mempty :: VarOcc' a
    mempty  = FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc (a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible a
    forall a. Monoid a => a
    mempty) Modality
    zeroModality
      mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a
    mappend = VarOcc' a -> VarOcc' a -> VarOcc' a
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | The absorptive element of variable occurrence under aggregation:
    --   strongly rigid, relevant.
    topVarOcc :: VarOcc' a
    topVarOcc :: forall a. VarOcc' a
    topVarOcc = FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc FlexRig' a
    forall a. FlexRig' a
    StronglyRigid Modality
    topModality

    -- | First argument is the outer occurrence (context) and second is the inner.
    --   This multiplicative operation is to modify an occurrence under a context.
    composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
    composeVarOcc :: forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
    composeVarOcc (VarOcc FlexRig' a
    o Modality
    m) (VarOcc FlexRig' a
    o' Modality
    m') = FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc (FlexRig' a -> FlexRig' a -> FlexRig' a
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    composeFlexRig FlexRig' a
    o FlexRig' a
    o') (Modality -> Modality -> Modality
    composeModality Modality
    m Modality
    m')
      -- We use the multipicative modality monoid (composition).

    oneVarOcc :: VarOcc' a
    oneVarOcc :: forall a. VarOcc' a
    oneVarOcc = FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc FlexRig' a
    forall a. FlexRig' a
    Unguarded Modality
    unitModality

    ---------------------------------------------------------------------------
    -- * Storing variable occurrences (semimodule).

    -- | Any representation @c@ of a set of variables need to be able to be modified by
    --   a variable occurrence. This is to ensure that free variable analysis is
    --   compositional. For instance, it should be possible to compute `fv (v [u/x])`
    --   from `fv v` and `fv u`.
    --
    --   In algebraic terminology, a variable set @a@ needs to be (almost) a left semimodule
    --   to the semiring 'VarOcc'.
    class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where
      -- | Laws
      --    * Respects monoid operations:
      --      ```
      --        withVarOcc o mempty   == mempty
      --        withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y
      --      ```
      --    * Respects VarOcc composition:
      --      ```
      --        withVarOcc oneVarOcc             = id
      --        withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2
      --      ```
      --    * Respects VarOcc aggregation:
      --      ```
      --        withVarOcc (o1 <> o2) x = withVarOcc o1 x <> withVarOcc o2 x
      --      ```
      --      Since the corresponding unit law may fail,
      --      ```
      --        withVarOcc mempty x = mempty
      --      ```
      --      it is not quite a semimodule.
      withVarOcc :: VarOcc' a -> c -> c

    -- | Representation of a variable set as map from de Bruijn indices
    --   to 'VarOcc'.
    type TheVarMap' a = IntMap (VarOcc' a)
    newtype VarMap' a = VarMap { forall a. VarMap' a -> TheVarMap' a
    theVarMap :: TheVarMap' a }
      deriving (VarMap' a -> VarMap' a -> Bool
    (VarMap' a -> VarMap' a -> Bool)
    -> (VarMap' a -> VarMap' a -> Bool) -> Eq (VarMap' a)
    forall a. Eq a => VarMap' a -> VarMap' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => VarMap' a -> VarMap' a -> Bool
    == :: VarMap' a -> VarMap' a -> Bool
    $c/= :: forall a. Eq a => VarMap' a -> VarMap' a -> Bool
    /= :: VarMap' a -> VarMap' a -> Bool
    Eq, Variable -> VarMap' a -> ShowS
    [VarMap' a] -> ShowS
    VarMap' a -> String
    (Variable -> VarMap' a -> ShowS)
    -> (VarMap' a -> String)
    -> ([VarMap' a] -> ShowS)
    -> Show (VarMap' a)
    forall a. Show a => Variable -> VarMap' a -> ShowS
    forall a. Show a => [VarMap' a] -> ShowS
    forall a. Show a => VarMap' a -> String
    forall a.
    (Variable -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Variable -> VarMap' a -> ShowS
    showsPrec :: Variable -> VarMap' a -> ShowS
    $cshow :: forall a. Show a => VarMap' a -> String
    show :: VarMap' a -> String
    $cshowList :: forall a. Show a => [VarMap' a] -> ShowS
    showList :: [VarMap' a] -> ShowS
    Show)

    type TheVarMap = TheVarMap' MetaSet
    type    VarMap =    VarMap' MetaSet

    -- | A "set"-style 'Singleton' instance with default/initial variable occurrence.
    instance Singleton Variable (VarMap' a) where
      singleton :: Variable -> VarMap' a
    singleton Variable
    i = TheVarMap' a -> VarMap' a
    forall a. TheVarMap' a -> VarMap' a
    VarMap (TheVarMap' a -> VarMap' a) -> TheVarMap' a -> VarMap' a
    forall a b. (a -> b) -> a -> b
    $ Variable -> VarOcc' a -> TheVarMap' a
    forall a. Variable -> a -> IntMap a
    IntMap.singleton Variable
    i VarOcc' a
    forall a. VarOcc' a
    oneVarOcc

    mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
    mapVarMap :: forall a b.
    (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
    mapVarMap TheVarMap' a -> TheVarMap' b
    f = TheVarMap' b -> VarMap' b
    forall a. TheVarMap' a -> VarMap' a
    VarMap (TheVarMap' b -> VarMap' b)
    -> (VarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TheVarMap' a -> TheVarMap' b
    f (TheVarMap' a -> TheVarMap' b)
    -> (VarMap' a -> TheVarMap' a) -> VarMap' a -> TheVarMap' b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VarMap' a -> TheVarMap' a
    forall a. VarMap' a -> TheVarMap' a
    theVarMap

    lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
    lookupVarMap :: forall a. Variable -> VarMap' a -> Maybe (VarOcc' a)
    lookupVarMap Variable
    i = Variable -> IntMap (VarOcc' a) -> Maybe (VarOcc' a)
    forall a. Variable -> IntMap a -> Maybe a
    IntMap.lookup Variable
    i (IntMap (VarOcc' a) -> Maybe (VarOcc' a))
    -> (VarMap' a -> IntMap (VarOcc' a))
    -> VarMap' a
    -> Maybe (VarOcc' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VarMap' a -> IntMap (VarOcc' a)
    forall a. VarMap' a -> TheVarMap' a
    theVarMap

    -- Andreas & Jesper, 2018-05-11, issue #3052:

    -- | Proper monoid instance for @VarMap@ rather than inheriting the broken one from IntMap.
    --   We combine two occurrences of a variable using 'mappend'.
    instance Semigroup a => Semigroup (VarMap' a) where
      VarMap TheVarMap' a
    m <> :: VarMap' a -> VarMap' a -> VarMap' a
    <> VarMap TheVarMap' a
    m' = TheVarMap' a -> VarMap' a
    forall a. TheVarMap' a -> VarMap' a
    VarMap (TheVarMap' a -> VarMap' a) -> TheVarMap' a -> VarMap' a
    forall a b. (a -> b) -> a -> b
    $ (VarOcc' a -> VarOcc' a -> VarOcc' a)
    -> TheVarMap' a -> TheVarMap' a -> TheVarMap' a
    forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
    IntMap.unionWith VarOcc' a -> VarOcc' a -> VarOcc' a
    forall a. Semigroup a => a -> a -> a
    (<>) TheVarMap' a
    m TheVarMap' a
    m'

    instance Semigroup a => Monoid (VarMap' a) where
      mempty :: VarMap' a
    mempty  = TheVarMap' a -> VarMap' a
    forall a. TheVarMap' a -> VarMap' a
    VarMap TheVarMap' a
    forall a. IntMap a
    IntMap.empty
      mappend :: VarMap' a -> VarMap' a -> VarMap' a
    mappend = VarMap' a -> VarMap' a -> VarMap' a
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [VarMap' a] -> VarMap' a
    mconcat = TheVarMap' a -> VarMap' a
    forall a. TheVarMap' a -> VarMap' a
    VarMap (TheVarMap' a -> VarMap' a)
    -> ([VarMap' a] -> TheVarMap' a) -> [VarMap' a] -> VarMap' a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (VarOcc' a -> VarOcc' a -> VarOcc' a)
    -> [TheVarMap' a] -> TheVarMap' a
    forall (f :: * -> *) a.
    Foldable f =>
    (a -> a -> a) -> f (IntMap a) -> IntMap a
    IntMap.unionsWith VarOcc' a -> VarOcc' a -> VarOcc' a
    forall a. Semigroup a => a -> a -> a
    (<>) ([TheVarMap' a] -> TheVarMap' a)
    -> ([VarMap' a] -> [TheVarMap' a]) -> [VarMap' a] -> TheVarMap' a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (VarMap' a -> TheVarMap' a) -> [VarMap' a] -> [TheVarMap' a]
    forall a b. (a -> b) -> [a] -> [b]
    map VarMap' a -> TheVarMap' a
    forall a. VarMap' a -> TheVarMap' a
    theVarMap
      -- mconcat = VarMap . IntMap.unionsWith mappend . coerce   -- ghc 8.6.5 does not seem to like this coerce

    instance (Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) where
      withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a
    withVarOcc VarOcc' a
    o = (TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a
    forall a b.
    (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
    mapVarMap ((TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a)
    -> (TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a
    forall a b. (a -> b) -> a -> b
    $ (VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a
    forall a b. (a -> b) -> IntMap a -> IntMap b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a)
    -> (VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a
    forall a b. (a -> b) -> a -> b
    $ VarOcc' a -> VarOcc' a -> VarOcc' a
    forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
    composeVarOcc VarOcc' a
    o

    ---------------------------------------------------------------------------
    -- * Simple flexible/rigid variable collection.

    -- | Keep track of 'FlexRig' for every variable, but forget the involved meta vars.
    type TheFlexRigMap = IntMap (FlexRig' ())
    newtype FlexRigMap = FlexRigMap { FlexRigMap -> TheFlexRigMap
    theFlexRigMap :: TheFlexRigMap }
      deriving (Variable -> FlexRigMap -> ShowS
    [FlexRigMap] -> ShowS
    FlexRigMap -> String
    (Variable -> FlexRigMap -> ShowS)
    -> (FlexRigMap -> String)
    -> ([FlexRigMap] -> ShowS)
    -> Show FlexRigMap
    forall a.
    (Variable -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Variable -> FlexRigMap -> ShowS
    showsPrec :: Variable -> FlexRigMap -> ShowS
    $cshow :: FlexRigMap -> String
    show :: FlexRigMap -> String
    $cshowList :: [FlexRigMap] -> ShowS
    showList :: [FlexRigMap] -> ShowS
    Show, Singleton (Variable, FlexRig' ()))

    mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
    mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
    mapFlexRigMap TheFlexRigMap -> TheFlexRigMap
    f = TheFlexRigMap -> FlexRigMap
    FlexRigMap (TheFlexRigMap -> FlexRigMap)
    -> (FlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TheFlexRigMap -> TheFlexRigMap
    f (TheFlexRigMap -> TheFlexRigMap)
    -> (FlexRigMap -> TheFlexRigMap) -> FlexRigMap -> TheFlexRigMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FlexRigMap -> TheFlexRigMap
    theFlexRigMap

    instance Semigroup FlexRigMap where
      FlexRigMap TheFlexRigMap
    m <> :: FlexRigMap -> FlexRigMap -> FlexRigMap
    <> FlexRigMap TheFlexRigMap
    m' = TheFlexRigMap -> FlexRigMap
    FlexRigMap (TheFlexRigMap -> FlexRigMap) -> TheFlexRigMap -> FlexRigMap
    forall a b. (a -> b) -> a -> b
    $ (FlexRig' () -> FlexRig' () -> FlexRig' ())
    -> TheFlexRigMap -> TheFlexRigMap -> TheFlexRigMap
    forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
    IntMap.unionWith FlexRig' () -> FlexRig' () -> FlexRig' ()
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    addFlexRig TheFlexRigMap
    m TheFlexRigMap
    m'

    instance Monoid FlexRigMap where
      mempty :: FlexRigMap
    mempty  = TheFlexRigMap -> FlexRigMap
    FlexRigMap TheFlexRigMap
    forall a. IntMap a
    IntMap.empty
      mappend :: FlexRigMap -> FlexRigMap -> FlexRigMap
    mappend = FlexRigMap -> FlexRigMap -> FlexRigMap
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [FlexRigMap] -> FlexRigMap
    mconcat = TheFlexRigMap -> FlexRigMap
    FlexRigMap (TheFlexRigMap -> FlexRigMap)
    -> ([FlexRigMap] -> TheFlexRigMap) -> [FlexRigMap] -> FlexRigMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (FlexRig' () -> FlexRig' () -> FlexRig' ())
    -> [TheFlexRigMap] -> TheFlexRigMap
    forall (f :: * -> *) a.
    Foldable f =>
    (a -> a -> a) -> f (IntMap a) -> IntMap a
    IntMap.unionsWith FlexRig' () -> FlexRig' () -> FlexRig' ()
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    addFlexRig ([TheFlexRigMap] -> TheFlexRigMap)
    -> ([FlexRigMap] -> [TheFlexRigMap])
    -> [FlexRigMap]
    -> TheFlexRigMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (FlexRigMap -> TheFlexRigMap) -> [FlexRigMap] -> [TheFlexRigMap]
    forall a b. (a -> b) -> [a] -> [b]
    map FlexRigMap -> TheFlexRigMap
    theFlexRigMap

    -- | Compose everything with the 'varFlexRig' part of the 'VarOcc'.
    instance IsVarSet () FlexRigMap where
      withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap
    withVarOcc VarOcc' ()
    o = (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
    mapFlexRigMap ((TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap)
    -> (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
    forall a b. (a -> b) -> a -> b
    $ (FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap
    forall a b. (a -> b) -> IntMap a -> IntMap b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap)
    -> (FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap
    forall a b. (a -> b) -> a -> b
    $ FlexRig' () -> FlexRig' () -> FlexRig' ()
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    composeFlexRig (FlexRig' () -> FlexRig' () -> FlexRig' ())
    -> FlexRig' () -> FlexRig' () -> FlexRig' ()
    forall a b. (a -> b) -> a -> b
    $ () () -> FlexRig' () -> FlexRig' ()
    forall a b. a -> FlexRig' b -> FlexRig' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ VarOcc' () -> FlexRig' ()
    forall a. VarOcc' a -> FlexRig' a
    varFlexRig VarOcc' ()
    o

    instance Singleton MetaId () where
      singleton :: MetaId -> ()
    singleton MetaId
    _ = ()

    ---------------------------------------------------------------------------
    -- * Environment for collecting free variables.

    -- | Where should we skip sorts in free variable analysis?

    data IgnoreSorts
      = IgnoreNot            -- ^ Do not skip.
      | IgnoreInAnnotations  -- ^ Skip when annotation to a type.
      | IgnoreAll            -- ^ Skip unconditionally.
      deriving (IgnoreSorts -> IgnoreSorts -> Bool
    (IgnoreSorts -> IgnoreSorts -> Bool)
    -> (IgnoreSorts -> IgnoreSorts -> Bool) -> Eq IgnoreSorts
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: IgnoreSorts -> IgnoreSorts -> Bool
    == :: IgnoreSorts -> IgnoreSorts -> Bool
    $c/= :: IgnoreSorts -> IgnoreSorts -> Bool
    /= :: IgnoreSorts -> IgnoreSorts -> Bool
    Eq, Variable -> IgnoreSorts -> ShowS
    [IgnoreSorts] -> ShowS
    IgnoreSorts -> String
    (Variable -> IgnoreSorts -> ShowS)
    -> (IgnoreSorts -> String)
    -> ([IgnoreSorts] -> ShowS)
    -> Show IgnoreSorts
    forall a.
    (Variable -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Variable -> IgnoreSorts -> ShowS
    showsPrec :: Variable -> IgnoreSorts -> ShowS
    $cshow :: IgnoreSorts -> String
    show :: IgnoreSorts -> String
    $cshowList :: [IgnoreSorts] -> ShowS
    showList :: [IgnoreSorts] -> ShowS
    Show)

    -- | The current context.

    data FreeEnv' a b c = FreeEnv
      { forall a b c. FreeEnv' a b c -> b
    feExtra     :: !b
        -- ^ Additional context, e.g., whether to ignore free variables in sorts.
      , forall a b c. FreeEnv' a b c -> FlexRig' a
    feFlexRig   :: !(FlexRig' a)
        -- ^ Are we flexible or rigid?
      , forall a b c. FreeEnv' a b c -> Modality
    feModality  :: !Modality
        -- ^ What is the current relevance and quantity?
      , forall a b c. FreeEnv' a b c -> Maybe Variable -> c
    feSingleton :: Maybe Variable -> c
        -- ^ Method to return a single variable.
      }

    type Variable    = Int
    type SingleVar c = Variable -> c

    type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c

    -- | Ignore free variables in sorts.
    feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts
    feIgnoreSorts :: forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
    feIgnoreSorts = FreeEnv' a IgnoreSorts c -> IgnoreSorts
    forall a b c. FreeEnv' a b c -> b
    feExtra

    instance LensFlexRig (FreeEnv' a b c) a where
      lensFlexRig :: Lens' (FreeEnv' a b c) (FlexRig' a)
    lensFlexRig FlexRig' a -> f (FlexRig' a)
    f FreeEnv' a b c
    e = FlexRig' a -> f (FlexRig' a)
    f (FreeEnv' a b c -> FlexRig' a
    forall a b c. FreeEnv' a b c -> FlexRig' a
    feFlexRig FreeEnv' a b c
    e) f (FlexRig' a)
    -> (FlexRig' a -> FreeEnv' a b c) -> f (FreeEnv' a b c)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ FlexRig' a
    fr -> FreeEnv' a b c
    e { feFlexRig = fr }

    instance LensModality (FreeEnv' a b c) where
      getModality :: FreeEnv' a b c -> Modality
    getModality = FreeEnv' a b c -> Modality
    forall a b c. FreeEnv' a b c -> Modality
    feModality
      mapModality :: (Modality -> Modality) -> FreeEnv' a b c -> FreeEnv' a b c
    mapModality Modality -> Modality
    f FreeEnv' a b c
    e = FreeEnv' a b c
    e { feModality = f (feModality e) }

    instance LensRelevance (FreeEnv' a b c) where
    instance LensQuantity (FreeEnv' a b c) where

    -- | The initial context.

    initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c
    initFreeEnv :: forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
    initFreeEnv b
    e SingleVar c
    sing = FreeEnv
      { feExtra :: b
    feExtra       = b
    e
      , feFlexRig :: FlexRig' a
    feFlexRig     = FlexRig' a
    forall a. FlexRig' a
    Unguarded
      , feModality :: Modality
    feModality    = Modality
    unitModality      -- multiplicative monoid
      , feSingleton :: Maybe Variable -> c
    feSingleton   = c -> SingleVar c -> Maybe Variable -> c
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe c
    forall a. Monoid a => a
    mempty SingleVar c
    sing
      }

    type FreeT a b m c = ReaderT (FreeEnv' a b c) m c
    type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c

    -- | Run function for FreeM.
    runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c
    runFreeM :: forall a c.
    IsVarSet a c =>
    SingleVar c -> IgnoreSorts -> FreeM a c -> c
    runFreeM SingleVar c
    single IgnoreSorts
    i FreeM a c
    m = FreeM a c -> FreeEnv' a IgnoreSorts c -> c
    forall r a. Reader r a -> r -> a
    runReader FreeM a c
    m (FreeEnv' a IgnoreSorts c -> c) -> FreeEnv' a IgnoreSorts c -> c
    forall a b. (a -> b) -> a -> b
    $ IgnoreSorts -> SingleVar c -> FreeEnv' a IgnoreSorts c
    forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
    initFreeEnv IgnoreSorts
    i SingleVar c
    single

    instance (Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c) where
      mempty :: FreeT a b m c
    mempty  = c -> FreeT a b m c
    forall a. a -> ReaderT (FreeEnv' a b c) m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure c
    forall a. Monoid a => a
    mempty
      mappend :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c
    mappend = FreeT a b m c -> FreeT a b m c -> FreeT a b m c
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [FreeT a b m c] -> FreeT a b m c
    mconcat = [c] -> c
    forall a. Monoid a => [a] -> a
    mconcat ([c] -> c)
    -> ([FreeT a b m c] -> ReaderT (FreeEnv' a b c) m [c])
    -> [FreeT a b m c]
    -> FreeT a b m c
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> [FreeT a b m c] -> ReaderT (FreeEnv' a b c) m [c]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence

    -- | Base case: a variable.
    variable :: (Monad m, IsVarSet a c) => Int -> FreeT a b m c
    variable :: forall (m :: * -> *) a c b.
    (Monad m, IsVarSet a c) =>
    Variable -> FreeT a b m c
    variable Variable
    n = do
      o <- (FreeEnv' a b c -> FlexRig' a)
    -> ReaderT (FreeEnv' a b c) m (FlexRig' a)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks FreeEnv' a b c -> FlexRig' a
    forall a b c. FreeEnv' a b c -> FlexRig' a
    feFlexRig
      r <- asks feModality
      s <- asks feSingleton
      return $ withVarOcc (VarOcc o r) (s $ Just n)

    -- | Subtract, but return Nothing if result is negative.
    subVar :: Int -> Maybe Variable -> Maybe Variable
    -- subVar n x = x >>= \ i -> (i - n) <$ guard (n <= i)
    subVar :: Variable -> Maybe Variable -> Maybe Variable
    subVar Variable
    n Maybe Variable
    x = do
      i <- Maybe Variable
    x
      guard $ i >= n
      return $ i - n

    -- | Going under a binder.
    underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z
    underBinder :: forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    m z -> m z
    underBinder = Variable -> m z -> m z
    forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    Variable -> m z -> m z
    underBinder' Variable
    1

    -- | Going under @n@ binders.
    underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z
    underBinder' :: forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    Variable -> m z -> m z
    underBinder' Variable
    n = (FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z
    forall a. (FreeEnv' a b c -> FreeEnv' a b c) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z)
    -> (FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z
    forall a b. (a -> b) -> a -> b
    $ \ FreeEnv' a b c
    e -> FreeEnv' a b c
    e { feSingleton = feSingleton e . subVar n }

    -- | Changing the 'Modality'.
    underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z
    underModality :: forall r (m :: * -> *) o z.
    (MonadReader r m, LensModality r, LensModality o) =>
    o -> m z -> m z
    underModality = (r -> r) -> m z -> m z
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Modality -> Modality) -> r -> r
    forall a. LensModality a => (Modality -> Modality) -> a -> a
    mapModality ((Modality -> Modality) -> r -> r)
    -> (o -> Modality -> Modality) -> o -> r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Modality -> Modality -> Modality
    composeModality (Modality -> Modality -> Modality)
    -> (o -> Modality) -> o -> Modality -> Modality
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . o -> Modality
    forall a. LensModality a => a -> Modality
    getModality

    -- | Changing the 'Relevance'.
    underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z
    underRelevance :: forall r (m :: * -> *) o z.
    (MonadReader r m, LensRelevance r, LensRelevance o) =>
    o -> m z -> m z
    underRelevance = (r -> r) -> m z -> m z
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Relevance -> Relevance) -> r -> r
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance ((Relevance -> Relevance) -> r -> r)
    -> (o -> Relevance -> Relevance) -> o -> r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Relevance -> Relevance -> Relevance
    composeRelevance (Relevance -> Relevance -> Relevance)
    -> (o -> Relevance) -> o -> Relevance -> Relevance
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . o -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance

    -- | In the given computation the 'Quantity' is locally scaled using
    -- the 'Quantity' of the first argument.
    underQuantity ::
      (MonadReader r m, LensQuantity r, LensQuantity o) => o -> m a -> m a
    underQuantity :: forall r (m :: * -> *) o a.
    (MonadReader r m, LensQuantity r, LensQuantity o) =>
    o -> m a -> m a
    underQuantity = (r -> r) -> m a -> m a
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((r -> r) -> m a -> m a) -> (o -> r -> r) -> o -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantity -> Quantity) -> r -> r
    forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
    mapQuantity ((Quantity -> Quantity) -> r -> r)
    -> (o -> Quantity -> Quantity) -> o -> r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> Quantity -> Quantity
    composeQuantity (Quantity -> Quantity -> Quantity)
    -> (o -> Quantity) -> o -> Quantity -> Quantity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . o -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity

    -- | Changing the 'FlexRig' context.
    underFlexRig :: (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) => o -> m z -> m z
    underFlexRig :: forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig = (r -> r) -> m z -> m z
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' r (FlexRig' a) -> LensMap r (FlexRig' a)
    forall o i. Lens' o i -> LensMap o i
    over (FlexRig' a -> f (FlexRig' a)) -> r -> f r
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' r (FlexRig' a)
    lensFlexRig LensMap r (FlexRig' a)
    -> (o -> FlexRig' a -> FlexRig' a) -> o -> r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FlexRig' a -> FlexRig' a -> FlexRig' a
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    composeFlexRig (FlexRig' a -> FlexRig' a -> FlexRig' a)
    -> (o -> FlexRig' a) -> o -> FlexRig' a -> FlexRig' a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' o (FlexRig' a) -> o -> FlexRig' a
    forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
    view (FlexRig' a -> f (FlexRig' a)) -> o -> f o
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' o (FlexRig' a)
    lensFlexRig

    -- | What happens to the variables occurring under a constructor?
    underConstructor :: (MonadReader r m, LensFlexRig r a, Semigroup a) => ConHead -> Elims -> m z -> m z
    underConstructor :: forall r (m :: * -> *) a z.
    (MonadReader r m, LensFlexRig r a, Semigroup a) =>
    ConHead -> Elims -> m z -> m z
    underConstructor (ConHead QName
    _c DataOrRecord
    _d Induction
    i [Arg QName]
    fs) Elims
    es =
      case Induction
    i of
        -- Coinductive (record) constructors admit infinite cycles:
        Induction
    CoInductive -> FlexRig' a -> m z -> m z
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
        -- Inductive constructors do not admit infinite cycles:
        Induction
    Inductive   | Elims -> Peano
    forall a. Sized a => a -> Peano
    natSize Elims
    es Peano -> Peano -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg QName] -> Peano
    forall a. Sized a => a -> Peano
    natSize [Arg QName]
    fs -> FlexRig' a -> m z -> m z
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    StronglyRigid
                    | Bool
    otherwise                -> FlexRig' a -> m z -> m z
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
        -- Jesper, 2020-10-22: Issue #4995: treat occurrences in non-fully
        -- applied constructors as weakly rigid.
        -- Ulf, 2019-10-18: Now the termination checker treats inductive recursive records
        -- the same as datatypes, so absense of infinite cycles can be proven in Agda, and thus
        -- the unifier is allowed to do it too. Test case: test/Succeed/Issue1271a.agda
        -- WAS:
        -- -- Inductive record constructors do not admit infinite cycles,
        -- -- but this cannot be proven inside Agda.
        -- -- Thus, unification should not prove it either.

    ---------------------------------------------------------------------------
    -- * Recursively collecting free variables.

    -- | Gather free variables in a collection.
    class Free t where
      -- Misplaced SPECIALIZE pragma:
      -- {-# SPECIALIZE freeVars' :: a -> FreeM Any #-}
      -- So you cannot specialize all instances in one go. :(
      freeVars' :: IsVarSet a c => t -> FreeM a c

      default freeVars' :: (t ~ f b, Foldable f, Free b) => IsVarSet a c => t -> FreeM a c
      freeVars' = (b -> FreeM a c) -> f b -> FreeM a c
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap b -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => b -> FreeM a c
    freeVars'

    instance Free Term where
      -- SPECIALIZE instance does not work as well, see
      -- https://ghc.haskell.org/trac/ghc/ticket/10434#ticket
      -- {-# SPECIALIZE instance Free Term All #-}
      -- {-# SPECIALIZE freeVars' :: Term -> FreeM Any #-}
      -- {-# SPECIALIZE freeVars' :: Term -> FreeM All #-}
      -- {-# SPECIALIZE freeVars' :: Term -> FreeM VarSet #-}
      freeVars' :: forall a c. IsVarSet a c => Term -> FreeM a c
    freeVars' Term
    t = case Term -> Term
    unSpine Term
    t of -- #4484: unSpine to avoid projected variables being treated as StronglyRigid
        Var Variable
    n Elims
    ts     -> Variable -> FreeM a c
    forall (m :: * -> *) a c b.
    (Monad m, IsVarSet a c) =>
    Variable -> FreeT a b m c
    variable Variable
    n FreeM a c -> FreeM a c -> FreeM a c
    forall a. Monoid a => a -> a -> a
    `mappend` do FlexRig' a -> FreeM a c -> FreeM a c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Elims -> FreeM a c
    freeVars' Elims
    ts
        -- λ is not considered guarding, as
        -- we cannot prove that x ≡ λy.x is impossible.
        Lam ArgInfo
    _ Abs Term
    t      -> FlexRig' a -> FreeM a c -> FreeM a c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Abs Term -> FreeM a c
    freeVars' Abs Term
    t
        Lit Literal
    _        -> FreeM a c
    forall a. Monoid a => a
    mempty
        Def QName
    _ Elims
    ts     -> FlexRig' a -> FreeM a c -> FreeM a c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Elims -> FreeM a c
    freeVars' Elims
    ts  -- because we are not in TCM
          -- we cannot query whether we are dealing with a data/record (strongly r.)
          -- or a definition by pattern matching (weakly rigid)
          -- thus, we approximate, losing that x = List x is unsolvable
        Con ConHead
    c ConInfo
    _ Elims
    ts   -> ConHead -> Elims -> FreeM a c -> FreeM a c
    forall r (m :: * -> *) a z.
    (MonadReader r m, LensFlexRig r a, Semigroup a) =>
    ConHead -> Elims -> m z -> m z
    underConstructor ConHead
    c Elims
    ts (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Elims -> FreeM a c
    freeVars' Elims
    ts
        -- Pi is not guarding, since we cannot prove that A ≡ B → A is impossible.
        -- Even as we do not permit infinite type expressions,
        -- we cannot prove their absence (as Set is not inductive).
        -- Also, this is incompatible with univalence (HoTT).
        Pi Dom Type
    a Abs Type
    b       -> (Dom Type, Abs Type) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (Dom Type, Abs Type) -> FreeM a c
    freeVars' (Dom Type
    a,Abs Type
    b)
        Sort Sort
    s       -> Sort -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Sort -> FreeM a c
    freeVars' Sort
    s
        Level Level
    l      -> Level -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Level -> FreeM a c
    freeVars' Level
    l
        MetaV MetaId
    m Elims
    ts   -> FlexRig' a -> FreeM a c -> FreeM a c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig (a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible (a -> FlexRig' a) -> a -> FlexRig' a
    forall a b. (a -> b) -> a -> b
    $ MetaId -> a
    forall el coll. Singleton el coll => el -> coll
    singleton MetaId
    m) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Elims -> FreeM a c
    freeVars' Elims
    ts
        DontCare Term
    mt  -> Modality -> FreeM a c -> FreeM a c
    forall r (m :: * -> *) o z.
    (MonadReader r m, LensModality r, LensModality o) =>
    o -> m z -> m z
    underModality (Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality
    Modality Relevance
    irrelevant Quantity
    unitQuantity Cohesion
    unitCohesion PolarityModality
    unitPolarity) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
    forall a b. (a -> b) -> a -> b
    $ Term -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Term -> FreeM a c
    freeVars' Term
    mt
        Dummy{}      -> FreeM a c
    forall a. Monoid a => a
    mempty

    instance Free t => Free (Type' t) where
      freeVars' :: forall a c. IsVarSet a c => Type' t -> FreeM a c
    freeVars' (El Sort
    s t
    t) =
        ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((FreeEnv' a IgnoreSorts c -> Bool)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((IgnoreSorts
    IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (IgnoreSorts -> Bool)
    -> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
    -> FreeEnv' a IgnoreSorts c
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FreeEnv' a IgnoreSorts c -> IgnoreSorts
    forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
    feIgnoreSorts))
          {- then -} ((Sort, t) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (Sort, t) -> FreeM a c
    freeVars' (Sort
    s, t
    t))
          {- else -} (t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' t
    t)

    instance Free Sort where
      freeVars' :: forall a c. IsVarSet a c => Sort -> FreeM a c
    freeVars' Sort
    s =
        ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((FreeEnv' a IgnoreSorts c -> Bool)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((IgnoreSorts
    IgnoreAll IgnoreSorts -> IgnoreSorts -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (IgnoreSorts -> Bool)
    -> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
    -> FreeEnv' a IgnoreSorts c
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FreeEnv' a IgnoreSorts c -> IgnoreSorts
    forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
    feIgnoreSorts)) ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ {- else -}
        case Sort
    s of
          Univ Univ
    _ Level
    a   -> Level -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Level -> FreeM a c
    freeVars' Level
    a
          Inf Univ
    _ Integer
    _    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty
          Sort
    SizeUniv   -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty
          Sort
    LockUniv   -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty
          Sort
    LevelUniv  -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty
          Sort
    IntervalUniv -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> FlexRig' a
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig (a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible a
    forall a. Monoid a => a
    mempty) (Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Term -> FreeM a c
    freeVars' (Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Term -> Term
    forall t e. Dom' t e -> e
    unDom Dom' Term Term
    a) ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a -> a -> a
    `mappend`
                            FlexRig' a
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid ((Sort, Abs Sort) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (Sort, Abs Sort) -> FreeM a c
    freeVars' (Sort
    s1, Abs Sort
    s2))
          FunSort Sort
    s1 Sort
    s2 -> Sort -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Sort -> FreeM a c
    freeVars' Sort
    s1 ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a -> a -> a
    `mappend` Sort -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Sort -> FreeM a c
    freeVars' Sort
    s2
          UnivSort Sort
    s -> FlexRig' a
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Sort -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Sort -> FreeM a c
    freeVars' Sort
    s
          MetaS MetaId
    x Elims
    es -> FlexRig' a
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig (a -> FlexRig' a
    forall a. a -> FlexRig' a
    Flexible (a -> FlexRig' a) -> a -> FlexRig' a
    forall a b. (a -> b) -> a -> b
    $ MetaId -> a
    forall el coll. Singleton el coll => el -> coll
    singleton MetaId
    x) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Elims -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Elims -> FreeM a c
    freeVars' Elims
    es
          DefS QName
    _ Elims
    es  -> FlexRig' a
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Elims -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Elims -> FreeM a c
    freeVars' Elims
    es
          DummyS{}   -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty

    instance Free Level where
      freeVars' :: forall a c. IsVarSet a c => Level -> FreeM a c
    freeVars' (Max Integer
    _ [PlusLevel' Term]
    as) = [PlusLevel' Term] -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => [PlusLevel' Term] -> FreeM a c
    freeVars' [PlusLevel' Term]
    as

    instance Free t => Free (PlusLevel' t) where
      freeVars' :: forall a c. IsVarSet a c => PlusLevel' t -> FreeM a c
    freeVars' (Plus Integer
    _ t
    l)    = t -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' t
    l

    instance Free t => Free [t]
    instance Free t => Free (List1 t)
    instance Free t => Free (Maybe t)
    instance Free t => Free (WithHiding t)
    instance Free t => Free (Named nm t)
    instance Free t => Free (Ranged t)

    instance (Free t, Free u) => Free (t, u) where
      freeVars' :: forall a c. IsVarSet a c => (t, u) -> FreeM a c
    freeVars' (t
    t, u
    u) = t -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' t
    t FreeM a c -> FreeM a c -> FreeM a c
    forall a. Monoid a => a -> a -> a
    `mappend` u -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => u -> FreeM a c
    freeVars' u
    u

    instance (Free t, Free u, Free v) => Free (t, u, v) where
      freeVars' :: forall a c. IsVarSet a c => (t, u, v) -> FreeM a c
    freeVars' (t
    t, u
    u, v
    v) = t -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' t
    t FreeM a c -> FreeM a c -> FreeM a c
    forall a. Monoid a => a -> a -> a
    `mappend` u -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => u -> FreeM a c
    freeVars' u
    u FreeM a c -> FreeM a c -> FreeM a c
    forall a. Monoid a => a -> a -> a
    `mappend` v -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => v -> FreeM a c
    freeVars' v
    v

    instance Free t => Free (Elim' t) where
      freeVars' :: forall a c. IsVarSet a c => Elim' t -> FreeM a c
    freeVars' (Apply Arg t
    t) = Arg t -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Arg t -> FreeM a c
    freeVars' Arg t
    t
      freeVars' (Proj{} ) = FreeM a c
    forall a. Monoid a => a
    mempty
      freeVars' (IApply t
    x t
    y t
    r) = (t, t, t) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (t, t, t) -> FreeM a c
    freeVars' (t
    x,t
    y,t
    r)

    instance Free t => Free (Arg t) where
      freeVars' :: forall a c. IsVarSet a c => Arg t -> FreeM a c
    freeVars' Arg t
    t = Modality
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall r (m :: * -> *) o z.
    (MonadReader r m, LensModality r, LensModality o) =>
    o -> m z -> m z
    underModality (Arg t -> Modality
    forall a. LensModality a => a -> Modality
    getModality Arg t
    t) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' (t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Arg t -> t
    forall e. Arg e -> e
    unArg Arg t
    t

    instance Free t => Free (Dom t) where
      freeVars' :: forall a c. IsVarSet a c => Dom t -> FreeM a c
    freeVars' Dom t
    d = (Maybe Term, t) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (Maybe Term, t) -> FreeM a c
    freeVars' (Dom t -> Maybe Term
    forall t e. Dom' t e -> Maybe t
    domTactic Dom t
    d, Dom t -> t
    forall t e. Dom' t e -> e
    unDom Dom t
    d)

    instance Free t => Free (Abs t) where
      freeVars' :: forall a c. IsVarSet a c => Abs t -> FreeM a c
    freeVars' (Abs   String
    _ t
    b) = ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    m z -> m z
    underBinder (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' t
    b
      freeVars' (NoAbs String
    _ t
    b) = t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => t -> FreeM a c
    freeVars' t
    b

    instance Free t => Free (Tele t) where
      freeVars' :: forall a c. IsVarSet a c => Tele t -> FreeM a c
    freeVars' Tele t
    EmptyTel          = FreeM a c
    forall a. Monoid a => a
    mempty
      freeVars' (ExtendTel t
    t Abs (Tele t)
    tel) = (t, Abs (Tele t)) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (t, Abs (Tele t)) -> FreeM a c
    freeVars' (t
    t, Abs (Tele t)
    tel)

    instance Free Clause where
      freeVars' :: forall a c. IsVarSet a c => Clause -> FreeM a c
    freeVars' Clause
    cl = Variable
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    Variable -> m z -> m z
    underBinder' (Telescope -> Variable
    forall a. Sized a => a -> Variable
    size (Telescope -> Variable) -> Telescope -> Variable
    forall a b. (a -> b) -> a -> b
    $ Clause -> Telescope
    clauseTel Clause
    cl) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
     -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Maybe Term -> FreeM a c
    freeVars' (Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
    -> Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    cl

    instance Free EqualityView where
      freeVars' :: forall a c. IsVarSet a c => EqualityView -> FreeM a c
    freeVars' = \case
        OtherType Type
    t -> Type -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Type -> FreeM a c
    freeVars' Type
    t
        IdiomType Type
    t -> Type -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Type -> FreeM a c
    freeVars' Type
    t
        EqualityType Range
    _r Sort
    s QName
    _eq Args
    l Arg Term
    t Arg Term
    a Arg Term
    b -> (Sort, Args, Args) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (Sort, Args, Args) -> FreeM a c
    freeVars' (Sort
    s, Args
    l, [Arg Term
    t, Arg Term
    a, Arg Term
    b])