Fix bug in Resolver

diff --git a/Resolver.hs b/Resolver.hs
index 76ec78fd302a241275f1d5c8e6a3b7a20b881933..5cb5ddc8dd9faa4595f34b6b615c0f2e71f7ca63 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -264,10 +264,12 @@ resolveTele ((i,d):t) =
 resolveLabel :: [(Ident,SymKind)] -> Label -> Resolver CTT.Label
 resolveLabel _ (OLabel n vdecl) =
   CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
-resolveLabel cs (PLabel n vdecl t0 t1) =
-  CTT.PLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
-                          <*> local (insertIdents cs) (resolveExp t0)
-                          <*> local (insertIdents cs) (resolveExp t1)
+resolveLabel cs (PLabel n vdecl t0 t1) = do
+  let tele' = flattenTele vdecl
+      ts = map fst tele'
+  CTT.PLabel (unAIdent n) <$> resolveTele tele'
+                          <*> local (insertIdents cs . insertVars ts) (resolveExp t0)
+                          <*> local (insertIdents cs . insertVars ts) (resolveExp t1)
 
 -- Resolve Data or Def or Split declarations
 resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])