{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_HADDOCK hide #-}
module Rebound.Env.Lazy where

-- "Defunctionalized" representation of environment
-- stored values are lazy
-- *rest* of the environment is strict
-- Includes optimized composition (Inc and Cons cancel)
-- Includes Wadler's optimizations for the empty environment

import Rebound.Lib
import Data.Fin (Fin(..))
import qualified Data.Fin as Fin
import GHC.Generics hiding (S)
import Control.DeepSeq (NFData (..))

------------------------------------------------------------------------------
-- Substitution class declarations
------------------------------------------------------------------------------
-- | Well-scoped types that can be the range of
-- an environment. This should generally be the @Var@
-- constructor from the syntax.
class (Subst v v) => SubstVar (v :: Nat -> Type) where
  var :: Fin n -> v n

-- | Apply the environment throughout a term of
-- type `c n`, replacing variables with values
-- of type `v m`
class (SubstVar v) => Subst v c where
  applyE :: Env v n m -> c n -> c m
  default applyE :: (Generic1 c, GSubst v (Rep1 c), SubstVar v) => Env v m n -> c m -> c n
  applyE = Env v m n -> c m -> c n
forall (c :: Nat -> *) (v :: Nat -> *) (m :: Nat) (n :: Nat).
(Generic1 c, GSubst v (Rep1 c), Subst v c) =>
Env v m n -> c m -> c n
gapplyE
  {-# INLINE applyE #-}
  isVar :: c n -> Maybe (v :~: c, Fin n)
  isVar c n
_ = Maybe (v :~: c, Fin n)
forall a. Maybe a
Nothing
  {-# INLINE isVar #-}

-- | Generic programming variant of 'applyE'.
gapplyE :: forall c v m n. (Generic1 c, GSubst v (Rep1 c), Subst v c) => Env v m n -> c m -> c n
gapplyE :: forall (c :: Nat -> *) (v :: Nat -> *) (m :: Nat) (n :: Nat).
(Generic1 c, GSubst v (Rep1 c), Subst v c) =>
Env v m n -> c m -> c n
gapplyE Env v m n
r c m
e | Just (v :~: c
Refl, Fin m
x) <- forall (v :: Nat -> *) (c :: Nat -> *) (n :: Nat).
Subst v c =>
c n -> Maybe (v :~: c, Fin n)
isVar @v @c c m
e = Env c m n -> Fin m -> c n
forall (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar a =>
Env a n m -> Fin n -> a m
applyEnv Env c m n
Env v m n
r Fin m
x
gapplyE Env v m n
r c m
e = (Env v m n -> c m -> c n) -> Env v m n -> c m -> c n
forall (v :: Nat -> *) (n :: Nat) (m :: Nat) (c :: Nat -> *).
(Env v n m -> c n -> c m) -> Env v n m -> c n -> c m
applyOpt (\Env v m n
s c m
x -> Rep1 c n -> c n
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
forall (a :: Nat). Rep1 c a -> c a
to1 (Rep1 c n -> c n) -> Rep1 c n -> c n
forall a b. (a -> b) -> a -> b
$ Env v m n -> Rep1 c m -> Rep1 c n
forall (m :: Nat) (n :: Nat). Env v m n -> Rep1 c m -> Rep1 c n
forall (v :: Nat -> *) (e :: Nat -> *) (m :: Nat) (n :: Nat).
GSubst v e =>
Env v m n -> e m -> e n
gsubst Env v m n
s (c m -> Rep1 c m
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
forall (a :: Nat). c a -> Rep1 c a
from1 c m
x)) Env v m n
r c m
e
{-# INLINEABLE gapplyE #-}

-- | Generic programming support for 'Subst'.
class GSubst v (e :: Nat -> Type) where
  gsubst :: Env v m n -> e m -> e n


------------------------------------------------------------------------------
-- Environment representation
------------------------------------------------------------------------------

-- | Maps variables in scope @n@ to terms (of type @a@) in scope @m@.
data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where
  Zero  :: Env a Z n
  WeakR :: (SNat m) -> Env a n (n + m) --  weaken values in range by m
  Weak  :: (SNat m) -> Env a n (m + n) --  weaken values in range by m
  Inc   :: (SNat m) -> Env a n (m + n) --  increment values in range (shift) by m
  Cons  :: (a m) -> (Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)
  (:<>) :: (Env a m n) -> (Env a n p) -> Env a m p --  compose substitutions


instance (forall n. NFData (a n)) => NFData (Env a n m) where
  rnf :: Env a n m -> ()
rnf Env a n m
Zero = ()
  rnf (WeakR SNat m
m) = SNat m -> ()
forall a. NFData a => a -> ()
rnf SNat m
m
  rnf (Weak SNat m
m) = SNat m -> ()
forall a. NFData a => a -> ()
rnf SNat m
m
  rnf (Inc SNat m
m) = SNat m -> ()
forall a. NFData a => a -> ()
rnf SNat m
m
  rnf (Cons a m
x Env a n m
r) = a m -> ()
forall a. NFData a => a -> ()
rnf a m
x () -> () -> ()
forall a b. a -> b -> b
`seq` Env a n m -> ()
forall a. NFData a => a -> ()
rnf Env a n m
r
  rnf (Env a n n
r1 :<> Env a n m
r2) = Env a n n -> ()
forall a. NFData a => a -> ()
rnf Env a n n
r1 () -> () -> ()
forall a b. a -> b -> b
`seq` Env a n m -> ()
forall a. NFData a => a -> ()
rnf Env a n m
r2

------------------------------------------------------------------------------
-- Application
------------------------------------------------------------------------------

-- | Value of the index x in the substitution s

applyEnv :: SubstVar a => Env a n m -> Fin n -> a m
applyEnv :: forall (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar a =>
Env a n m -> Fin n -> a m
applyEnv Env a n m
Zero Fin n
x = Fin 'Z -> a m
forall b. Fin 'Z -> b
Fin.absurd Fin n
Fin 'Z
x
applyEnv (Inc SNat m
m) Fin n
x = Fin m -> a m
forall (n :: Nat). Fin n -> a n
forall (v :: Nat -> *) (n :: Nat). SubstVar v => Fin n -> v n
var (SNat m -> Fin n -> Fin (m + n)
forall (n :: Nat) (m :: Nat). SNat n -> Fin m -> Fin (n + m)
Fin.shiftN SNat m
m Fin n
x)
applyEnv (WeakR SNat m
m) Fin n
x = Fin m -> a m
forall (n :: Nat). Fin n -> a n
forall (v :: Nat -> *) (n :: Nat). SubstVar v => Fin n -> v n
var (SNat m -> Fin n -> Fin (n + m)
forall (proxy :: Nat -> *) (m :: Nat) (n :: Nat).
proxy m -> Fin n -> Fin (n + m)
Fin.weakenFinRight SNat m
m Fin n
x)
applyEnv (Weak SNat m
m) Fin n
x = Fin m -> a m
forall (n :: Nat). Fin n -> a n
forall (v :: Nat -> *) (n :: Nat). SubstVar v => Fin n -> v n
var (SNat m -> Fin n -> Fin (m + n)
forall (proxy :: Nat -> *) (m :: Nat) (n :: Nat).
proxy m -> Fin n -> Fin (m + n)
Fin.weakenFin SNat m
m Fin n
x)
applyEnv (Cons a m
ty Env a n m
_s) Fin n
FZ = a m
ty
applyEnv (Cons a m
_ty Env a n m
s) (FS Fin n1
x) = Env a n m -> Fin n -> a m
forall (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar a =>
Env a n m -> Fin n -> a m
applyEnv Env a n m
s Fin n
Fin n1
x
applyEnv (Env a n n
s1 :<> Env a n m
s2) Fin n
x = Env a n m -> a n -> a m
forall (n :: Nat) (m :: Nat). Env a n m -> a n -> a m
forall (v :: Nat -> *) (c :: Nat -> *) (n :: Nat) (m :: Nat).
Subst v c =>
Env v n m -> c n -> c m
applyE Env a n m
s2 (Env a n n -> Fin n -> a n
forall (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar a =>
Env a n m -> Fin n -> a m
applyEnv Env a n n
s1 Fin n
x)
{-# INLINEABLE applyEnv #-}

-- | Build an optimized version of applyE.
-- Checks to see if we are applying the identity substitution first.
applyOpt :: (Env v n m -> c n -> c m) -> (Env v n m -> c n -> c m)
applyOpt :: forall (v :: Nat -> *) (n :: Nat) (m :: Nat) (c :: Nat -> *).
(Env v n m -> c n -> c m) -> Env v n m -> c n -> c m
applyOpt Env v n m -> c n -> c m
f (Inc SNat m
SZ) c n
x = c n
c m
x
applyOpt Env v n m -> c n -> c m
f (Weak SNat m
SZ) c n
x = c n
c m
x
applyOpt Env v n m -> c n -> c m
f (WeakR SNat m
SZ) (c n
x :: c m) =
  case forall (m :: Nat). (m + 'Z) :~: m
axiomPlusZ @m of (n + 'Z) :~: n
Refl -> c n
c m
x
applyOpt Env v n m -> c n -> c m
f Env v n m
r c n
x = Env v n m -> c n -> c m
f Env v n m
r c n
x
{-# INLINEABLE applyOpt #-}

------------------------------------------------------------------------------
-- Construction and modification
------------------------------------------------------------------------------

-- | The empty environment (zero domain)
zeroE :: Env v Z n
zeroE :: forall (v :: Nat -> *) (n :: Nat). Env v 'Z n
zeroE = Env v 'Z n
forall (v :: Nat -> *) (n :: Nat). Env v 'Z n
Zero
{-# INLINEABLE zeroE #-}

-- | Increase the bound on free variables (on the right), without changing any free variable.
weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)
weakenER :: forall (m :: Nat) (v :: Nat -> *) (n :: Nat).
SubstVar v =>
SNat m -> Env v n (n + m)
weakenER = SNat m -> Env v n (n + m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
WeakR
{-# INLINEABLE weakenER #-}

-- | Increase the bound on free variables (on the left), without changing any free variable.
weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)
weakenE' :: forall (m :: Nat) (v :: Nat -> *) (n :: Nat).
SubstVar v =>
SNat m -> Env v n (m + n)
weakenE' = SNat m -> Env v n (m + n)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Weak
{-# INLINEABLE weakenE' #-}

-- | Shift the term, increasing every free variable as well as the bound by the provided amount.
shiftNE :: (SubstVar v) => (SubstVar v) => SNat m -> Env v n (m + n)
shiftNE :: forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
(SubstVar v, SubstVar v) =>
SNat m -> Env v n (m + n)
shiftNE = SNat m -> Env v n (m + n)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Inc
{-# INLINEABLE shiftNE #-}

-- | @cons@ an environment, adding a new mapping
-- for index '0'. All keys are shifted over.
(.:) :: v m -> Env v n m -> Env v (S n) m
.: :: forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
v m -> Env v n m -> Env v ('S n) m
(.:) = v m -> Env v n m -> Env v ('S n) m
forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
v m -> Env v n m -> Env v ('S n) m
Cons
{-# INLINEABLE (.:) #-}

-- | @uncons@ an environment, removing the mapping for index '0'.
-- All other keys are shifted back.
tail :: (SubstVar v) => Env v (S n) m -> Env v n m
tail :: forall (v :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar v =>
Env v ('S n) m -> Env v n m
tail Env v ('S n) m
x = SNat N1 -> Env v n (N1 + n)
forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
(SubstVar v, SubstVar v) =>
SNat m -> Env v n (m + n)
shiftNE SNat N1
s1 Env v n ('S n) -> Env v ('S n) m -> Env v n m
forall (v :: Nat -> *) (p :: Nat) (n :: Nat) (m :: Nat).
Subst v v =>
Env v p n -> Env v n m -> Env v p m
.>> Env v ('S n) m
x
{-# INLINEABLE tail #-}

-- | Compose two environments, applying them in sequence (left then right).
-- Some optimizations will be applied to optimize the resulting environment.
(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m
.>> :: forall (v :: Nat -> *) (p :: Nat) (n :: Nat) (m :: Nat).
Subst v v =>
Env v p n -> Env v n m -> Env v p m
(.>>) = Env v p n -> Env v n m -> Env v p m
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp
{-# INLINEABLE (.>>) #-}

-- | Compose two environments, applying them in sequence (left then right).
-- Some optimizations will be applied to optimize the resulting environment.
--
-- Some of the applied optimizations are:
-- - Identity environments (e.g., @'shiftNE' SZ@) are eliminated
-- - Absorbing environments on the right (i.e., 'zeroE') are eliminated
-- - Compatible environments are fused (e.g., @'weakenER' n@ and @'weakenER' m)
comp :: forall a m n p. SubstVar a =>
         Env a m n -> Env a n p -> Env a m p
comp :: forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp Env a m n
Zero Env a n p
s = Env a m p
Env a 'Z p
forall (v :: Nat -> *) (n :: Nat). Env v 'Z n
Zero
comp (Weak (SNat m
k1 :: SNat m1)) (Weak (SNat m
k2 :: SNat m2))  =
  case forall (p :: Nat) (m :: Nat) (n :: Nat).
(p + (m + n)) :~: ((p + m) + n)
axiomAssoc @m2 @m1 @m of
    (m + (m + m)) :~: ((m + m) + m)
Refl -> SNat (Plus m m) -> Env a m (Plus m m + m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Weak (SNat m -> SNat m -> SNat (m + m)
forall (n1 :: Nat) (n2 :: Nat).
SNat n1 -> SNat n2 -> SNat (n1 + n2)
sPlus SNat m
k2 SNat m
k1)
comp (Weak SNat m
SZ) Env a n p
s = Env a m p
Env a n p
s
comp Env a m n
s (Weak SNat m
SZ) = Env a m n
Env a m p
s
comp (WeakR (SNat m
k1 :: SNat m1)) (WeakR (SNat m
k2 :: SNat m2))  =
  case forall (p :: Nat) (m :: Nat) (n :: Nat).
(p + (m + n)) :~: ((p + m) + n)
axiomAssoc @m @m1 @m2 of
    (m + (m + m)) :~: ((m + m) + m)
Refl -> SNat (Plus m m) -> Env a m (m + Plus m m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
WeakR (SNat m -> SNat m -> SNat (m + m)
forall (n1 :: Nat) (n2 :: Nat).
SNat n1 -> SNat n2 -> SNat (n1 + n2)
sPlus SNat m
k1 SNat m
k2)
comp (WeakR SNat m
SZ) Env a n p
s =
  case forall (m :: Nat). (m + 'Z) :~: m
axiomPlusZ @m of
    (m + 'Z) :~: m
Refl -> Env a m p
Env a n p
s
comp Env a m n
s (WeakR SNat m
SZ) =
  case forall (m :: Nat). (m + 'Z) :~: m
axiomPlusZ @n of
    (n + 'Z) :~: n
Refl -> Env a m n
Env a m p
s
comp (Inc (SNat m
k1 :: SNat m1)) (Inc (SNat m
k2 :: SNat m2))  =
  case forall (p :: Nat) (m :: Nat) (n :: Nat).
(p + (m + n)) :~: ((p + m) + n)
axiomAssoc @m2 @m1 @m of
    (m + (m + m)) :~: ((m + m) + m)
Refl -> SNat (Plus m m) -> Env a m (Plus m m + m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Inc (SNat m -> SNat m -> SNat (m + m)
forall (n1 :: Nat) (n2 :: Nat).
SNat n1 -> SNat n2 -> SNat (n1 + n2)
sPlus SNat m
k2 SNat m
k1)
comp Env a m n
s (Inc SNat m
SZ) = Env a m n
Env a m p
s
comp (Inc SNat m
SZ) Env a n p
s = Env a m p
Env a n p
s
comp (Inc (SNat m -> SNat_ m
forall (n :: Nat). SNat n -> SNat_ n
snat_ -> SS_ SNat n1
p1)) (Cons a p
_t Env a n p
p) = Env a m n -> Env a n p -> Env a m p
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp (SNat n1 -> Env a m (n1 + m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Inc SNat n1
p1) Env a n p
p
comp (Env a m n
s1 :<> Env a n n
s2) Env a n p
s3 = Env a m n -> Env a n p -> Env a m p
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp Env a m n
s1 (Env a n n -> Env a n p -> Env a n p
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp Env a n n
s2 Env a n p
s3)
comp (Cons a n
t Env a n n
s1) Env a n p
s2 = a p -> Env a n p -> Env a ('S n) p
forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
v m -> Env v n m -> Env v ('S n) m
Cons (Env a n p -> a n -> a p
forall (n :: Nat) (m :: Nat). Env a n m -> a n -> a m
forall (v :: Nat -> *) (c :: Nat -> *) (n :: Nat) (m :: Nat).
Subst v c =>
Env v n m -> c n -> c m
applyE Env a n p
s2 a n
t) (Env a n n -> Env a n p -> Env a n p
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp Env a n n
s1 Env a n p
s2)
comp Env a m n
s1 Env a n p
s2 = Env a m n
s1 Env a m n -> Env a n p -> Env a m p
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
Env a m n -> Env a n p -> Env a m p
:<> Env a n p
s2
{-# INLINEABLE comp #-}

-- | Adapt an environment to go under a binder.
up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)
up :: forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
SubstVar v =>
Env v m n -> Env v ('S m) ('S n)
up (Inc SNat m
SZ) = SNat 'Z -> Env v ('S m) ('Z + 'S m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Inc SNat 'Z
SZ
up (Weak SNat m
SZ) = SNat 'Z -> Env v ('S m) ('Z + 'S m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Weak SNat 'Z
SZ
up (WeakR SNat m
SZ) = SNat 'Z -> Env v ('S m) ('S m + 'Z)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
WeakR SNat 'Z
SZ
up Env v m n
e = Fin ('S n) -> v ('S n)
forall (n :: Nat). Fin n -> v n
forall (v :: Nat -> *) (n :: Nat). SubstVar v => Fin n -> v n
var Fin ('S n)
forall (n :: Nat). Fin ('S n)
Fin.f0 v ('S n) -> Env v m ('S n) -> Env v ('S m) ('S n)
forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
v m -> Env v n m -> Env v ('S n) m
.: Env v m n -> Env v n ('S n) -> Env v m ('S n)
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
SubstVar a =>
Env a m n -> Env a n p -> Env a m p
comp Env v m n
e (SNat N1 -> Env v n (N1 + n)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Inc SNat N1
s1)
{-# INLINEABLE up #-}

-- | Map the range of an environment. Has to preserve the scope of the range.
transform :: (SubstVar b) => (forall m. a m -> b m) -> Env a n m -> Env b n m
transform :: forall (b :: Nat -> *) (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar b =>
(forall (m :: Nat). a m -> b m) -> Env a n m -> Env b n m
transform forall (m :: Nat). a m -> b m
f Env a n m
Zero = Env b n m
Env b 'Z m
forall (v :: Nat -> *) (n :: Nat). Env v 'Z n
Zero
transform forall (m :: Nat). a m -> b m
f (Weak SNat m
x) = SNat m -> Env b n (m + n)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Weak SNat m
x
transform forall (m :: Nat). a m -> b m
f (WeakR SNat m
x) = SNat m -> Env b n (n + m)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
WeakR SNat m
x
transform forall (m :: Nat). a m -> b m
f (Inc SNat m
x) = SNat m -> Env b n (m + n)
forall (n :: Nat) (a :: Nat -> *) (n :: Nat).
SNat n -> Env a n (n + n)
Inc SNat m
x
transform forall (m :: Nat). a m -> b m
f (Cons a m
a Env a n m
r) = b m -> Env b n m -> Env b ('S n) m
forall (v :: Nat -> *) (m :: Nat) (n :: Nat).
v m -> Env v n m -> Env v ('S n) m
Cons (a m -> b m
forall (m :: Nat). a m -> b m
f a m
a) ((forall (m :: Nat). a m -> b m) -> Env a n m -> Env b n m
forall (b :: Nat -> *) (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar b =>
(forall (m :: Nat). a m -> b m) -> Env a n m -> Env b n m
transform a m -> b m
forall (m :: Nat). a m -> b m
f Env a n m
r)
transform forall (m :: Nat). a m -> b m
f (Env a n n
r1 :<> Env a n m
r2) = (forall (m :: Nat). a m -> b m) -> Env a n n -> Env b n n
forall (b :: Nat -> *) (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar b =>
(forall (m :: Nat). a m -> b m) -> Env a n m -> Env b n m
transform a m -> b m
forall (m :: Nat). a m -> b m
f Env a n n
r1 Env b n n -> Env b n m -> Env b n m
forall (a :: Nat -> *) (m :: Nat) (n :: Nat) (p :: Nat).
Env a m n -> Env a n p -> Env a m p
:<> (forall (m :: Nat). a m -> b m) -> Env a n m -> Env b n m
forall (b :: Nat -> *) (a :: Nat -> *) (n :: Nat) (m :: Nat).
SubstVar b =>
(forall (m :: Nat). a m -> b m) -> Env a n m -> Env b n m
transform a m -> b m
forall (m :: Nat). a m -> b m
f Env a n m
r2