1 files changed, 7 insertions, 2 deletions
diff --git a/src/AST.hs b/src/AST.hs
index ed2039b..8dfea68 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -13,6 +13,7 @@
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 module AST (module AST, module AST.Types, module AST.Weaken) where
 
 import Data.Functor.Const
@@ -43,8 +44,12 @@ type family AcVal t i where
   AcVal (TPair a b) (S i) = TEither (AcVal a i) (AcVal b i)
   AcVal (TEither a b) (S i) = TEither (AcVal a i) (AcVal b i)
   AcVal (TMaybe t) (S i) = AcVal t i
-  AcVal (TArr Z t) (S i) = AcVal t i
-  AcVal (TArr (S n) t) (S i) = AcVal (TArr n t) i
+  AcVal (TArr n t) (S i) = TPair (Tup (Replicate n TIx)) (AcValArr n t (S i))
+
+type family AcValArr n t i where
+  AcValArr n t Z = TArr n t
+  AcValArr Z t (S i) = AcVal t i
+  AcValArr (S n) t (S i) = AcValArr n t i
 
 -- General assumption: head of the list (whatever way it is associated) is the
 -- inner variable / inner array dimension. In pretty printing, the inner