@@ -63,12 +63,16 @@ match_unify ctxt env topx topy inj holes =
6363 | holeIn env y || y `elem` holes
6464 = do sc 1; checkCycle names (y, tm)
6565 un bnames (V i) (P _ x _)
66− | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
66+ | length bnames > i,
67+ fst (fst (bnames!!i)) == x ||
68+ snd (fst (bnames!!i)) == x = do sc 1; return []
6769 un bnames (P _ x _) (V i)
68− | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
70+ | length bnames > i,
71+ fst (fst (bnames!!i)) == x ||
72+ snd (fst (bnames!!i)) == x = do sc 1; return []
6973 un bnames (Bind x bx sx) (Bind y by sy)
7074 = do h1 <- uB bnames bx by
71− h2 <- un ((x, y) : bnames) sx sy
75+ h2 <- un (((x, y), binderTy bx) : bnames) sx sy
7276 combine bnames h1 h2
7377 un names (App fx ax) (App fy ay)
7478 = do hf <- un names fx fy
@@ -126,12 +130,22 @@ match_unify ctxt env topx topy inj holes =
126130 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
127131
128132 checkScope ns (x, tm) =
129− case boundVs (envPos x 0 env) tm of
130− [] -> return [(x, tm)]
131− (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
132− (inst ns tm) (errEnv env))
133+-- case boundVs (envPos x 0 env) tm of
134+-- [] -> return [(x, tm)]
135+-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
136+-- (inst ns tm) (errEnv env))
137+ let v = highV (-1) tm in
138+ if v >= length ns
139+ then lift $ tfail (Msg "SCOPE ERROR")
140+ else return [(x, bind (highV (-1) tm) ns tm)]
133141 where inst [] tm = tm
134142 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
143+
144+ bind i ns tm
145+ | i < 0 = tm
146+ | otherwise = let ((x,y),ty) = ns!!i in
147+ App (Bind y (Lam ty) (bind (i-1) ns tm))
148+ (P Bound x ty)
135149
136150renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)
137151renameBinders env (x, tm) = (x, uniqueBinders tm)
@@ -225,7 +239,7 @@ unify ctxt env topx topy inj holes =
225239 then return r
226240 else do put (UI s f); u2
227241
228− un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
242+ un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
229243 StateT UInfo
230244 TC [(Name, TT Name)]
231245 un = un'
@@ -236,7 +250,7 @@ unify ctxt env topx topy inj holes =
236250-- uplus (un' fn names x y)
237251-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
238252
239− un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
253+ un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
240254 StateT UInfo
241255 TC [(Name, TT Name)]
242256 un' fn names x y | x == y = return [] -- shortcut
@@ -253,7 +267,7 @@ unify ctxt env topx topy inj holes =
253267 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
254268 = unifyFail topx topy
255269 un' fn bnames tx@(P _ x _) ty@(P _ y _)
256− | (x,y) `elem` bnames || x == y = do sc 1; return []
270+ | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
257271 | injective tx && not (holeIn env y || y `elem` holes)
258272 = unifyTmpFail tx ty
259273 | injective ty && not (holeIn env x || x `elem` holes)
@@ -287,9 +301,16 @@ unify ctxt env topx topy inj holes =
287301 = do checkCycle bnames (y, tm)
288302 unifyTmpFail tm ytm
289303 un' fn bnames (V i) (P _ x _)
290− | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
304+ | length bnames > i,
305+ fst ((map fst bnames)!!i) == x ||
306+ snd ((map fst bnames)!!i) == x = do sc 1; return []
291307 un' fn bnames (P _ x _) (V i)
292− | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
308+ | length bnames > i,
309+ fst ((map fst bnames)!!i) == x ||
310+ snd ((map fst bnames)!!i) == x = do sc 1; return []
311+
312+ un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
313+ un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
293314
294315 un' fn bnames appx@(App _ _) appy@(App _ _)
295316 = unApp fn bnames appx appy
@@ -327,9 +348,13 @@ unify ctxt env topx topy inj holes =
327348 combine bnames ux uf
328349
329350 un' fn bnames (Bind x bx sx) (Bind y by sy)
330− = do h1 <- uB bnames bx by
331− h2 <- un' False ((x,y):bnames) sx sy
332− combine bnames h1 h2
351+ | sameBinder bx by
352+ = do h1 <- uB bnames bx by
353+ h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
354+ combine bnames h1 h2
355+ where sameBinder (Lam _) (Lam _) = True
356+ sameBinder (Pi _) (Pi _) = True
357+ sameBinder _ _ = False
333358 un' fn bnames x y
334359 | OK True <- convEq' ctxt x y = do sc 1; return []
335360 | otherwise = do UI s f <- get
@@ -367,24 +392,7 @@ unify ctxt env topx topy inj holes =
367392 hf <- un' False bnames fx' fy'
368393 sc 1
369394 combine bnames hf ha)
370− | otherwise = -- FIXME: This fudge should be:
371− unifyTmpFail appx appy
372−-- do let (headx, argsx) = unApply appx
373−-- let (heady, argsy) = unApply appy
374−-- -- traceWhen (headx == heady) (show (appx, appy)) $
375−-- uplus (
376−-- if (length argsx == length argsy &&
377−-- ((headx == heady && inenv headx) || (argsx == argsy) ||
378−-- (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
379−-- then
380−-- -- (notFn headx && notFn heady))) then
381−-- do uf <- un' True bnames headx heady
382−-- failed <- errors
383−-- if (not failed) then unArgs uf argsx argsy
384−-- else return []
385−-- else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
386−-- unifyTmpFail appx appy)
387−-- (unifyTmpFail appx appy) -- whole application fails
395+ | otherwise = unifyTmpFail appx appy
388396 where hnormalise [] _ _ t = t
389397 hnormalise ns ctxt env t = normalise ctxt env t
390398 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
@@ -417,28 +425,6 @@ unify ctxt env topx topy inj holes =
417425 all (\x -> pat x || metavar x) (f : args)
418426 && nub args == args
419427
420− sameArgStruct appx appy
421− = let (_, ax) = unApply appx
422− (_, ay) = unApply appy in
423− length ax == length ay &&
424− and (zipWith sameStruct ax ay)
425−
426− sameStruct fapp@(App f x) gapp@(App g y)
427− = let (f',a') = unApply fapp
428− (g',b') = unApply gapp in
429− (f' == g' && length a' == length b' &&
430− (injective f' || injective g'))
431− || (sameStruct f g && sameStruct x y)
432− sameStruct (P _ x _) (P _ y _) = True
433− sameStruct (V i) (V j) = i == j
434− sameStruct (Constant x) (Constant y) = True
435− sameStruct (P _ _ _) (Constant y) = True
436− sameStruct (Constant x) (P _ _ _) = True
437− sameStruct (Bind n t sc) (P _ _ _) = True
438− sameStruct (P _ _ _) (Bind n t sc) = True
439− sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
440− sameStruct _ _ = False
441−
442428 rigid (P (DCon _ _) _ _) = True
443429 rigid (P (TCon _ _) _ _) = True
444430 rigid t@(P Ref _ _) = inenv t || globmetavar t
@@ -513,12 +499,22 @@ unify ctxt env topx topy inj holes =
513499 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
514500
515501 checkScope ns (x, tm) =
516− case boundVs (envPos x 0 env) tm of
517− [] -> return [(x, tm)]
518− (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
519− (inst ns tm) (errEnv env))
502+-- case boundVs (envPos x 0 env) tm of
503+-- [] -> return [(x, tm)]
504+-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
505+-- (inst ns tm) (errEnv env))
506+ let v = highV (-1) tm in
507+ if v >= length ns
508+ then lift $ tfail (Msg "SCOPE ERROR")
509+ else return [(x, bind (highV (-1) tm) ns tm)]
520510 where inst [] tm = tm
521− inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
511+ inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
512+
513+ bind i ns tm
514+ | i < 0 = tm
515+ | otherwise = let ((x,y),ty) = ns!!i in
516+ App (Bind y (Lam ty) (bind (i-1) ns tm))
517+ (P Bound x ty)
522518
523519 combineArgs bnames args = ca [] args where
524520 ca acc [] = return acc
@@ -536,7 +532,7 @@ unify ctxt env topx topy inj holes =
536532 combine bnames as (ns' ++ bs)
537533
538534boundVs :: Int -> Term -> [Int]
539−boundVs i (V j) | j <= i = []
535+boundVs i (V j) | j < i = []
540536 | otherwise = [j]
541537boundVs i (Bind n b sc) = boundVs (i + 1) sc
542538boundVs i (App f x) = let fs = boundVs i f
@@ -544,6 +540,13 @@ boundVs i (App f x) = let fs = boundVs i f
544540 nub (fs ++ xs)
545541boundVs i _ = []
546542
543+highV :: Int -> Term -> Int
544+highV i (V j) | j > i = j
545+ | otherwise = i
546+highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
547+highV i (App f x) = max (highV i f) (highV i x)
548+highV i _ = i
549+
547550envPos x i [] = 0
548551envPos x i ((y, _) : ys) | x == y = i
549552 | otherwise = envPos x (i + 1) ys