From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 13 Apr 2015 21:33:52 +0000 (+0200)
Subject: Fix bug in Resolver
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=543b51c27a453d8a9b97fa4f15b3cea1d6485398;p=cubicaltt.git

Fix bug in Resolver
---

diff --git a/Resolver.hs b/Resolver.hs
index 76ec78f..5cb5ddc 100644
--- 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)])