    -- | 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        ( guard )
    import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, Reader, runReader )

    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import Data.Semigroup ( Semigroup, (<>) )

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

    import Agda.Utils.Functor
    import Agda.Utils.Lens
    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 -> IntSet
    theMetaSet :: IntSet }
      deriving (MetaSet -> MetaSet -> Bool
    (MetaSet -> MetaSet -> Bool)
    -> (MetaSet -> MetaSet -> Bool) -> Eq MetaSet
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: MetaSet -> MetaSet -> Bool
    $c/= :: MetaSet -> MetaSet -> Bool
    == :: MetaSet -> MetaSet -> Bool
    $c== :: 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
    showList :: [MetaSet] -> ShowS
    $cshowList :: [MetaSet] -> ShowS
    show :: MetaSet -> String
    $cshow :: MetaSet -> String
    showsPrec :: Variable -> MetaSet -> ShowS
    $cshowsPrec :: Variable -> MetaSet -> ShowS
    Show, MetaSet
    MetaSet -> Bool
    MetaSet -> (MetaSet -> Bool) -> Null MetaSet
    forall a. a -> (a -> Bool) -> Null a
    null :: MetaSet -> Bool
    $cnull :: MetaSet -> Bool
    empty :: MetaSet
    $cempty :: MetaSet
    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
    stimes :: forall b. Integral b => b -> MetaSet -> MetaSet
    $cstimes :: forall b. Integral b => b -> MetaSet -> MetaSet
    sconcat :: NonEmpty MetaSet -> MetaSet
    $csconcat :: NonEmpty MetaSet -> MetaSet
    <> :: MetaSet -> MetaSet -> MetaSet
    $c<> :: MetaSet -> 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
    mconcat :: [MetaSet] -> MetaSet
    $cmconcat :: [MetaSet] -> MetaSet
    mappend :: MetaSet -> MetaSet -> MetaSet
    $cmappend :: MetaSet -> MetaSet -> MetaSet
    mempty :: MetaSet
    $cmempty :: MetaSet
    Monoid)

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

    insertMetaSet :: MetaId -> MetaSet -> MetaSet
    insertMetaSet :: MetaId -> MetaSet -> MetaSet
    insertMetaSet (MetaId Variable
    m) (MetaSet IntSet
    ms) = IntSet -> MetaSet
    MetaSet (IntSet -> MetaSet) -> IntSet -> MetaSet
    forall a b. (a -> b) -> a -> b
    $ Variable -> IntSet -> IntSet
    IntSet.insert Variable
    m IntSet
    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 = (Variable -> a -> a) -> a -> IntSet -> a
    forall b. (Variable -> b -> b) -> b -> IntSet -> b
    IntSet.foldr (MetaId -> a -> a
    f (MetaId -> a -> a) -> (Variable -> MetaId) -> Variable -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Variable -> MetaId
    MetaId) a
    e (IntSet -> a) -> IntSet -> a
    forall a b. (a -> b) -> a -> b
    $ MetaSet -> IntSet
    theMetaSet 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
    /= :: FlexRig' a -> FlexRig' a -> Bool
    $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
    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
    showList :: [FlexRig' a] -> ShowS
    $cshowList :: forall a. Show a => [FlexRig' a] -> ShowS
    show :: FlexRig' a -> String
    $cshow :: forall a. Show a => FlexRig' a -> String
    showsPrec :: Variable -> FlexRig' a -> ShowS
    $cshowsPrec :: forall a. Show a => Variable -> 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
    <$ :: forall a b. a -> FlexRig' b -> FlexRig' a
    $c<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
    fmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
    $cfmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
    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
    product :: forall a. Num a => FlexRig' a -> a
    $cproduct :: forall a. Num a => FlexRig' a -> a
    sum :: forall a. Num a => FlexRig' a -> a
    $csum :: forall a. Num a => FlexRig' a -> a
    minimum :: forall a. Ord a => FlexRig' a -> a
    $cminimum :: forall a. Ord a => FlexRig' a -> a
    maximum :: forall a. Ord a => FlexRig' a -> a
    $cmaximum :: forall a. Ord a => FlexRig' a -> a
    elem :: forall a. Eq a => a -> FlexRig' a -> Bool
    $celem :: forall a. Eq a => a -> FlexRig' a -> Bool
    length :: forall a. FlexRig' a -> Variable
    $clength :: forall a. FlexRig' a -> Variable
    null :: forall a. FlexRig' a -> Bool
    $cnull :: forall a. FlexRig' a -> Bool
    toList :: forall a. FlexRig' a -> [a]
    $ctoList :: forall a. FlexRig' a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    foldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
    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
    $cfoldl :: forall b a. (b -> a -> 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
    $cfoldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
    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
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
    fold :: forall m. Monoid m => FlexRig' m -> m
    $cfold :: forall m. Monoid m => FlexRig' m -> m
    Foldable)

    type FlexRig = FlexRig' MetaSet

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

    instance LensFlexRig a (FlexRig' a) where
      lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)
    lensFlexRig FlexRig' a -> f (FlexRig' a)
    f FlexRig' a
    x = FlexRig' a -> f (FlexRig' a)
    f FlexRig' a
    x

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

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

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

    isStronglyRigid :: LensFlexRig a o => o -> Bool
    isStronglyRigid :: forall a o. LensFlexRig a o => o -> Bool
    isStronglyRigid o
    o = case o
    o o -> Lens' (FlexRig' a) o -> FlexRig' a
    forall o i. o -> Lens' i o -> i
    ^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' a) o
    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
    showList :: [VarOcc' a] -> ShowS
    $cshowList :: forall a. Show a => [VarOcc' a] -> ShowS
    show :: VarOcc' a -> String
    $cshow :: forall a. Show a => VarOcc' a -> String
    showsPrec :: Variable -> VarOcc' a -> ShowS
    $cshowsPrec :: forall a. Show a => Variable -> 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 a (VarOcc' a) where
      lensFlexRig :: Lens' (FlexRig' a) (VarOcc' 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ FlexRig' a
    fr' -> FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc FlexRig' a
    fr' Modality
    m
    -- lensFlexRig :: Lens' (FlexRig' a) (VarOcc' 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
    /= :: VarMap' a -> VarMap' a -> Bool
    $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
    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
    showList :: [VarMap' a] -> ShowS
    $cshowList :: forall a. Show a => [VarMap' a] -> ShowS
    show :: VarMap' a -> String
    $cshow :: forall a. Show a => VarMap' a -> String
    showsPrec :: Variable -> VarMap' a -> ShowS
    $cshowsPrec :: forall a. Show a => Variable -> 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 (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
    showList :: [FlexRigMap] -> ShowS
    $cshowList :: [FlexRigMap] -> ShowS
    show :: FlexRigMap -> String
    $cshow :: FlexRigMap -> String
    showsPrec :: Variable -> FlexRigMap -> ShowS
    $cshowsPrec :: Variable -> 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 (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 (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
    /= :: IgnoreSorts -> IgnoreSorts -> Bool
    $c/= :: IgnoreSorts -> IgnoreSorts -> Bool
    == :: IgnoreSorts -> IgnoreSorts -> Bool
    $c== :: 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
    showList :: [IgnoreSorts] -> ShowS
    $cshowList :: [IgnoreSorts] -> ShowS
    show :: IgnoreSorts -> String
    $cshow :: IgnoreSorts -> String
    showsPrec :: Variable -> IgnoreSorts -> ShowS
    $cshowsPrec :: Variable -> 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 a (FreeEnv' a b c) where
      lensFlexRig :: Lens' (FlexRig' a) (FreeEnv' a b c)
    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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ FlexRig' a
    fr -> FreeEnv' a b c
    e { feFlexRig :: FlexRig' a
    feFlexRig = FlexRig' a
    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 :: Modality
    feModality = Modality -> Modality
    f (FreeEnv' a b c -> Modality
    forall a b c. FreeEnv' a b c -> Modality
    feModality FreeEnv' a b c
    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 :: forall a b c.
    b
    -> FlexRig' a
    -> Modality
    -> (Maybe Variable -> c)
    -> FreeEnv' a b c
    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 (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)
    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
      FlexRig' a
    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
      Modality
    r <- (FreeEnv' a b c -> Modality) -> ReaderT (FreeEnv' a b c) m Modality
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks FreeEnv' a b c -> Modality
    forall a b c. FreeEnv' a b c -> Modality
    feModality
      Maybe Variable -> c
    s <- (FreeEnv' a b c -> Maybe Variable -> c)
    -> ReaderT (FreeEnv' a b c) m (Maybe Variable -> c)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks FreeEnv' a b c -> Maybe Variable -> c
    forall a b c. FreeEnv' a b c -> Maybe Variable -> c
    feSingleton
      c -> FreeT a b m c
    forall (m :: * -> *) a. Monad m => a -> m a
    return (c -> FreeT a b m c) -> c -> FreeT a b m c
    forall a b. (a -> b) -> a -> b
    $ VarOcc' a -> c -> c
    forall a c. IsVarSet a c => VarOcc' a -> c -> c
    withVarOcc (FlexRig' a -> Modality -> VarOcc' a
    forall a. FlexRig' a -> Modality -> VarOcc' a
    VarOcc FlexRig' a
    o Modality
    r) (Maybe Variable -> c
    s (Maybe Variable -> c) -> Maybe Variable -> c
    forall a b. (a -> b) -> a -> b
    $ Variable -> Maybe Variable
    forall a. a -> Maybe a
    Just Variable
    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
      Variable
    i <- Maybe Variable
    x
      Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Variable
    i Variable -> Variable -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Variable
    n
      Variable -> Maybe Variable
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Variable -> Maybe Variable) -> Variable -> Maybe Variable
    forall a b. (a -> b) -> a -> b
    $ Variable
    i Variable -> Variable -> Variable
    forall a. Num a => a -> a -> a
    - Variable
    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 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 :: Maybe Variable -> c
    feSingleton = FreeEnv' a b c -> Maybe Variable -> c
    forall a b c. FreeEnv' a b c -> Maybe Variable -> c
    feSingleton FreeEnv' a b c
    e (Maybe Variable -> c)
    -> (Maybe Variable -> Maybe Variable) -> Maybe Variable -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Variable -> Maybe Variable -> Maybe Variable
    subVar Variable
    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 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 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

    -- | Changing the 'FlexRig' context.
    underFlexRig :: (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) => o -> m z -> m z
    underFlexRig :: forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
    o -> m z -> m z
    underFlexRig = (r -> r) -> m z -> m z
    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' (FlexRig' a) r -> LensMap (FlexRig' a) r
    forall i o. Lens' i o -> LensMap i o
    over forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' a) r
    lensFlexRig LensMap (FlexRig' a) r
    -> (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' (FlexRig' a) o -> o -> FlexRig' a
    forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
    view forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' a) o
    lensFlexRig

    -- | What happens to the variables occurring under a constructor?
    underConstructor :: (MonadReader r m, LensFlexRig a r, Semigroup a) => ConHead -> Elims -> m z -> m z
    underConstructor :: forall r (m :: * -> *) a z.
    (MonadReader r m, LensFlexRig a r, 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 a r, Semigroup a, LensFlexRig a o) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid
        -- Inductive constructors do not admit infinite cycles:
        Induction
    Inductive   | Elims -> Variable
    forall a. Sized a => a -> Variable
    size Elims
    es Variable -> Variable -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg QName] -> Variable
    forall a. Sized a => a -> Variable
    size [Arg QName]
    fs -> FlexRig' a -> m z -> m z
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
    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 a r, Semigroup a, LensFlexRig a o) =>
    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 (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
    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 -> FreeT a IgnoreSorts Identity c
    forall (m :: * -> *) a c b.
    (Monad m, IsVarSet a c) =>
    Variable -> FreeT a b m c
    variable Variable
    n FreeT a IgnoreSorts Identity c
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a. Monoid a => a -> a -> a
    `mappend` do FlexRig' a
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c)
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> 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
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c)
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Abs Term
    t
        Lit Literal
    _        -> FreeT a IgnoreSorts Identity c
    forall a. Monoid a => a
    mempty
        Def QName
    _ Elims
    ts     -> FlexRig' a
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
    o -> m z -> m z
    underFlexRig FlexRig' a
    forall a. FlexRig' a
    WeaklyRigid (FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c)
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> 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
    -> FreeT a IgnoreSorts Identity c
    -> FreeT a IgnoreSorts Identity c
    forall r (m :: * -> *) a z.
    (MonadReader r m, LensFlexRig a r, Semigroup a) =>
    ConHead -> Elims -> m z -> m z
    underConstructor ConHead
    c Elims
    ts (FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c)
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> 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) -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' (Dom Type
    a,Abs Type
    b)
        Sort Sort
    s       -> Sort -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Sort
    s
        Level Level
    l      -> Level -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Level
    l
        MetaV MetaId
    m Elims
    ts   -> FlexRig' a
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall r (m :: * -> *) a o z.
    (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
    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) (FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c)
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a b. (a -> b) -> a -> b
    $ Elims -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Elims
    ts
        DontCare Term
    mt  -> Modality
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall r (m :: * -> *) o z.
    (MonadReader r m, LensModality r, LensModality o) =>
    o -> m z -> m z
    underModality (Relevance -> Quantity -> Cohesion -> Modality
    Modality Relevance
    Irrelevant Quantity
    unitQuantity Cohesion
    unitCohesion) (FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c)
    -> FreeT a IgnoreSorts Identity c -> FreeT a IgnoreSorts Identity c
    forall a b. (a -> b) -> a -> b
    $ Term -> FreeT a IgnoreSorts Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Term
    mt
        Dummy{}      -> FreeT a IgnoreSorts Identity 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
    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
    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
          Type Level
    a     -> Level -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Level
    a
          Prop Level
    a     -> Level -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Level
    a
          Inf IsFibrant
    _ Integer
    _    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall a. Monoid a => a
    mempty
          SSet Level
    a     -> Level -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Level
    a
          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
          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 a r, Semigroup a, LensFlexRig a o) =>
    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
    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 a r, Semigroup a, LensFlexRig a o) =>
    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
    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
    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
    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 a r, Semigroup a, LensFlexRig a o) =>
    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
    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 a r, Semigroup a, LensFlexRig a o) =>
    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
    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 a r, Semigroup a, LensFlexRig a o) =>
    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
    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
    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
    freeVars' t
    l

    instance Free t => Free [t]            where
    instance Free t => Free (Maybe t)      where
    instance Free t => Free (WithHiding t) where
    instance Free t => Free (Named nm 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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    freeVars' Type
    t
        IdiomType Type
    t -> Type -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Type
    t
        EqualityType Sort
    s QName
    _eq [Arg Term]
    l Arg Term
    t Arg Term
    a Arg Term
    b -> (Sort, [Arg Term], [Arg Term]) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' (Sort
    s, [Arg Term]
    l, [Arg Term
    t, Arg Term
    a, Arg Term
    b])