Need to pToV when making metavariables

or we get name clashes, and the typechecker gets confused when resolving names

darcs-hash:20081217140825-228f4-2381e9de2db166d4b25a0c59180baaf8425005f2.gz

Ivor/Typecheck.lhs

@@ -185,7 +185,7 @@ Return a list of the functions we need to define to complete the definition.
 >       then return (v1',t1',v2',t2',e'', [])
 >       else do let (Ind v2tt) = v2' 
 >               let (v2'', newdefs) = updateMetas v2tt
->               return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)
+>               trace (show newdefs) $ return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)
 
                if (null newdefs) then 
                   else trace (traceConstraints bs') $ return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, Ind y)) newdefs)
@@ -409,12 +409,15 @@ the expected type.
 >          -- Abstract it over the environment so that we have everything
 >          -- in scope we need.
 >          tm <- abstractOver (orderEnv env) n exp []
->          return (tm,Ind exp)
+>          trace (show tm ++ " : " ++ show exp) $ return (tm,Ind exp)
 > --              fail $ show (n, exp, bindings, env) ++ " -- Not implemented"
 >    where abstractOver [] mv exp args =
 >              return (Ind (appArgs (Meta mv exp) args))
 >          abstractOver ((n,B _ t):ns) mv exp args =
->              abstractOver ns mv (Bind n (B Pi t) (Sc exp)) ((P n):args)
+>              abstractOver ns mv (Bind n (B Pi t) (pToV n exp)) ((P n):args)
+
+          mkn (UN n) = MN (n,0)
+          mkn (MN (n,x)) = MN (n,x+1)
 
 >  tc env lvl (RMeta n) Nothing 
 >         -- just invent a name for it and see what inference gives us

Ivor/Unify.lhs

@@ -96,7 +96,7 @@ Collect names which do unify, and ignore errors
 >                   do acc' <- un envl envr f f' acc
 >                      un envl envr s s' acc'
 >              | otherwise = if ignore then return acc
->                               else fail $ "Can't unify "++show x++" and "++show y -- ++ " 5"
+>                               else fail $ "Can't unify "++show x++" and "++show y
 >             where funify (P x) (P y)
 >                       | x==y = True
 >                       | otherwise = hole envl x || hole envl y
@@ -125,7 +125,7 @@ Collect names which do unify, and ignore errors
 >          unbb envl envr (Guess v) (Guess v') acc = un envl envr v v' acc
 >          unbb envl envr x y acc
 >                   = if ignore then return acc
->                        else fail $ "Can't unify "++show x++" and "++show y -- ++ " 2"
+>                        else fail $ "Can't unify "++show x++" and "++show y
 
 >          unst envl envr (Quote x) (Quote y) acc = un envl envr x y acc
 >          unst envl envr (Code x) (Code y) acc = un envl envr x y acc
@@ -134,7 +134,7 @@ Collect names which do unify, and ignore errors
 >          unst envl envr x y acc =
 >                   if ignore then return acc
 >                       else fail $ "Can't unify " ++ show (Stage x) ++
->                                " and " ++ show (Stage y) -- ++ " 3"
+>                                " and " ++ show (Stage y)
 
 >          hole env x | (Just (B Hole ty)) <- lookup x env = True
 >                     | otherwise = isInferred x
@@ -147,7 +147,7 @@ Collect names which do unify, and ignore errors
 >                  = if (ueq tm tm')  -- Take account of names! == no good.
 >                       then checkAcc xs
 >                       else fail $ "Can't unify " ++ show tm ++
->                                   " and " ++ show tm' -- ++ " 4"
+>                                   " and " ++ show tm'
 >              | otherwise = checkAcc xs
 
 >          loc x xs = loc' 0 x xs