    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Substitute.Class where

    import Control.Arrow ((***), second)
    import Control.DeepSeq
    import GHC.Generics

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

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

    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) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    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 ]

    -- | Apply to two default arguments.
    apply2 :: Apply t => t -> Term -> Term -> t
    apply2 :: forall t. Apply t => t -> Term -> Term -> t
    apply2 t
    t Term
    u Term
    v = t -> [Term] -> t
    forall t. Apply t => t -> [Term] -> t
    applys t
    t [Term
    u, Term
    v]

    ---------------------------------------------------------------------------
    -- * 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 a b. (a -> b) -> f a -> 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 -> Nat -> Substitution' (SubstArg a)
    forall a. Impossible -> Nat -> Substitution' a
    strengthenS Impossible
    err Nat
    1)

    -- | 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))

    -- | Checks whether the variable bound by the abstraction is actually
    -- used, and, if /not/, returns the term within, 'strengthen'ed to live in
    -- the context /outside/ the abstraction.
    -- See also 'Agda.TypeChecking.Free.isBinderUsed'.
    isNoAbs :: (Free a, Subst a) => Abs a -> Maybe a
    isNoAbs :: forall a. (Free a, Subst a) => Abs a -> Maybe a
    isNoAbs (NoAbs ArgName
    _ a
    b) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    b
    isNoAbs (Abs ArgName
    _ a
    b)
      | Bool -> Bool
    not (Nat
    0 Nat -> a -> Bool
    forall a. Free a => Nat -> a -> Bool
    `freeIn` a
    b) = a -> Maybe a
    forall a. a -> Maybe a
    Just (Impossible -> a -> a
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ a
    b)
      | Bool
    otherwise          = Maybe a
    forall a. Maybe a
    Nothing

    -- ** Identity instances

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

    -- | Wrapper for types that do not contain variables (so applying a substitution is the identity).
    --   Useful if you have a structure of types that support substitution mixed with types that don't
    --   and need to apply a substitution to the full structure.
    newtype NoSubst t a = NoSubst { forall t a. NoSubst t a -> a
    unNoSubst :: a }
      deriving ((forall x. NoSubst t a -> Rep (NoSubst t a) x)
    -> (forall x. Rep (NoSubst t a) x -> NoSubst t a)
    -> Generic (NoSubst t a)
    forall x. Rep (NoSubst t a) x -> NoSubst t a
    forall x. NoSubst t a -> Rep (NoSubst t a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall t a x. Rep (NoSubst t a) x -> NoSubst t a
    forall t a x. NoSubst t a -> Rep (NoSubst t a) x
    $cfrom :: forall t a x. NoSubst t a -> Rep (NoSubst t a) x
    from :: forall x. NoSubst t a -> Rep (NoSubst t a) x
    $cto :: forall t a x. Rep (NoSubst t a) x -> NoSubst t a
    to :: forall x. Rep (NoSubst t a) x -> NoSubst t a
    Generic, NoSubst t a -> ()
    (NoSubst t a -> ()) -> NFData (NoSubst t a)
    forall a. (a -> ()) -> NFData a
    forall t a. NFData a => NoSubst t a -> ()
    $crnf :: forall t a. NFData a => NoSubst t a -> ()
    rnf :: NoSubst t a -> ()
    NFData, (forall a b. (a -> b) -> NoSubst t a -> NoSubst t b)
    -> (forall a b. a -> NoSubst t b -> NoSubst t a)
    -> Functor (NoSubst t)
    forall a b. a -> NoSubst t b -> NoSubst t a
    forall a b. (a -> b) -> NoSubst t a -> NoSubst t b
    forall t a b. a -> NoSubst t b -> NoSubst t a
    forall t a b. (a -> b) -> NoSubst t a -> NoSubst t b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall t a b. (a -> b) -> NoSubst t a -> NoSubst t b
    fmap :: forall a b. (a -> b) -> NoSubst t a -> NoSubst t b
    $c<$ :: forall t a b. a -> NoSubst t b -> NoSubst t a
    <$ :: forall a b. a -> NoSubst t b -> NoSubst t a
    Functor)

    instance DeBruijn t => Subst (NoSubst t a) where
      type SubstArg (NoSubst t a) = t
      applySubst :: Substitution' (SubstArg (NoSubst t a))
    -> NoSubst t a -> NoSubst t a
    applySubst Substitution' (SubstArg (NoSubst t a))
    _ NoSubst t a
    x = NoSubst t a
    x

    ---------------------------------------------------------------------------
    -- * 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

    {-# INLINABLE consS #-}
    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
    forall a b. a -> b -> b
    seq a
    u (a
    u a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' a
    rho)
    {-# SPECIALIZE consS :: Term  -> Substitution' Term  -> Substitution' Term #-}
    {-# SPECIALIZE consS :: Level -> Substitution' Level -> Substitution' Level #-}

    {-# INLINABLE singletonS #-}
    -- | 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
    {-# SPECIALIZE singletonS :: Int -> Term -> Substitution' Term #-}
    {-# SPECIALIZE singletonS :: Int -> Level -> Substitution' Level #-}

    -- | 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 (EmptyS Impossible
    err)       = Impossible -> Substitution' a
    forall a. Impossible -> a
    throwImpossible Impossible
    err
    dropS Nat
    n (Lift Nat
    m Substitution' a
    rho)
      -- dropS n (Lift m rho) =
      --   wkS 1 $ dropS (n - 1) $ liftS (m - 1) rho
      | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    m     = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    m (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
    m) Substitution' a
    rho
      | Bool
    otherwise = Nat -> Substitution' a -> Substitution' a
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    n (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
    n) Substitution' a
    rho
    dropS Nat
    n (Strengthen Impossible
    err Nat
    m Substitution' a
    rho)
      | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    m     = Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) Substitution' a
    rho
      | Bool
    otherwise = 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
    m) Substitution' a
    rho

    {-# INLINABLE composeS #-}
    -- | @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 Nat
    n Substitution' a
    sgm) = Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Nat
    n (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 b c d. (b -> c) -> (d, b) -> (d, c)
    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 (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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    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__
    splitS Nat
    n (Strengthen Impossible
    err Nat
    m Substitution' a
    rho)
      -- splitS n (Strengthen err 1 rho) =
      --   second (Strengthen err) $ splitS (n - 1) rho
      | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    m     = (Substitution' a -> Substitution' a)
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err 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 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    m) Substitution' a
    rho
      | Bool
    otherwise = (Substitution' a -> Substitution' a)
    -> (Substitution' a, Substitution' a)
    -> (Substitution' a, Substitution' a)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Nat
    n) ((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
    0 (Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) Substitution' a
    rho)

    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 a b. (a -> b -> b) -> b -> [a] -> b
    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 = Nat -> [Maybe a] -> Substitution' a
    go Nat
    0 [Maybe a]
    us
      where
      -- The function strengthenS' is not used here, to avoid replacing
      -- the "error message" of a potential outermost Strengthen
      -- constructor in rho.
      str :: Nat -> Substitution' a -> Substitution' a
    str Nat
    0 = Substitution' a -> Substitution' a
    forall a. a -> a
    id
      str Nat
    n = Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Nat
    n

      go :: Nat -> [Maybe a] -> Substitution' a
    go !Nat
    n (Just a
    u  : [Maybe a]
    us) = Nat -> Substitution' a -> Substitution' a
    str Nat
    n (a -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS a
    u (Nat -> [Maybe a] -> Substitution' a
    go Nat
    0 [Maybe a]
    us))
      go  Nat
    n (Maybe a
    Nothing : [Maybe a]
    us) = Nat -> [Maybe a] -> Substitution' a
    go (Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n) [Maybe a]
    us
      go  Nat
    n []             = Nat -> Substitution' a -> Substitution' a
    str Nat
    n Substitution' a
    rho

    -- | @
    --        Γ ⊢ reverse vs : Δ
    --      -----------------------------
    --        Γ ⊢ parallelS vs ρ : Γ, Δ
    --   @
    --
    --   Note the @Γ@ in @Γ, Δ@.
    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

    -- | Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
    strengthenS :: Impossible -> Int -> Substitution' a
    strengthenS :: forall a. Impossible -> Nat -> Substitution' a
    strengthenS Impossible
    err Nat
    n = case Nat -> Nat -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Nat
    n Nat
    0 of
      Ordering
    LT -> Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Ordering
    EQ -> Substitution' a
    forall a. Substitution' a
    idS
      Ordering
    GT -> Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Nat
    n Substitution' a
    forall a. Substitution' a
    idS

    -- | A \"smart\" variant of 'Strengthen'. If 'strengthenS' is applied
    -- to a substitution with an outermost 'Strengthen' constructor, then
    -- the \"error message\" of that constructor is discarded in favour of
    -- the 'Impossible' argument of this function.
    strengthenS' :: Impossible -> Int -> Substitution' a -> Substitution' a
    strengthenS' :: forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    strengthenS' Impossible
    err Nat
    m Substitution' a
    rho = case Nat -> Nat -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Nat
    m Nat
    0 of
      Ordering
    LT -> Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Ordering
    EQ -> Substitution' a
    rho
      Ordering
    GT -> case Substitution' a
    rho of
        Strengthen Impossible
    _ Nat
    n Substitution' a
    rho -> Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n) Substitution' a
    rho
        Substitution' a
    _                  -> Impossible -> Nat -> Substitution' a -> Substitution' a
    forall a. Impossible -> Nat -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Nat
    m       Substitution' a
    rho

    {-# INLINABLE lookupS #-}
    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 Nat
    n Substitution' a
    rho
                 | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    0     -> a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                 | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n     -> Impossible -> a
    forall a. Impossible -> a
    throwImpossible Impossible
    err
                 | 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
    n)
      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