    {-# OPTIONS_GHC -fno-warn-orphans       #-}

    module Agda.Compiler.Treeless.Subst where

    import qualified Data.Map as Map
    import Data.Map (Map)
    import Data.Maybe
    import Data.Semigroup ( Semigroup, (<>), All(..), Any(..) )

    import Agda.Syntax.Treeless
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Impossible

    instance DeBruijn TTerm where
      deBruijnVar :: Int -> TTerm
    deBruijnVar = Int -> TTerm
    TVar
      deBruijnView :: TTerm -> Maybe Int
    deBruijnView (TVar Int
    i) = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i
      deBruijnView TTerm
    _ = Maybe Int
    forall a. Maybe a
    Nothing

    instance Subst TTerm where
      type SubstArg TTerm = TTerm

      applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    applySubst Substitution' (SubstArg TTerm)
    IdS = TTerm -> TTerm
    forall a. a -> a
    id
      applySubst Substitution' (SubstArg TTerm)
    rho = \case
          t :: TTerm
    t@TDef{}    -> TTerm
    t
          t :: TTerm
    t@TLit{}    -> TTerm
    t
          t :: TTerm
    t@TCon{}    -> TTerm
    t
          t :: TTerm
    t@TPrim{}   -> TTerm
    t
          t :: TTerm
    t@TUnit{}   -> TTerm
    t
          t :: TTerm
    t@TSort{}   -> TTerm
    t
          t :: TTerm
    t@TErased{} -> TTerm
    t
          t :: TTerm
    t@TError{}  -> TTerm
    t
          TVar Int
    i         -> Substitution' TTerm -> Int -> TTerm
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution' TTerm
    Substitution' (SubstArg TTerm)
    rho Int
    i
          TApp TTerm
    f Args
    ts      -> TTerm -> Args -> TTerm
    tApp (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TTerm)
    rho TTerm
    f) (Substitution' (SubstArg Args) -> Args -> Args
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Args)
    Substitution' (SubstArg TTerm)
    rho Args
    ts)
          TLam TTerm
    b         -> TTerm -> TTerm
    TLam (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    1 Substitution' TTerm
    Substitution' (SubstArg TTerm)
    rho) TTerm
    b)
          TLet TTerm
    e TTerm
    b       -> TTerm -> TTerm -> TTerm
    TLet (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TTerm)
    rho TTerm
    e) (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    1 Substitution' TTerm
    Substitution' (SubstArg TTerm)
    rho) TTerm
    b)
          TCase Int
    i CaseInfo
    t TTerm
    d [TAlt]
    bs ->
            case Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TTerm)
    rho (Int -> TTerm
    TVar Int
    i) of
              TVar Int
    j  -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    j CaseInfo
    t (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TTerm)
    rho TTerm
    d) (Substitution' (SubstArg [TAlt]) -> [TAlt] -> [TAlt]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [TAlt])
    Substitution' (SubstArg TTerm)
    rho [TAlt]
    bs)
              TTerm
    e       -> TTerm -> TTerm -> TTerm
    TLet TTerm
    e (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    0 CaseInfo
    t (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' TTerm
    Substitution' (SubstArg TTerm)
    rho' TTerm
    d) (Substitution' (SubstArg [TAlt]) -> [TAlt] -> [TAlt]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' TTerm
    Substitution' (SubstArg [TAlt])
    rho' [TAlt]
    bs)
                where rho' :: Substitution' TTerm
    rho' = Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    wkS Int
    1 Substitution' TTerm
    Substitution' (SubstArg TTerm)
    rho
          TCoerce TTerm
    e -> TTerm -> TTerm
    TCoerce (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TTerm)
    rho TTerm
    e)
        where
          tApp :: TTerm -> Args -> TTerm
    tApp (TPrim TPrim
    PSeq) [TTerm
    TErased, TTerm
    b] = TTerm
    b
          tApp TTerm
    f Args
    ts = TTerm -> Args -> TTerm
    TApp TTerm
    f Args
    ts

    instance Subst TAlt where
      type SubstArg TAlt = TTerm
      applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt
    applySubst Substitution' (SubstArg TAlt)
    rho (TACon QName
    c Int
    i TTerm
    b) = QName -> Int -> TTerm -> TAlt
    TACon QName
    c Int
    i (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    i Substitution' TTerm
    Substitution' (SubstArg TAlt)
    rho) TTerm
    b)
      applySubst Substitution' (SubstArg TAlt)
    rho (TALit Literal
    l TTerm
    b)   = Literal -> TTerm -> TAlt
    TALit Literal
    l (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TAlt)
    Substitution' (SubstArg TTerm)
    rho TTerm
    b)
      applySubst Substitution' (SubstArg TAlt)
    rho (TAGuard TTerm
    g TTerm
    b) = TTerm -> TTerm -> TAlt
    TAGuard (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TAlt)
    Substitution' (SubstArg TTerm)
    rho TTerm
    g) (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg TAlt)
    Substitution' (SubstArg TTerm)
    rho TTerm
    b)

    newtype UnderLambda = UnderLambda Any
      deriving (UnderLambda -> UnderLambda -> Bool
    (UnderLambda -> UnderLambda -> Bool)
    -> (UnderLambda -> UnderLambda -> Bool) -> Eq UnderLambda
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: UnderLambda -> UnderLambda -> Bool
    $c/= :: UnderLambda -> UnderLambda -> Bool
    == :: UnderLambda -> UnderLambda -> Bool
    $c== :: UnderLambda -> UnderLambda -> Bool
    Eq, Eq UnderLambda
    Eq UnderLambda
    -> (UnderLambda -> UnderLambda -> Ordering)
    -> (UnderLambda -> UnderLambda -> Bool)
    -> (UnderLambda -> UnderLambda -> Bool)
    -> (UnderLambda -> UnderLambda -> Bool)
    -> (UnderLambda -> UnderLambda -> Bool)
    -> (UnderLambda -> UnderLambda -> UnderLambda)
    -> (UnderLambda -> UnderLambda -> UnderLambda)
    -> Ord UnderLambda
    UnderLambda -> UnderLambda -> Bool
    UnderLambda -> UnderLambda -> Ordering
    UnderLambda -> UnderLambda -> UnderLambda
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: UnderLambda -> UnderLambda -> UnderLambda
    $cmin :: UnderLambda -> UnderLambda -> UnderLambda
    max :: UnderLambda -> UnderLambda -> UnderLambda
    $cmax :: UnderLambda -> UnderLambda -> UnderLambda
    >= :: UnderLambda -> UnderLambda -> Bool
    $c>= :: UnderLambda -> UnderLambda -> Bool
    > :: UnderLambda -> UnderLambda -> Bool
    $c> :: UnderLambda -> UnderLambda -> Bool
    <= :: UnderLambda -> UnderLambda -> Bool
    $c<= :: UnderLambda -> UnderLambda -> Bool
    < :: UnderLambda -> UnderLambda -> Bool
    $c< :: UnderLambda -> UnderLambda -> Bool
    compare :: UnderLambda -> UnderLambda -> Ordering
    $ccompare :: UnderLambda -> UnderLambda -> Ordering
    Ord, Int -> UnderLambda -> ShowS
    [UnderLambda] -> ShowS
    UnderLambda -> String
    (Int -> UnderLambda -> ShowS)
    -> (UnderLambda -> String)
    -> ([UnderLambda] -> ShowS)
    -> Show UnderLambda
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [UnderLambda] -> ShowS
    $cshowList :: [UnderLambda] -> ShowS
    show :: UnderLambda -> String
    $cshow :: UnderLambda -> String
    showsPrec :: Int -> UnderLambda -> ShowS
    $cshowsPrec :: Int -> UnderLambda -> ShowS
    Show, NonEmpty UnderLambda -> UnderLambda
    UnderLambda -> UnderLambda -> UnderLambda
    (UnderLambda -> UnderLambda -> UnderLambda)
    -> (NonEmpty UnderLambda -> UnderLambda)
    -> (forall b. Integral b => b -> UnderLambda -> UnderLambda)
    -> Semigroup UnderLambda
    forall b. Integral b => b -> UnderLambda -> UnderLambda
    forall a.
    (a -> a -> a)
    -> (NonEmpty a -> a)
    -> (forall b. Integral b => b -> a -> a)
    -> Semigroup a
    stimes :: forall b. Integral b => b -> UnderLambda -> UnderLambda
    $cstimes :: forall b. Integral b => b -> UnderLambda -> UnderLambda
    sconcat :: NonEmpty UnderLambda -> UnderLambda
    $csconcat :: NonEmpty UnderLambda -> UnderLambda
    <> :: UnderLambda -> UnderLambda -> UnderLambda
    $c<> :: UnderLambda -> UnderLambda -> UnderLambda
    Semigroup, Semigroup UnderLambda
    UnderLambda
    Semigroup UnderLambda
    -> UnderLambda
    -> (UnderLambda -> UnderLambda -> UnderLambda)
    -> ([UnderLambda] -> UnderLambda)
    -> Monoid UnderLambda
    [UnderLambda] -> UnderLambda
    UnderLambda -> UnderLambda -> UnderLambda
    forall a.
    Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
    mconcat :: [UnderLambda] -> UnderLambda
    $cmconcat :: [UnderLambda] -> UnderLambda
    mappend :: UnderLambda -> UnderLambda -> UnderLambda
    $cmappend :: UnderLambda -> UnderLambda -> UnderLambda
    mempty :: UnderLambda
    $cmempty :: UnderLambda
    Monoid)

    newtype SeqArg = SeqArg All
      deriving (SeqArg -> SeqArg -> Bool
    (SeqArg -> SeqArg -> Bool)
    -> (SeqArg -> SeqArg -> Bool) -> Eq SeqArg
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SeqArg -> SeqArg -> Bool
    $c/= :: SeqArg -> SeqArg -> Bool
    == :: SeqArg -> SeqArg -> Bool
    $c== :: SeqArg -> SeqArg -> Bool
    Eq, Eq SeqArg
    Eq SeqArg
    -> (SeqArg -> SeqArg -> Ordering)
    -> (SeqArg -> SeqArg -> Bool)
    -> (SeqArg -> SeqArg -> Bool)
    -> (SeqArg -> SeqArg -> Bool)
    -> (SeqArg -> SeqArg -> Bool)
    -> (SeqArg -> SeqArg -> SeqArg)
    -> (SeqArg -> SeqArg -> SeqArg)
    -> Ord SeqArg
    SeqArg -> SeqArg -> Bool
    SeqArg -> SeqArg -> Ordering
    SeqArg -> SeqArg -> SeqArg
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: SeqArg -> SeqArg -> SeqArg
    $cmin :: SeqArg -> SeqArg -> SeqArg
    max :: SeqArg -> SeqArg -> SeqArg
    $cmax :: SeqArg -> SeqArg -> SeqArg
    >= :: SeqArg -> SeqArg -> Bool
    $c>= :: SeqArg -> SeqArg -> Bool
    > :: SeqArg -> SeqArg -> Bool
    $c> :: SeqArg -> SeqArg -> Bool
    <= :: SeqArg -> SeqArg -> Bool
    $c<= :: SeqArg -> SeqArg -> Bool
    < :: SeqArg -> SeqArg -> Bool
    $c< :: SeqArg -> SeqArg -> Bool
    compare :: SeqArg -> SeqArg -> Ordering
    $ccompare :: SeqArg -> SeqArg -> Ordering
    Ord, Int -> SeqArg -> ShowS
    [SeqArg] -> ShowS
    SeqArg -> String
    (Int -> SeqArg -> ShowS)
    -> (SeqArg -> String) -> ([SeqArg] -> ShowS) -> Show SeqArg
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [SeqArg] -> ShowS
    $cshowList :: [SeqArg] -> ShowS
    show :: SeqArg -> String
    $cshow :: SeqArg -> String
    showsPrec :: Int -> SeqArg -> ShowS
    $cshowsPrec :: Int -> SeqArg -> ShowS
    Show, NonEmpty SeqArg -> SeqArg
    SeqArg -> SeqArg -> SeqArg
    (SeqArg -> SeqArg -> SeqArg)
    -> (NonEmpty SeqArg -> SeqArg)
    -> (forall b. Integral b => b -> SeqArg -> SeqArg)
    -> Semigroup SeqArg
    forall b. Integral b => b -> SeqArg -> SeqArg
    forall a.
    (a -> a -> a)
    -> (NonEmpty a -> a)
    -> (forall b. Integral b => b -> a -> a)
    -> Semigroup a
    stimes :: forall b. Integral b => b -> SeqArg -> SeqArg
    $cstimes :: forall b. Integral b => b -> SeqArg -> SeqArg
    sconcat :: NonEmpty SeqArg -> SeqArg
    $csconcat :: NonEmpty SeqArg -> SeqArg
    <> :: SeqArg -> SeqArg -> SeqArg
    $c<> :: SeqArg -> SeqArg -> SeqArg
    Semigroup, Semigroup SeqArg
    SeqArg
    Semigroup SeqArg
    -> SeqArg
    -> (SeqArg -> SeqArg -> SeqArg)
    -> ([SeqArg] -> SeqArg)
    -> Monoid SeqArg
    [SeqArg] -> SeqArg
    SeqArg -> SeqArg -> SeqArg
    forall a.
    Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
    mconcat :: [SeqArg] -> SeqArg
    $cmconcat :: [SeqArg] -> SeqArg
    mappend :: SeqArg -> SeqArg -> SeqArg
    $cmappend :: SeqArg -> SeqArg -> SeqArg
    mempty :: SeqArg
    $cmempty :: SeqArg
    Monoid)

    data Occurs = Occurs Int UnderLambda SeqArg
      deriving (Occurs -> Occurs -> Bool
    (Occurs -> Occurs -> Bool)
    -> (Occurs -> Occurs -> Bool) -> Eq Occurs
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Occurs -> Occurs -> Bool
    $c/= :: Occurs -> Occurs -> Bool
    == :: Occurs -> Occurs -> Bool
    $c== :: Occurs -> Occurs -> Bool
    Eq, Eq Occurs
    Eq Occurs
    -> (Occurs -> Occurs -> Ordering)
    -> (Occurs -> Occurs -> Bool)
    -> (Occurs -> Occurs -> Bool)
    -> (Occurs -> Occurs -> Bool)
    -> (Occurs -> Occurs -> Bool)
    -> (Occurs -> Occurs -> Occurs)
    -> (Occurs -> Occurs -> Occurs)
    -> Ord Occurs
    Occurs -> Occurs -> Bool
    Occurs -> Occurs -> Ordering
    Occurs -> Occurs -> Occurs
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Occurs -> Occurs -> Occurs
    $cmin :: Occurs -> Occurs -> Occurs
    max :: Occurs -> Occurs -> Occurs
    $cmax :: Occurs -> Occurs -> Occurs
    >= :: Occurs -> Occurs -> Bool
    $c>= :: Occurs -> Occurs -> Bool
    > :: Occurs -> Occurs -> Bool
    $c> :: Occurs -> Occurs -> Bool
    <= :: Occurs -> Occurs -> Bool
    $c<= :: Occurs -> Occurs -> Bool
    < :: Occurs -> Occurs -> Bool
    $c< :: Occurs -> Occurs -> Bool
    compare :: Occurs -> Occurs -> Ordering
    $ccompare :: Occurs -> Occurs -> Ordering
    Ord, Int -> Occurs -> ShowS
    [Occurs] -> ShowS
    Occurs -> String
    (Int -> Occurs -> ShowS)
    -> (Occurs -> String) -> ([Occurs] -> ShowS) -> Show Occurs
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Occurs] -> ShowS
    $cshowList :: [Occurs] -> ShowS
    show :: Occurs -> String
    $cshow :: Occurs -> String
    showsPrec :: Int -> Occurs -> ShowS
    $cshowsPrec :: Int -> Occurs -> ShowS
    Show)

    once :: Occurs
    once :: Occurs
    once = Int -> UnderLambda -> SeqArg -> Occurs
    Occurs Int
    1 UnderLambda
    forall a. Monoid a => a
    mempty (All -> SeqArg
    SeqArg (All -> SeqArg) -> All -> SeqArg
    forall a b. (a -> b) -> a -> b
    $ Bool -> All
    All Bool
    False)

    inSeq :: Occurs -> Occurs
    inSeq :: Occurs -> Occurs
    inSeq (Occurs Int
    n UnderLambda
    l SeqArg
    _) = Int -> UnderLambda -> SeqArg -> Occurs
    Occurs Int
    n UnderLambda
    l SeqArg
    forall a. Monoid a => a
    mempty

    underLambda :: Occurs -> Occurs
    underLambda :: Occurs -> Occurs
    underLambda Occurs
    o = Occurs
    o Occurs -> Occurs -> Occurs
    forall a. Semigroup a => a -> a -> a
    <> Int -> UnderLambda -> SeqArg -> Occurs
    Occurs Int
    0 (Any -> UnderLambda
    UnderLambda (Any -> UnderLambda) -> Any -> UnderLambda
    forall a b. (a -> b) -> a -> b
    $ Bool -> Any
    Any Bool
    True) SeqArg
    forall a. Monoid a => a
    mempty

    instance Semigroup Occurs where
      Occurs Int
    a UnderLambda
    k SeqArg
    s <> :: Occurs -> Occurs -> Occurs
    <> Occurs Int
    b UnderLambda
    l SeqArg
    t = Int -> UnderLambda -> SeqArg -> Occurs
    Occurs (Int
    a Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    b) (UnderLambda
    k UnderLambda -> UnderLambda -> UnderLambda
    forall a. Semigroup a => a -> a -> a
    <> UnderLambda
    l) (SeqArg
    s SeqArg -> SeqArg -> SeqArg
    forall a. Semigroup a => a -> a -> a
    <> SeqArg
    t)

    instance Monoid Occurs where
      mempty :: Occurs
    mempty  = Int -> UnderLambda -> SeqArg -> Occurs
    Occurs Int
    0 UnderLambda
    forall a. Monoid a => a
    mempty SeqArg
    forall a. Monoid a => a
    mempty
      mappend :: Occurs -> Occurs -> Occurs
    mappend = Occurs -> Occurs -> Occurs
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- Andreas, 2019-07-10: this free variable computation should be rewritten
    -- in the style of TypeChecking.Free.Lazy.
    -- https://github.com/agda/agda/commit/03eb3945114a4ccdb449f22d69db8d6eaa4699b8#commitcomment-34249120

    class HasFree a where
      freeVars :: a -> Map Int Occurs

    freeIn :: HasFree a => Int -> a -> Bool
    freeIn :: forall a. HasFree a => Int -> a -> Bool
    freeIn Int
    i a
    x = Int -> Map Int Occurs -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member Int
    i (a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    x)

    occursIn :: HasFree a => Int -> a -> Occurs
    occursIn :: forall a. HasFree a => Int -> a -> Occurs
    occursIn Int
    i a
    x = Occurs -> Maybe Occurs -> Occurs
    forall a. a -> Maybe a -> a
    fromMaybe Occurs
    forall a. Monoid a => a
    mempty (Maybe Occurs -> Occurs) -> Maybe Occurs -> Occurs
    forall a b. (a -> b) -> a -> b
    $ Int -> Map Int Occurs -> Maybe Occurs
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Int
    i (a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    x)

    instance HasFree Int where
      freeVars :: Int -> Map Int Occurs
    freeVars Int
    x = Int -> Occurs -> Map Int Occurs
    forall k a. k -> a -> Map k a
    Map.singleton Int
    x Occurs
    once

    instance HasFree a => HasFree [a] where
      freeVars :: [a] -> Map Int Occurs
    freeVars [a]
    xs = (Occurs -> Occurs -> Occurs) -> [Map Int Occurs] -> Map Int Occurs
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith Occurs -> Occurs -> Occurs
    forall a. Monoid a => a -> a -> a
    mappend ([Map Int Occurs] -> Map Int Occurs)
    -> [Map Int Occurs] -> Map Int Occurs
    forall a b. (a -> b) -> a -> b
    $ (a -> Map Int Occurs) -> [a] -> [Map Int Occurs]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars [a]
    xs

    instance (HasFree a, HasFree b) => HasFree (a, b) where
      freeVars :: (a, b) -> Map Int Occurs
    freeVars (a
    x, b
    y) = (Occurs -> Occurs -> Occurs)
    -> Map Int Occurs -> Map Int Occurs -> Map Int Occurs
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith Occurs -> Occurs -> Occurs
    forall a. Monoid a => a -> a -> a
    mappend (a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    x) (b -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars b
    y)

    data Binder a = Binder Int a

    instance HasFree a => HasFree (Binder a) where
      freeVars :: Binder a -> Map Int Occurs
    freeVars (Binder Int
    0 a
    x) = a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    x
      freeVars (Binder Int
    k a
    x) = (Int -> Occurs -> Bool) -> Map Int Occurs -> Map Int Occurs
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (\ Int
    k Occurs
    _ -> Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0) (Map Int Occurs -> Map Int Occurs)
    -> Map Int Occurs -> Map Int Occurs
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> Map Int Occurs -> Map Int Occurs
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract Int
    k) (Map Int Occurs -> Map Int Occurs)
    -> Map Int Occurs -> Map Int Occurs
    forall a b. (a -> b) -> a -> b
    $ a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    x

    newtype InSeq a = InSeq a

    instance HasFree a => HasFree (InSeq a) where
      freeVars :: InSeq a -> Map Int Occurs
    freeVars (InSeq a
    x) = Occurs -> Occurs
    inSeq (Occurs -> Occurs) -> Map Int Occurs -> Map Int Occurs
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    x

    instance HasFree TTerm where
      freeVars :: TTerm -> Map Int Occurs
    freeVars = \case
        TDef{}    -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TLit{}    -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TCon{}    -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TPrim{}   -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TUnit{}   -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TSort{}   -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TErased{} -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TError{}  -> Map Int Occurs
    forall k a. Map k a
    Map.empty
        TVar Int
    i         -> Int -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars Int
    i
        TApp (TPrim TPrim
    PSeq) [TVar Int
    x, TTerm
    b] -> (InSeq Int, TTerm) -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (Int -> InSeq Int
    forall a. a -> InSeq a
    InSeq Int
    x, TTerm
    b)
        TApp TTerm
    f Args
    ts      -> (TTerm, Args) -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (TTerm
    f, Args
    ts)
        TLam TTerm
    b         -> Occurs -> Occurs
    underLambda (Occurs -> Occurs) -> Map Int Occurs -> Map Int Occurs
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Binder TTerm -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (Int -> TTerm -> Binder TTerm
    forall a. Int -> a -> Binder a
    Binder Int
    1 TTerm
    b)
        TLet TTerm
    e TTerm
    b       -> (TTerm, Binder TTerm) -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (TTerm
    e, Int -> TTerm -> Binder TTerm
    forall a. Int -> a -> Binder a
    Binder Int
    1 TTerm
    b)
        TCase Int
    i CaseInfo
    _ TTerm
    d [TAlt]
    bs -> (Int, (TTerm, [TAlt])) -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (Int
    i, (TTerm
    d, [TAlt]
    bs))
        TCoerce TTerm
    t      -> TTerm -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars TTerm
    t

    instance HasFree TAlt where
      freeVars :: TAlt -> Map Int Occurs
    freeVars = \case
        TACon QName
    _ Int
    i TTerm
    b -> Binder TTerm -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (Int -> TTerm -> Binder TTerm
    forall a. Int -> a -> Binder a
    Binder Int
    i TTerm
    b)
        TALit Literal
    _ TTerm
    b   -> TTerm -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars TTerm
    b
        TAGuard TTerm
    g TTerm
    b -> (TTerm, TTerm) -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars (TTerm
    g, TTerm
    b)

    -- | Strenghtening.
    tryStrengthen :: (HasFree a, Subst a) => Int -> a -> Maybe a
    tryStrengthen :: forall a. (HasFree a, Subst a) => Int -> a -> Maybe a
    tryStrengthen Int
    n a
    t =
      case Map Int Occurs -> Maybe ((Int, Occurs), Map Int Occurs)
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.minViewWithKey (a -> Map Int Occurs
    forall a. HasFree a => a -> Map Int Occurs
    freeVars a
    t) of
        Just ((Int
    i, Occurs
    _), Map Int Occurs
    _) | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n -> Maybe a
    forall a. Maybe a
    Nothing
        Maybe ((Int, Occurs), Map Int Occurs)
    _ -> a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Impossible -> Int -> Substitution' (SubstArg a)
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible Int
    n) a
    t