git.iko.soy/Idris-dev
on 85cf83f help sign in
Idris-dev/src/Idris/Core/Unify.hs
712 lines 31 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..),
4 unrecoverable) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
9import Control.Monad
10import Control.Monad.State.Strict
11import Data.List
12import Debug.Trace
14-- Unification is applied inside the theorem prover. We're looking for holes
15-- which can be filled in, by matching one term's normal form against another.
16-- Returns a list of hole names paired with the term which solves them, and
17-- a list of things which need to be injective.
19-- terms which need to be injective, with the things we're trying to unify
20-- at the time
22data FailAt = Match | Unify
23 deriving (Show, Eq)
25data FailContext = FailContext { fail_sourceloc :: FC,
26 fail_fn :: Name,
27 fail_param :: Name
28 }
29 deriving (Eq, Show)
31type Injs = [(TT Name, TT Name, TT Name)]
32type Fails = [(TT Name, TT Name, -- unification error
33 Bool, -- ready to retry yet
34 Env, Err, [FailContext], FailAt)]
36unrecoverable :: Fails -> Bool
37unrecoverable = any bad
38 where bad (_,_,_,_, err, _, _) = unrec err
40 unrec (CantUnify r _ _ _ _ _) = not r
41 unrec (At _ e) = unrec e
42 unrec (Elaborating _ _ e) = unrec e
43 unrec (ElaboratingArg _ _ _ e) = unrec e
44 unrec _ = False
46data UInfo = UI Int Fails
47 deriving Show
49data UResult a = UOK a
50 | UPartOK a
51 | UFail Err
53-- | Smart constructor for unification errors that takes into account the FailContext
54cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t
55cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
56cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
57 At fc (ElaboratingArg f x
58 (map (\(FailContext _ f' x') -> (f', x')) prev)
59 (CantUnify r t1 t2 e ctxt i))
61-- Solve metavariables by matching terms against each other
62-- Not really unification, of course!
64match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->
65 TC [(Name, TT Name)]
66match_unify ctxt env topx topy inj holes from =
67 case runStateT (un [] (renameBindersTm env topx)
68 (renameBindersTm env topy)) (UI 0 []) of
69 OK (v, UI _ []) ->
70 do v' <- trimSolutions topx topy from env v
71 return (map (renameBinders env) v')
72 res ->
73 let topxn = renameBindersTm env (normalise ctxt env topx)
74 topyn = renameBindersTm env (normalise ctxt env topy) in
75 case runStateT (un [] topxn topyn)
76 (UI 0 []) of
77 OK (v, UI _ fails) ->
78 do v' <- trimSolutions topx topy from env v
79 return (map (renameBinders env) v')
80 Error e ->
81 -- just normalise the term we're matching against
82 case runStateT (un [] topxn topy)
83 (UI 0 []) of
84 OK (v, UI _ fails) ->
85 do v' <- trimSolutions topx topy from env v
86 return (map (renameBinders env) v')
87 _ -> tfail e
88 where
89 -- This rule is highly dubious... it certainly produces a valid answer
90 -- but it scares me. However, matching is never guaranteed to give a unique
91 -- answer, merely a valid one, so perhaps we're okay.
92 -- In other words: it may vanish without warning some day :)
93 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
94 StateT UInfo
95 TC [(Name, TT Name)]
97 un names x tm@(App (P _ f (Bind fn (Pi t _) sc)) a)
98 | (P (DCon _ _ _) _ _, _) <- unApply x,
99 holeIn env f || f `elem` holes
100 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
101 checkCycle names (f, Bind n' (Lam t) x)
102 un names tm@(App (P _ f (Bind fn (Pi t _) sc)) a) x
103 | (P (DCon _ _ _) _ _, _) <- unApply x,
104 holeIn env f || f `elem` holes
105 = let n' = uniqueName fn (map fst env) in
106 checkCycle names (f, Bind n' (Lam t) x)
108 un names tx@(P _ x _) tm
109 | tx /= tm && holeIn env x || x `elem` holes
110 = do sc 1; checkCycle names (x, tm)
111 un names tm ty@(P _ y _)
112 | ty /= tm && holeIn env y || y `elem` holes
113 = do sc 1; checkCycle names (y, tm)
114 un bnames (V i) (P _ x _)
115 | length bnames > i,
116 fst (fst (bnames!!i)) == x ||
117 snd (fst (bnames!!i)) == x = do sc 1; return []
118 un bnames (P _ x _) (V i)
119 | length bnames > i,
120 fst (fst (bnames!!i)) == x ||
121 snd (fst (bnames!!i)) == x = do sc 1; return []
122 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
123 = do h1 <- uB bnames bx by
124 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
125 combine bnames h1 h2
126 un names (App fx ax) (App fy ay)
127 = do hf <- un names fx fy
128 ha <- un names ax ay
129 combine names hf ha
130 un names x y
131 | OK True <- convEq' ctxt holes x y = do sc 1; return []
132 | otherwise = do UI s f <- get
133 let r = recoverable (normalise ctxt env x)
134 (normalise ctxt env y)
135 let err = cantUnify from r
136 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
137 if (not r) then lift $ tfail err
138 else do put (UI s ((x, y, True, env, err, from, Match) : f))
139 lift $ tfail err
142 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
143 h2 <- un bnames vx vy
144 combine bnames h1 h2
145 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
146 uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty
147 uB bnames x y = do UI s f <- get
148 let r = recoverable (normalise ctxt env (binderTy x))
149 (normalise ctxt env (binderTy y))
150 let err = cantUnify from r topx topy
151 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
152 (errEnv env) s
153 put (UI s ((binderTy x, binderTy y,
154 False,
155 env, err, from, Match) : f))
156 return []
158 notHole (Hole _) = False
159 notHole _ = True
161 -- TODO: there's an annoying amount of repetition between this and the
162 -- main unification function. Consider lifting it out.
163 -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721
165 sc i = do UI s f <- get
166 put (UI (s+i) f)
168 unifyFail x y = do UI s f <- get
169 let r = recoverable (normalise ctxt env x)
170 (normalise ctxt env y)
171 let err = cantUnify from r
172 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
173 put (UI s ((x, y, True, env, err, from, Match) : f))
174 lift $ tfail err
175 combine bnames as [] = return as
176 combine bnames as ((n, t) : bs)
177 = case lookup n as of
178 Nothing -> combine bnames (as ++ [(n,t)]) bs
179 Just t' -> do ns <- un bnames t t'
180 let ns' = filter (\ (x, _) -> x/=n) ns
181 sc 1
182 combine bnames as (ns' ++ bs)
184-- substN n tm (var, sol) = (var, subst n tm sol)
186 checkCycle ns p@(x, P _ x' _) | x == x' = return []
187 checkCycle ns p@(x, P _ _ _) = return [p]
188 checkCycle ns (x, tm)
189 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
190 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
192 checkScope ns (x, tm) =
193-- case boundVs (envPos x 0 env) tm of
194-- [] -> return [(x, tm)]
195-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
196-- (inst ns tm) (errEnv env))
197 let v = highV (-1) tm in
198 if v >= length ns
199 then lift $ tfail (Msg "SCOPE ERROR")
200 else return [(x, bind v ns tm)]
201 where inst [] tm = tm
202 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
204 bind i ns tm
205 | i < 0 = tm
206 | otherwise = let ((x,y),ty) = ns!!i in
207 App (Bind y (Lam ty) (bind (i-1) ns tm))
208 (P Bound x ty)
210renameBinders env (x, t) = (x, renameBindersTm env t)
212renameBindersTm :: Env -> TT Name -> TT Name
213renameBindersTm env tm = uniqueBinders (map fst env) tm
214 where
215 uniqueBinders env (Bind n b sc)
216 | n `elem` env
217 = let n' = uniqueName n env in
218 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
219 (uniqueBinders (n':env) (rename n n' sc))
220 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
221 (uniqueBinders (n:env) sc)
222 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)
223 uniqueBinders env t = t
225 rename n n' (P nt x ty) | n == x = P nt n' ty
226 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
227 rename n n' (App f a) = App (rename n n' f) (rename n n' a)
228 rename n n' t = t
230 explicitHole (Bind n (Hole ty) sc)
231 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
232 explicitHole t = t
234trimSolutions topx topy from env topns = followSols [] (dropPairs topns)
235 where dropPairs [] = []
236 dropPairs (n@(x, P _ x' _) : ns)
237 | x == x' = dropPairs ns
238 | otherwise
239 = n : dropPairs
240 (filter (\t -> case t of
241 (n, P _ n' _) -> not (n == x' && n' == x)
242 _ -> True) ns)
243 dropPairs (n : ns) = n : dropPairs ns
245 followSols vs [] = return []
246 followSols vs ((n, P _ t _) : ns)
247 | Just t' <- lookup t ns
248 = do vs' <- case t' of
249 P _ tn _ ->
250 if (n, tn) `elem` vs then -- cycle
251 tfail (cantUnify from False topx topy
252 (Msg "") (errEnv env) 0)
253 else return ((n, tn) : vs)
254 _ -> return vs
255 followSols vs' ((n, t') : ns)
256 followSols vs (n : ns) = do ns' <- followSols vs ns
257 return $ n : ns'
259expandLets env (x, tm) = (x, doSubst (reverse env) tm)
260 where
261 doSubst [] tm = tm
262 doSubst ((n, Let v t) : env) tm
263 = doSubst env (subst n v tm)
264 doSubst (_ : env) tm
265 = doSubst env tm
267hasv :: TT Name -> Bool
268hasv (V x) = True
269hasv (App f a) = hasv f || hasv a
270hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
271hasv _ = False
273unify :: Context -> Env -> TT Name -> TT Name ->
274 [Name] -> [Name] -> [Name] -> [FailContext] ->
275 TC ([(Name, TT Name)], Fails)
276unify ctxt env topx topy inj holes usersupp from =
277-- traceWhen (hasv topx || hasv topy)
278-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
279 -- don't bother if topx and topy are different at the head
280 case runStateT (un False [] (renameBindersTm env topx)
281 (renameBindersTm env topy)) (UI 0 []) of
282 OK (v, UI _ []) -> do v' <- trimSolutions topx topy from env v
283 return (map (renameBinders env) v', [])
284 res ->
285 let topxn = renameBindersTm env (normalise ctxt env topx)
286 topyn = renameBindersTm env (normalise ctxt env topy) in
287-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
288 case runStateT (un False [] topxn topyn)
289 (UI 0 []) of
290 OK (v, UI _ fails) ->
291 do v' <- trimSolutions topx topy from env v
292 return (map (renameBinders env) v', reverse fails)
293-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
294 Error e -> tfail e
295 where
296 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
297 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
298 headDiff _ _ = False
300 injective (P (DCon _ _ _) _ _) = True
301 injective (P (TCon _ _) _ _) = True
302-- injective (App f (P _ _ _)) = injective f
303-- injective (App f (Constant _)) = injective f
304 injective (App f a) = injective f -- && injective a
305 injective _ = False
307-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
308 injectiveVar (P _ n _) = n `elem` inj
309 injectiveVar (App f a) = injectiveVar f -- && injective a
310 injectiveVar _ = False
312 injectiveApp x = injective x || injectiveVar x
314 notP (P _ _ _) = False
315 notP _ = True
317 sc i = do UI s f <- get
318 put (UI (s+i) f)
320 errors :: StateT UInfo TC Bool
321 errors = do UI s f <- get
322 return (not (null f))
324 uplus u1 u2 = do UI s f <- get
325 r <- u1
326 UI s f' <- get
327 if (length f == length f')
328 then return r
329 else do put (UI s f); u2
331 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
332 StateT UInfo
333 TC [(Name, TT Name)]
334 un = un'
335-- un fn names x y
336-- = let (xf, _) = unApply x
337-- (yf, _) = unApply y in
338-- if headDiff xf yf then unifyFail x y else
339-- uplus (un' fn names x y)
340-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
342 un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
343 StateT UInfo
344 TC [(Name, TT Name)]
345 un' fn names x y | x == y = return [] -- shortcut
346 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
347 | x /= y = unifyFail topx topy
348 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
349 | x /= y = unifyFail topx topy
350 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
351 = unifyFail topx topy
352 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
353 = unifyFail topx topy
354 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
355 = unifyFail topx topy
356 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
357 = unifyFail topx topy
358 un' fn bnames tx@(P _ x _) ty@(P _ y _)
359 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
360 | injective tx && not (holeIn env y || y `elem` holes)
361 = unifyTmpFail tx ty
362 | injective ty && not (holeIn env x || x `elem` holes)
363 = unifyTmpFail tx ty
364 -- pick the one bound earliest if both are holes
365 | tx /= ty && (holeIn env x || x `elem` holes)
366 && (holeIn env y || y `elem` holes)
367 = case compare (envPos 0 x env) (envPos 0 y env) of
368 LT -> do sc 1; checkCycle bnames (x, ty)
369 _ -> do sc 1; checkCycle bnames (y, tx)
370 where envPos i n ((n',_):env) | n == n' = i
371 envPos i n (_:env) = envPos (i+1) n env
372 envPos _ _ _ = 100000
373 un' fn bnames xtm@(P _ x _) tm
374 | pureTerm tm, holeIn env x || x `elem` holes
375 = do UI s f <- get
376 -- injectivity check
377 x <- checkCycle bnames (x, tm)
378 if (notP tm && fn)
379-- trace (show (x, tm, normalise ctxt env tm)) $
380-- put (UI s ((tm, topx, topy) : i) f)
381 then unifyTmpFail xtm tm
382 else do sc 1
383 return x
384 | pureTerm tm, not (injective xtm) && injective tm
385 = do checkCycle bnames (x, tm)
386 unifyTmpFail xtm tm
387 un' fn bnames tm ytm@(P _ y _)
388 | pureTerm tm, holeIn env y || y `elem` holes
389 = do UI s f <- get
390 -- injectivity check
391 x <- checkCycle bnames (y, tm)
392 if (notP tm && fn)
393-- trace (show (y, tm, normalise ctxt env tm)) $
394-- put (UI s ((tm, topx, topy) : i) f)
395 then unifyTmpFail tm ytm
396 else do sc 1
397 return x
398 | pureTerm tm, not (injective ytm) && injective tm
399 = do checkCycle bnames (y, tm)
400 unifyTmpFail tm ytm
401 un' fn bnames (V i) (P _ x _)
402 | length bnames > i,
403 fst ((map fst bnames)!!i) == x ||
404 snd ((map fst bnames)!!i) == x = do sc 1; return []
405 un' fn bnames (P _ x _) (V i)
406 | length bnames > i,
407 fst ((map fst bnames)!!i) == x ||
408 snd ((map fst bnames)!!i) == x = do sc 1; return []
410 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
411 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
413 un' fn bnames appx@(App _ _) appy@(App _ _)
414 = unApp fn bnames appx appy
415-- = uplus (unApp fn bnames appx appy)
416-- (unifyTmpFail appx appy) -- take the whole lot
418 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
419 | n == n' = un' False bnames x y
420 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
421 | n == n' = un' False bnames x y
422 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
423 = un' False bnames x y
424 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
425 = un' False bnames x y
426-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
427-- = un' False ((x,y):bnames) sx sy
428-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
429-- = un' False ((x,y):bnames) sx sy
431 -- f D unifies with t -> D. This is dubious, but it helps with type
432 -- class resolution for type classes over functions.
434 un' fn bnames (App f x) (Bind n (Pi t k) y)
435 | noOccurrence n y && injectiveApp f
436 = do ux <- un' False bnames x y
437 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
438 (Bind n (Pi t k) (V 1)))
439 combine bnames ux uf
441 un' fn bnames (Bind n (Pi t k) y) (App f x)
442 | noOccurrence n y && injectiveApp f
443 = do ux <- un' False bnames y x
444 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
445 (Bind n (Pi t k) (V 1))) f
446 combine bnames ux uf
448 un' fn bnames (Bind x bx sx) (Bind y by sy)
449 | sameBinder bx by
450 = do h1 <- uB bnames bx by
451 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
452 combine bnames h1 h2
453 where sameBinder (Lam _) (Lam _) = True
454 sameBinder (Pi _ _) (Pi _ _) = True
455 sameBinder _ _ = False
456 un' fn bnames x y
457 | OK True <- convEq' ctxt holes x y = do sc 1; return []
458 | isUniverse x && isUniverse y = do sc 1; return []
459 | otherwise = do UI s f <- get
460 let r = recoverable (normalise ctxt env x)
461 (normalise ctxt env y)
462 let err = cantUnify from r
463 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
464 if (not r) then lift $ tfail err
465 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
466 return [] -- lift $ tfail err
468 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
469 -- shortcut for the common case where we just want to check the
470 -- arguments are correct
471 | (injectiveApp fx && fx == fy)
472 = un' False bnames ax ay
473 | (injectiveApp fx && injectiveApp fy)
474 || (injectiveApp fx && metavarApp fy && ax == ay)
475 || (injectiveApp fy && metavarApp fx && ax == ay)
476 = do let (headx, _) = unApply fx
477 let (heady, _) = unApply fy
478 -- fail quickly if the heads are disjoint
479 checkHeads headx heady
480 uplus
481 (do hf <- un' True bnames fx fy
482 let ax' = hnormalise hf ctxt env (substNames hf ax)
483 let ay' = hnormalise hf ctxt env (substNames hf ay)
484 ha <- un' False bnames ax' ay'
485 sc 1
486 combine bnames hf ha)
487 (do ha <- un' False bnames ax ay
488 let fx' = hnormalise ha ctxt env (substNames ha fx)
489 let fy' = hnormalise ha ctxt env (substNames ha fy)
490 hf <- un' False bnames fx' fy'
491 sc 1
492 combine bnames hf ha)
493 | otherwise = unifyTmpFail appx appy
494 where hnormalise [] _ _ t = t
495 hnormalise ns ctxt env t = normalise ctxt env t
496 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
497 | x /= y = unifyFail appx appy
498 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
499 | x /= y = unifyFail appx appy
500 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
501 = unifyFail appx appy
502 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
503 = unifyFail appx appy
504 checkHeads _ _ = return []
506 unArgs as [] [] = return as
507 unArgs as (x : xs) (y : ys)
508 = do let x' = hnormalise as ctxt env (substNames as x)
509 let y' = hnormalise as ctxt env (substNames as y)
510 as' <- un' False bnames x' y'
511 vs <- combine bnames as as'
512 unArgs vs xs ys
514 numArgs tm = let (f, args) = unApply tm in length args
516 metavarApp tm = let (f, args) = unApply tm in
517 (metavar f &&
518 all (\x -> metavarApp x) args
519 && nub args == args) ||
520 globmetavar tm
521 metavarArgs tm = let (f, args) = unApply tm in
522 all (\x -> metavar x || inenv x) args
523 && nub args == args
524 metavarApp' tm = let (f, args) = unApply tm in
525 all (\x -> pat x || metavar x) (f : args)
526 && nub args == args
528 rigid (P (DCon _ _ _) _ _) = True
529 rigid (P (TCon _ _) _ _) = True
530 rigid t@(P Ref _ _) = inenv t || globmetavar t
531 rigid (Constant _) = True
532 rigid (App f a) = rigid f && rigid a
533 rigid t = not (metavar t) || globmetavar t
535 globmetavar t = case unApply t of
536 (P _ x _, _) ->
537 case lookupDef x ctxt of
538 [TyDecl _ _] -> True
539 _ -> False
540 _ -> False
542 metavar t = case t of
543 P _ x _ -> (x `notElem` usersupp &&
544 (x `elem` holes || holeIn env x))
545 || globmetavar t
546 _ -> False
547 pat t = case t of
548 P _ x _ -> x `elem` holes || patIn env x
549 _ -> False
550 inenv t = case t of
551 P _ x _ -> x `elem` (map fst env)
552 _ -> False
554 notFn t = injective t || metavar t || inenv t
557 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
558 unifyTmpFail x y
559 = do UI s f <- get
560 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
561 let err = cantUnify from r
562 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
563 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
564 return []
566 -- shortcut failure, if we *know* nothing can fix it
567 unifyFail x y = do UI s f <- get
568 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
569 let err = cantUnify from r
570 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
571 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
572 lift $ tfail err
575 uB bnames (Let tx vx) (Let ty vy)
576 = do h1 <- un' False bnames tx ty
577 h2 <- un' False bnames vx vy
578 sc 1
579 combine bnames h1 h2
580 uB bnames (Guess tx vx) (Guess ty vy)
581 = do h1 <- un' False bnames tx ty
582 h2 <- un' False bnames vx vy
583 sc 1
584 combine bnames h1 h2
585 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
586 uB bnames (Pi tx _) (Pi ty _) = do sc 1; un' False bnames tx ty
587 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
588 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
589 uB bnames x y = do UI s f <- get
590 let r = recoverable (normalise ctxt env (binderTy x))
591 (normalise ctxt env (binderTy y))
592 let err = cantUnify from r topx topy
593 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
594 (errEnv env) s
595 put (UI s ((binderTy x, binderTy y,
596 False,
597 env, err, from, Unify) : f))
598 return [] -- lift $ tfail err
600 checkCycle ns p@(x, P _ _ _) = return [p]
601 checkCycle ns (x, tm)
602 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
603 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
605 checkScope ns (x, tm) | pureTerm tm =
606-- case boundVs (envPos x 0 env) tm of
607-- [] -> return [(x, tm)]
608-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
609-- (inst ns tm) (errEnv env))
610 let v = highV (-1) tm in
611 if v >= length ns
612 then lift $ tfail (Msg "SCOPE ERROR")
613 else return [(x, bind v ns tm)]
614 where inst [] tm = tm
615 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
616 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
618 bind i ns tm
619 | i < 0 = tm
620 | otherwise = let ((x,y),ty) = ns!!i in
621 App (Bind y (Lam ty) (bind (i-1) ns tm))
622 (P Bound x ty)
624 combineArgs bnames args = ca [] args where
625 ca acc [] = return acc
626 ca acc (x : xs) = do x' <- combine bnames acc x
627 ca x' xs
629 combine bnames as [] = return as
630 combine bnames as ((n, t) : bs)
631 = case lookup n as of
632 Nothing -> combine bnames (as ++ [(n,t)]) bs
633 Just t' -> do ns <- un' False bnames t t'
634 -- make sure there's n mapping from n in ns
635 let ns' = filter (\ (x, _) -> x/=n) ns
636 sc 1
637 combine bnames as (ns' ++ bs)
639boundVs :: Int -> Term -> [Int]
640boundVs i (V j) | j < i = []
641 | otherwise = [j]
642boundVs i (Bind n b sc) = boundVs (i + 1) sc
643boundVs i (App f x) = let fs = boundVs i f
644 xs = boundVs i x in
645 nub (fs ++ xs)
646boundVs i _ = []
648highV :: Int -> Term -> Int
649highV i (V j) | j > i = j
650 | otherwise = i
651highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
652highV i (App f x) = max (highV i f) (highV i x)
653highV i _ = i
655envPos x i [] = 0
656envPos x i ((y, _) : ys) | x == y = i
657 | otherwise = envPos x (i + 1) ys
660-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
661-- more work may help.
662-- FIXME: Depending on how overloading gets used, this may cause problems. Better
663-- rethink overloading properly...
664-- ASSUMPTION: inputs are in normal form
665--
666-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
667--
668recoverable t@(App _ _) _
669 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
670recoverable _ t@(App _ _)
671 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
672recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
673recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
674recoverable (Constant _) (P (DCon _ _ _) y _) = False
675recoverable (Constant x) (Constant y) = x == y
676recoverable (P (DCon _ _ _) x _) (Constant _) = False
677recoverable (Constant _) (P (TCon _ _) y _) = False
678recoverable (P (TCon _ _) x _) (Constant _) = False
679recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
680recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
681recoverable p@(Constant _) (App f a) = recoverable p f
682recoverable (App f a) p@(Constant _) = recoverable f p
683recoverable p@(P _ n _) (App f a) = recoverable p f
684recoverable (App f a) p@(P _ _ _) = recoverable f p
685recoverable (App f a) (App f' a')
686 | f == f' = recoverable a a'
687recoverable (App f a) (App f' a')
688 = recoverable f f' -- && recoverable a a'
689recoverable f (Bind _ (Pi _ _) sc)
690 | (P (DCon _ _ _) _ _, _) <- unApply f = False
691 | (P (TCon _ _) _ _, _) <- unApply f = False
692recoverable (Bind _ (Pi _ _) sc) f
693 | (P (DCon _ _ _) _ _, _) <- unApply f = False
694 | (P (TCon _ _) _ _, _) <- unApply f = False
695recoverable (Bind _ (Lam _) sc) f = recoverable sc f
696recoverable f (Bind _ (Lam _) sc) = recoverable f sc
697recoverable x y = True
699errEnv :: [(a, Binder b)] -> [(a, b)]
700errEnv = map (\(x, b) -> (x, binderTy b))
702holeIn :: Env -> Name -> Bool
703holeIn env n = case lookup n env of
704 Just (Hole _) -> True
705 Just (Guess _ _) -> True
706 _ -> False
708patIn :: Env -> Name -> Bool
709patIn env n = case lookup n env of
710 Just (PVar _) -> True
711 Just (PVTy _) -> True
712 _ -> False