1 files changed, 7 insertions, 1 deletions
diff --git a/src/AST.hs b/src/AST.hs
index e39c74f..9ee2405 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE EmptyCase #-}
 module AST (module AST, module AST.Weaken) where
 
 import Data.Functor.Const
@@ -76,7 +77,7 @@ deriving instance Show (SScalTy t)
 
 type TIx = TScal TI64
 
-type Idx :: [Ty] -> Ty -> Type
+type Idx :: [k] -> k -> Type
 data Idx env t where
   IZ :: Idx (t : env) t
   IS :: Idx env t -> Idx (a : env) t
@@ -276,6 +277,11 @@ slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list
 slistMap _ SNil = SNil
 slistMap f (SCons x list) = SCons (f x) (slistMap f list)
 
+slistIdx :: SList f list -> Idx list t -> f t
+slistIdx (SCons x _) IZ = x
+slistIdx (SCons _ list) (IS i) = slistIdx list i
+slistIdx SNil i = case i of {}
+
 idx2int :: Idx env t -> Int
 idx2int IZ = 0
 idx2int (IS n) = 1 + idx2int n