1 files changed, 36 insertions, 22 deletions

diff --git a/src/AST/Env.hs b/src/AST/Env.hs
index 4f34166..bc2b9e0 100644
--- a/src/AST/Env.hs
+++ b/src/AST/Env.hs
@@ -1,59 +1,73 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeOperators #-}
 module AST.Env where
 
+import Data.Type.Equality
+
+import AST.Sparse
 import AST.Weaken
 import Data
 
 
 -- | @env'@ is a subset of @env@: each element of @env@ is either included in
 -- @env'@ ('SEYes') or not included in @env'@ ('SENo').
-data Subenv env env' where
-  SETop :: Subenv '[] '[]
-  SEYes :: forall t env env'. Subenv env env' -> Subenv (t : env) (t : env')
-  SENo  :: forall t env env'. Subenv env env' -> Subenv (t : env) env'
-deriving instance Show (Subenv env env')
+data Subenv' s env env' where
+  SETop :: Subenv' s '[] '[]
+  SEYes :: forall t t' env env' s. s t t' -> Subenv' s env env' -> Subenv' s (t : env) (t' : env')
+  SENo  :: forall t env env' s. Subenv' s env env' -> Subenv' s (t : env) env'
+deriving instance (forall t t'. Show (s t t')) => Show (Subenv' s env env')
+
+type Subenv = Subenv' (:~:)
+type SubenvS = Subenv' Sparse
+
+pattern SEYesR :: forall tenv tenv'. ()
+               => forall t env env'. (tenv ~ t : env, tenv' ~ t : env')
+               => Subenv env env' -> Subenv tenv tenv'
+pattern SEYesR s = SEYes Refl s
+
+{-# COMPLETE SETop, SEYesR, SENo #-}
 
-subList :: SList f env -> Subenv env env' -> SList f env'
+subList :: (IsSubType s, IsSubTypeSubject s f) => SList f env -> Subenv' s env env' -> SList f env'
 subList SNil SETop = SNil
-subList (SCons x xs) (SEYes sub) = SCons x (subList xs sub)
+subList (SCons x xs) (SEYes s sub) = SCons (subtApply s x) (subList xs sub)
 subList (SCons _ xs) (SENo sub) = subList xs sub
 
-subenvAll :: SList f env -> Subenv env env
+subenvAll :: IsSubType s => SList f env -> Subenv' s env env
 subenvAll SNil = SETop
-subenvAll (SCons _ env) = SEYes (subenvAll env)
+subenvAll (SCons _ env) = SEYes subtFull (subenvAll env)
 
-subenvNone :: SList f env -> Subenv env '[]
+subenvNone :: SList f env -> Subenv' s env '[]
 subenvNone SNil = SETop
 subenvNone (SCons _ env) = SENo (subenvNone env)
 
-subenvOnehot :: SList f env -> Idx env t -> Subenv env '[t]
-subenvOnehot (SCons _ env) IZ = SEYes (subenvNone env)
+subenvOnehot :: IsSubType s => SList f env -> Idx env t -> Subenv' s env '[t]
+subenvOnehot (SCons _ env) IZ = SEYes subtFull (subenvNone env)
 subenvOnehot (SCons _ env) (IS i) = SENo (subenvOnehot env i)
 subenvOnehot SNil i = case i of {}
 
-subenvCompose :: Subenv env1 env2 -> Subenv env2 env3 -> Subenv env1 env3
+subenvCompose :: IsSubType s => Subenv' s env1 env2 -> Subenv' s env2 env3 -> Subenv' s env1 env3
 subenvCompose SETop SETop = SETop
-subenvCompose (SEYes sub1) (SEYes sub2) = SEYes (subenvCompose sub1 sub2)
-subenvCompose (SEYes sub1) (SENo sub2) = SENo (subenvCompose sub1 sub2)
+subenvCompose (SEYes s1 sub1) (SEYes s2 sub2) = SEYes (subtTrans s1 s2) (subenvCompose sub1 sub2)
+subenvCompose (SEYes _ sub1) (SENo sub2) = SENo (subenvCompose sub1 sub2)
 subenvCompose (SENo sub1) sub2 = SENo (subenvCompose sub1 sub2)
 
-subenvConcat :: Subenv env1 env1' -> Subenv env2 env2' -> Subenv (Append env2 env1) (Append env2' env1')
+subenvConcat :: Subenv' s env1 env1' -> Subenv' s env2 env2' -> Subenv' s (Append env2 env1) (Append env2' env1')
 subenvConcat sub1 SETop = sub1
-subenvConcat sub1 (SEYes sub2) = SEYes (subenvConcat sub1 sub2)
+subenvConcat sub1 (SEYes s sub2) = SEYes s (subenvConcat sub1 sub2)
 subenvConcat sub1 (SENo sub2) = SENo (subenvConcat sub1 sub2)
 
-sinkWithSubenv :: Subenv env env' -> env0 :> Append env' env0
+sinkWithSubenv :: Subenv' s env env' -> env0 :> Append env' env0
 sinkWithSubenv SETop = WId
-sinkWithSubenv (SEYes sub) = WSink .> sinkWithSubenv sub
+sinkWithSubenv (SEYes _ sub) = WSink .> sinkWithSubenv sub
 sinkWithSubenv (SENo sub) = sinkWithSubenv sub
 
-wUndoSubenv :: Subenv env env' -> env' :> env
+wUndoSubenv :: Subenv' (:~:) env env' -> env' :> env
 wUndoSubenv SETop = WId
-wUndoSubenv (SEYes sub) = WCopy (wUndoSubenv sub)
+wUndoSubenv (SEYes Refl sub) = WCopy (wUndoSubenv sub)
 wUndoSubenv (SENo sub) = WSink .> wUndoSubenv sub