    module Agda.TypeChecking.Substitute.Class where

    import Control.Arrow ((***), second)

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

    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Substitute.DeBruijn

    import Agda.Utils.Empty
    import Agda.Utils.List

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Application
    ---------------------------------------------------------------------------

    -- | Apply something to a bunch of arguments.
    --   Preserves blocking tags (application can never resolve blocking).
    class Apply t where
      apply  :: t -> Args -> t
      applyE :: t -> Elims -> t

      apply t
    t Args
    args = t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    applyE t
    t (Elims -> t) -> Elims -> t
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args
      -- Andreas, 2018-06-18, issue #3136
      -- This default instance should be removed to get more precise
      -- crash locations (raise the IMPOSSIBLE in a more specific place).
      -- applyE t es  = apply  t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
        -- precondition: all @es@ are @Apply@s

    -- | Apply to some default arguments.
    applys :: Apply t => t -> [Term] -> t
    applys :: forall t. Apply t => t -> [Term] -> t
    applys t
    t [Term]
    vs = t -> Args -> t
    forall t. Apply t => t -> Args -> t
    apply t
    t (Args -> t) -> Args -> t
    forall a b. (a -> b) -> a -> b
    $ (Term -> Arg Term) -> [Term] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> Arg Term
    forall a. a -> Arg a
    defaultArg [Term]
    vs

    -- | Apply to a single default argument.
    apply1 :: Apply t => t -> Term -> t
    apply1 :: forall t. Apply t => t -> Term -> t
    apply1 t
    t Term
    u = t -> [Term] -> t
    forall t. Apply t => t -> [Term] -> t
    applys t
    t [ Term
    u ]

    ---------------------------------------------------------------------------
    -- * Abstraction
    ---------------------------------------------------------------------------

    -- | @(abstract args v) `apply` args --> v[args]@.
    class Abstract t where
      abstract :: Telescope -> t -> t

    ---------------------------------------------------------------------------
    -- * Substitution and shifting\/weakening\/strengthening
    ---------------------------------------------------------------------------

    -- | Apply a substitution.

    -- For terms:
    --
    --  Γ ⊢ ρ : Δ
    --  Δ ⊢ t : A
    -- -----------
    -- Γ ⊢ tρ : Aρ

    class DeBruijn (SubstArg a) => Subst a where
      type SubstArg a
      applySubst :: Substitution' (SubstArg a) -> a -> a

      default applySubst :: (a ~ f b, Functor f, Subst b, SubstArg a ~ SubstArg b) => Substitution' (SubstArg a) -> a -> a
      applySubst Substitution' (SubstArg a)
    rho = (b -> b) -> f b -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg b)
    rho)

    -- | Simple constraint alias for a `Subst` instance `a` with arg type `t`.
    type SubstWith t a = (Subst a, SubstArg a ~ t)

    -- | `Subst` instance whose agument type is itself
    type EndoSubst a = SubstWith a a

    -- | `Subst` instance whose argument type is `Term`
    type TermSubst a = SubstWith Term a

    -- | Raise de Bruijn index, i.e. weakening
    raise :: Subst a => Nat -> a -> a
    raise :: forall a. Subst a => Nat -> a -> a
    raise = Nat -> Nat -> a -> a
    forall a. Subst a => Nat -> Nat -> a -> a
    raiseFrom Nat
    0

    raiseFrom :: Subst a => Nat -> Nat -> a -> a
    raiseFrom :: forall a. Subst a => Nat -> Nat -> a -> a
    raiseFrom Nat
    n Nat
    k = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Nat -> Nat -> Substitution' (SubstArg a)
    forall a. Nat -> Nat -> Substitution' a
    raiseFromS Nat
    n Nat
    k)

    -- | Replace de Bruijn index i by a 'Term' in something.
    subst :: Subst a => Int -> SubstArg a -> a -> a
    subst :: forall a. Subst a => Nat -> SubstArg a -> a -> a
    subst Nat
    i SubstArg a
    u = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution' (SubstArg a) -> a -> a)
    -> Substitution' (SubstArg a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ Nat -> SubstArg a -> Substitution' (SubstArg a)
    forall a. DeBruijn a => Nat -> a -> Substitution' a
    singletonS Nat
    i SubstArg a
    u

    strengthen :: Subst a => Impossible -> a -> a
    strengthen :: forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    err = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Impossible -> [Maybe (SubstArg a)] -> Substitution' (SubstArg a)
    forall a. DeBruijn a => Impossible -> [Maybe a] -> Substitution' a
    compactS Impossible
    err [Maybe (SubstArg a)
    forall a. Maybe a
    Nothing])

    -- | Replace what is now de Bruijn index 0, but go under n binders.
    --   @substUnder n u == subst n (raise n u)@.
    substUnder :: Subst a => Nat -> SubstArg a -> a -> a
    substUnder :: forall a. Subst a => Nat -> SubstArg a -> a -> a
    substUnder Nat
    n SubstArg a
    u = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Nat -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    n (Nat -> SubstArg a -> Substitution' (SubstArg a)
    forall a. DeBruijn a => Nat -> a -> Substitution' a
    singletonS Nat
    0 SubstArg a
    u))

    -- ** Identity instances

    instance Subst QName where
      type SubstArg QName = Term
      applySubst :: Substitution' (SubstArg QName) -> QName -> QName
    applySubst Substitution' (SubstArg QName)
    _ QName
    q = QName
    q

    ---------------------------------------------------------------------------
    -- * Explicit substitutions
    ---------------------------------------------------------------------------

    -- See Syntax.Internal for the definition.

    idS :: Substitution' a
    idS :: forall a. Substitution' a
    idS = Substitution' a
    forall a. Substitution' a
    IdS

    wkS :: Int -> Substitution' a -> Substitution' a
    wkS :: forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    0 Substitution' a
    rho        = Substitution' a
    rho
    wkS Nat
    n (Wk Nat
    m Substitution' a
    rho) = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    Wk (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    m) Substitution' a
    rho
    wkS Nat
    n (EmptyS Impossible
    err) = Impossible -> Substitution' a
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    err
    wkS Nat
    n Substitution' a
    rho        = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    Wk Nat
    n Substitution' a
    rho

    raiseS :: Int -> Substitution' a
    raiseS :: forall a. Nat -> Substitution' a
    raiseS Nat
    n = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    n Substitution' a
    forall a. Substitution' a
    idS

    consS :: DeBruijn a => a -> Substitution' a -> Substitution' a
    consS :: forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS a
    t (Wk Nat
    m Substitution' a
    rho)
      | Just Nat
    n <- a -> Maybe Nat
    forall a. DeBruijn a => a -> Maybe Nat
    deBruijnView a
    t,
        Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1 Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    m = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 Substitution' a
    rho)
    consS a
    u Substitution' a
    rho = a -> Substitution' a -> Substitution' a
    seq a
    u (a
    u a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' a
    rho)

    -- | To replace index @n@ by term @u@, do @applySubst (singletonS n u)@.
    --   @
    --               Γ, Δ ⊢ u : A
    --    ---------------------------------
    --    Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ
    --   @
    singletonS :: DeBruijn a => Int -> a -> Substitution' a
    singletonS :: forall a. DeBruijn a => Nat -> a -> Substitution' a
    singletonS Nat
    n a
    u = (Nat -> a) -> [Nat] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> a
    forall a. DeBruijn a => Nat -> a
    deBruijnVar [Nat
    0..Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1] [a] -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# a -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS a
    u (Nat -> Substitution' a
    forall a. Nat -> Substitution' a
    raiseS Nat
    n)
      -- ALT: foldl (\ s i -> deBruijnVar i `consS` s) (consS u $ raiseS n) $ downFrom n

    -- | Single substitution without disturbing any deBruijn indices.
    --   @
    --             Γ, A, Δ ⊢ u : A
    --    ---------------------------------
    --    Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ
    --   @
    inplaceS :: EndoSubst a => Int -> a -> Substitution' a
    inplaceS :: forall a. EndoSubst a => Nat -> a -> Substitution' a
    inplaceS Nat
    k a
    u = Nat -> a -> Substitution' a
    forall a. DeBruijn a => Nat -> a -> Substitution' a
    singletonS Nat
    k a
    u Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Nat
    k Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) (Nat -> Substitution' a
    forall a. Nat -> Substitution' a
    raiseS Nat
    1)

    -- | Lift a substitution under k binders.
    liftS :: Int -> Substitution' a -> Substitution' a
    liftS :: forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    0 Substitution' a
    rho          = Substitution' a
    rho
    liftS Nat
    k Substitution' a
    IdS          = Substitution' a
    forall a. Substitution' a
    IdS
    liftS Nat
    k (Lift Nat
    n Substitution' a
    rho) = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    Lift (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    k) Substitution' a
    rho
    liftS Nat
    k Substitution' a
    rho          = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    Lift Nat
    k Substitution' a
    rho

    -- | @
    --         Γ ⊢ ρ : Δ, Ψ
    --      -------------------
    --      Γ ⊢ dropS |Ψ| ρ : Δ
    --   @
    dropS :: Int -> Substitution' a -> Substitution' a
    dropS :: forall a. Nat -> Substitution' a -> Substitution' a
    dropS Nat
    0 Substitution' a
    rho                = Substitution' a
    rho
    dropS Nat
    n Substitution' a
    IdS                = Nat -> Substitution' a
    forall a. Nat -> Substitution' a
    raiseS Nat
    n
    dropS Nat
    n (Wk Nat
    m Substitution' a
    rho)         = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    m (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    dropS Nat
    n Substitution' a
    rho)
    dropS Nat
    n (a
    u :# Substitution' a
    rho)         = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    dropS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    rho
    dropS Nat
    n (Strengthen Impossible
    _ Substitution' a
    rho) = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    dropS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    rho
    dropS Nat
    n (Lift Nat
    0 Substitution' a
    rho)       = Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    dropS Nat
    n (Lift Nat
    m Substitution' a
    rho)       = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    1 (Substitution' a -> Substitution' a)
    -> Substitution' a -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    dropS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) (Substitution' a -> Substitution' a)
    -> Substitution' a -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    rho
    dropS Nat
    n (EmptyS Impossible
    err)       = Impossible -> Substitution' a
    forall a. Impossible -> a
    throwImpossible Impossible
    err

    -- | @applySubst (ρ `composeS` σ) v == applySubst ρ (applySubst σ v)@
    composeS :: EndoSubst a => Substitution' a -> Substitution' a -> Substitution' a
    composeS :: forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' a
    rho Substitution' a
    IdS = Substitution' a
    rho
    composeS Substitution' a
    IdS Substitution' a
    sgm = Substitution' a
    sgm
    composeS Substitution' a
    rho (EmptyS Impossible
    err) = Impossible -> Substitution' a
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    err
    composeS Substitution' a
    rho (Wk Nat
    n Substitution' a
    sgm) = Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    dropS Nat
    n Substitution' a
    rho) Substitution' a
    sgm
    composeS Substitution' a
    rho (a
    u :# Substitution' a
    sgm) = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' a
    Substitution' (SubstArg a)
    rho a
    u a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' a
    rho Substitution' a
    sgm
    composeS Substitution' a
    rho (Strengthen Impossible
    err Substitution' a
    sgm) = Impossible -> Substitution' a -> Substitution' a
    forall a. Impossible -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err (Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' a
    rho Substitution' a
    sgm)
    composeS Substitution' a
    rho (Lift Nat
    0 Substitution' a
    sgm) = Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    composeS (a
    u :# Substitution' a
    rho) (Lift Nat
    n Substitution' a
    sgm) = a
    u a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' a
    rho (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    sgm)
    composeS Substitution' a
    rho (Lift Nat
    n Substitution' a
    sgm) = Substitution' a -> Nat -> a
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution' a
    rho Nat
    0 a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' a
    rho (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    1 (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    sgm))

    -- If Γ ⊢ ρ : Δ, Θ then splitS |Θ| ρ = (σ, δ), with
    --   Γ ⊢ σ : Δ
    --   Γ ⊢ δ : Θσ
    splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS :: forall a.
    Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS Nat
    0 Substitution' a
    rho                  = (Substitution' a
    rho, Impossible -> Substitution' a
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    HasCallStack => Impossible
    impossible)
    splitS Nat
    n (a
    u :# Substitution' a
    rho)           = (Substitution' a -> Substitution' a)
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (a
    u a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    :#) ((Substitution' a, Substitution' a)
     -> (Substitution' a, Substitution' a))
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    forall a.
    Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    rho
    splitS Nat
    n (Strengthen Impossible
    err Substitution' a
    rho) = (Substitution' a -> Substitution' a)
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Impossible -> Substitution' a -> Substitution' a
    forall a. Impossible -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err) ((Substitution' a, Substitution' a)
     -> (Substitution' a, Substitution' a))
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    forall a.
    Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    rho
    splitS Nat
    n (Lift Nat
    0 Substitution' a
    _)           = (Substitution' a, Substitution' a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    splitS Nat
    n (Wk Nat
    m Substitution' a
    rho)           = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    m (Substitution' a -> Substitution' a)
    -> (Substitution' a -> Substitution' a)
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    m ((Substitution' a, Substitution' a)
     -> (Substitution' a, Substitution' a))
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    forall a.
    Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS Nat
    n Substitution' a
    rho
    splitS Nat
    n Substitution' a
    IdS                  = (Nat -> Substitution' a
    forall a. Nat -> Substitution' a
    raiseS Nat
    n, Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    n (Substitution' a -> Substitution' a)
    -> Substitution' a -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Substitution' a
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    HasCallStack => Impossible
    impossible)
    splitS Nat
    n (Lift Nat
    m Substitution' a
    rho)         = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    1 (Substitution' a -> Substitution' a)
    -> (Substitution' a -> Substitution' a)
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 ((Substitution' a, Substitution' a)
     -> (Substitution' a, Substitution' a))
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    forall a.
    Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) (Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Substitution' a
    rho)
    splitS Nat
    n (EmptyS Impossible
    err)         = (Substitution' a, Substitution' a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    infixr 4 ++#

    (++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
    [a]
    us ++# :: forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Substitution' a
    rho = (a -> Substitution' a -> Substitution' a)
    -> Substitution' a -> [a] -> Substitution' a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr a -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Substitution' a
    rho [a]
    us

    -- | @
    --      Γ ⊢ ρ : Δ  Γ ⊢ reverse vs : Θ
    --      ----------------------------- (treating Nothing as having any type)
    --        Γ ⊢ prependS vs ρ : Δ, Θ
    --   @
    prependS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    prependS :: forall a.
    DeBruijn a =>
    Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    prependS Impossible
    err [Maybe a]
    us Substitution' a
    rho = (Maybe a -> Substitution' a -> Substitution' a)
    -> Substitution' a -> [Maybe a] -> Substitution' a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Maybe a -> Substitution' a -> Substitution' a
    f Substitution' a
    rho [Maybe a]
    us
      where
        f :: Maybe a -> Substitution' a -> Substitution' a
    f Maybe a
    Nothing  Substitution' a
    rho = Impossible -> Substitution' a -> Substitution' a
    forall a. Impossible -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Substitution' a
    rho
        f (Just a
    u) Substitution' a
    rho = a -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS a
    u Substitution' a
    rho

    parallelS :: DeBruijn a => [a] -> Substitution' a
    parallelS :: forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [a]
    us = [a]
    us [a] -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Substitution' a
    forall a. Substitution' a
    idS

    compactS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a
    compactS :: forall a. DeBruijn a => Impossible -> [Maybe a] -> Substitution' a
    compactS Impossible
    err [Maybe a]
    us = Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    forall a.
    DeBruijn a =>
    Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    prependS Impossible
    err [Maybe a]
    us Substitution' a
    forall a. Substitution' a
    idS

    -- | Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
    strengthenS :: Impossible -> Int -> Substitution' a
    strengthenS :: forall a. Impossible -> Nat -> Substitution' a
    strengthenS Impossible
    err = Substitution' a -> [Substitution' a] -> Nat -> Substitution' a
    forall a. a -> [a] -> Nat -> a
    indexWithDefault Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Substitution' a] -> Nat -> Substitution' a)
    -> [Substitution' a] -> Nat -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ (Substitution' a -> Substitution' a)
    -> Substitution' a -> [Substitution' a]
    forall a. (a -> a) -> a -> [a]
    iterate (Impossible -> Substitution' a -> Substitution' a
    forall a. Impossible -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err) Substitution' a
    forall a. Substitution' a
    idS

    lookupS :: EndoSubst a => Substitution' a -> Nat -> a
    lookupS :: forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution' a
    rho Nat
    i = case Substitution' a
    rho of
      Substitution' a
    IdS                    -> Nat -> a
    forall a. DeBruijn a => Nat -> a
    deBruijnVar Nat
    i
      Wk Nat
    n Substitution' a
    IdS               -> let j :: Nat
    j = Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n in
                                if  Nat
    j Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    0 then a
    forall a. HasCallStack => a
    __IMPOSSIBLE__ else Nat -> a
    forall a. DeBruijn a => Nat -> a
    deBruijnVar Nat
    j
      Wk Nat
    n Substitution' a
    rho               -> Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Nat -> Substitution' a
    forall a. Nat -> Substitution' a
    raiseS Nat
    n) (Substitution' a -> Nat -> a
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution' a
    rho Nat
    i)
      a
    u :# Substitution' a
    rho   | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0    -> a
    u
                 | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    0     -> a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                 | Bool
    otherwise -> Substitution' a -> Nat -> a
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution' a
    rho (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)
      Strengthen Impossible
    err Substitution' a
    rho
                 | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0    -> Impossible -> a
    forall a. Impossible -> a
    throwImpossible Impossible
    err
                 | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    0     -> a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                 | Bool
    otherwise -> Substitution' a -> Nat -> a
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution' a
    rho (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)
      Lift Nat
    n Substitution' a
    rho | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n     -> Nat -> a
    forall a. DeBruijn a => Nat -> a
    deBruijnVar Nat
    i
                 | Bool
    otherwise -> Nat -> a -> a
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n (a -> a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ Substitution' a -> Nat -> a
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution' a
    rho (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n)
      EmptyS Impossible
    err             -> Impossible -> a
    forall a. Impossible -> a
    throwImpossible Impossible
    err

    -- | lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.

    listS :: EndoSubst a => [(Int,a)] -> Substitution' a
    listS :: forall a. EndoSubst a => [(Nat, a)] -> Substitution' a
    listS ((Nat
    i,a
    t):[(Nat, a)]
    ts) = Nat -> a -> Substitution' a
    forall a. DeBruijn a => Nat -> a -> Substitution' a
    singletonS Nat
    i a
    t Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` [(Nat, a)] -> Substitution' a
    forall a. EndoSubst a => [(Nat, a)] -> Substitution' a
    listS [(Nat, a)]
    ts
    listS []         = Substitution' a
    forall a. Substitution' a
    IdS

    -- | @Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ@
    raiseFromS :: Nat -> Nat -> Substitution' a
    raiseFromS :: forall a. Nat -> Nat -> Substitution' a
    raiseFromS Nat
    n Nat
    k = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    n (Substitution' a -> Substitution' a)
    -> Substitution' a -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution' a
    forall a. Nat -> Substitution' a
    raiseS Nat
    k

    ---------------------------------------------------------------------------
    -- * Functions on abstractions
    --   and things we couldn't do before we could define 'absBody'
    ---------------------------------------------------------------------------

    -- | Instantiate an abstraction. Strict in the term.
    absApp :: Subst a => Abs a -> SubstArg a -> a
    absApp :: forall a. Subst a => Abs a -> SubstArg a -> a
    absApp (Abs   ArgName
    _ a
    v) SubstArg a
    u = Nat -> SubstArg a -> a -> a
    forall a. Subst a => Nat -> SubstArg a -> a -> a
    subst Nat
    0 SubstArg a
    u a
    v
    absApp (NoAbs ArgName
    _ a
    v) SubstArg a
    _ = a
    v

    -- | Instantiate an abstraction. Lazy in the term, which allow it to be
    --   __IMPOSSIBLE__ in the case where the variable shouldn't be used but we
    --   cannot use 'noabsApp'. Used in Apply.
    lazyAbsApp :: Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp :: forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp (Abs   ArgName
    _ a
    v) SubstArg a
    u = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (SubstArg a
    u SubstArg a
    -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' (SubstArg a)
    forall a. Substitution' a
    IdS) a
    v  -- Note: do not use consS here!
    lazyAbsApp (NoAbs ArgName
    _ a
    v) SubstArg a
    _ = a
    v

    -- | Instantiate an abstraction that doesn't use its argument.
    noabsApp :: Subst a => Impossible -> Abs a -> a
    noabsApp :: forall a. Subst a => Impossible -> Abs a -> a
    noabsApp Impossible
    err (Abs   ArgName
    _ a
    v) = Impossible -> a -> a
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    err a
    v
    noabsApp Impossible
    _   (NoAbs ArgName
    _ a
    v) = a
    v

    absBody :: Subst a => Abs a -> a
    absBody :: forall a. Subst a => Abs a -> a
    absBody (Abs   ArgName
    _ a
    v) = a
    v
    absBody (NoAbs ArgName
    _ a
    v) = Nat -> a -> a
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 a
    v

    mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a
    mkAbs :: forall a. (Subst a, Free a) => ArgName -> a -> Abs a
    mkAbs ArgName
    x a
    v | Nat
    0 Nat -> a -> Bool
    forall a. Free a => Nat -> a -> Bool
    `freeIn` a
    v = ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x a
    v
              | Bool
    otherwise    = ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    x (Nat -> a -> a
    forall a. Subst a => Nat -> a -> a
    raise (-Nat
    1) a
    v)

    reAbs :: (Subst a, Free a) => Abs a -> Abs a
    reAbs :: forall a. (Subst a, Free a) => Abs a -> Abs a
    reAbs (NoAbs ArgName
    x a
    v) = ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    x a
    v
    reAbs (Abs ArgName
    x a
    v)   = ArgName -> a -> Abs a
    forall a. (Subst a, Free a) => ArgName -> a -> Abs a
    mkAbs ArgName
    x a
    v

    -- | @underAbs k a b@ applies @k@ to @a@ and the content of
    --   abstraction @b@ and puts the abstraction back.
    --   @a@ is raised if abstraction was proper such that
    --   at point of application of @k@ and the content of @b@
    --   are at the same context.
    --   Precondition: @a@ and @b@ are at the same context at call time.
    underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
    underAbs :: forall a b. Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
    underAbs a -> b -> b
    cont a
    a = \case
      Abs   ArgName
    x b
    t -> ArgName -> b -> Abs b
    forall a. ArgName -> a -> Abs a
    Abs   ArgName
    x (b -> Abs b) -> b -> Abs b
    forall a b. (a -> b) -> a -> b
    $ a -> b -> b
    cont (Nat -> a -> a
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 a
    a) b
    t
      NoAbs ArgName
    x b
    t -> ArgName -> b -> Abs b
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    x (b -> Abs b) -> b -> Abs b
    forall a b. (a -> b) -> a -> b
    $ a -> b -> b
    cont a
    a b
    t

    -- | @underLambdas n k a b@ drops @n@ initial 'Lam's from @b@,
    --   performs operation @k@ on @a@ and the body of @b@,
    --   and puts the 'Lam's back.  @a@ is raised correctly
    --   according to the number of abstractions.
    underLambdas :: TermSubst a => Int -> (a -> Term -> Term) -> a -> Term -> Term
    underLambdas :: forall a.
    TermSubst a =>
    Nat -> (a -> Term -> Term) -> a -> Term -> Term
    underLambdas Nat
    n a -> Term -> Term
    cont = Nat -> a -> Term -> Term
    loop Nat
    n where
      loop :: Nat -> a -> Term -> Term
    loop Nat
    0 a
    a = a -> Term -> Term
    cont a
    a
      loop Nat
    n a
    a = \case
        Lam ArgInfo
    h Abs Term
    b -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    h (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ (a -> Term -> Term) -> a -> Abs Term -> Abs Term
    forall a b. Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
    underAbs (Nat -> a -> Term -> Term
    loop (Nat -> a -> Term -> Term) -> Nat -> a -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1) a
    a Abs Term
    b
        Term
    _       -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__