git.iko.soy/Idris-dev
on de2011f help sign in
Idris-dev/src/Idris/Core/Unify.hs
722 lines 32 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 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
90 StateT UInfo
91 TC [(Name, TT Name)]
93 -- This rule is highly dubious... it certainly produces a valid answer
94 -- but it scares me. However, matching is never guaranteed to give a unique
95 -- answer, merely a valid one, so perhaps we're okay.
96 -- In other words: it may vanish without warning some day :)
97 un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)
98 | (P (TCon _ _) _ _, _) <- 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 (TCon _ _) _ _, _) <- 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)
107 un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)
108 | (P (DCon _ _ _) _ _, _) <- unApply x,
109 holeIn env f || f `elem` holes
110 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
111 checkCycle names (f, Bind n' (Lam t) x)
112 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x
113 | (P (DCon _ _ _) _ _, _) <- unApply x,
114 holeIn env f || f `elem` holes
115 = let n' = uniqueName fn (map fst env) in
116 checkCycle names (f, Bind n' (Lam t) x)
118 un names tx@(P _ x _) tm
119 | tx /= tm && holeIn env x || x `elem` holes
120 = do sc 1; checkCycle names (x, tm)
121 un names tm ty@(P _ y _)
122 | ty /= tm && holeIn env y || y `elem` holes
123 = do sc 1; checkCycle names (y, tm)
124 un bnames (V i) (P _ x _)
125 | length bnames > i,
126 fst (fst (bnames!!i)) == x ||
127 snd (fst (bnames!!i)) == x = do sc 1; return []
128 un bnames (P _ x _) (V i)
129 | length bnames > i,
130 fst (fst (bnames!!i)) == x ||
131 snd (fst (bnames!!i)) == x = do sc 1; return []
132 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
133 = do h1 <- uB bnames bx by
134 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
135 combine bnames h1 h2
136 un names (App fx ax) (App fy ay)
137 = do hf <- un names fx fy
138 ha <- un names ax ay
139 combine names hf ha
140 un names x y
141 | OK True <- convEq' ctxt holes x y = do sc 1; return []
142 | otherwise = do UI s f <- get
143 let r = recoverable (normalise ctxt env x)
144 (normalise ctxt env y)
145 let err = cantUnify from r
146 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
147 if (not r) then lift $ tfail err
148 else do put (UI s ((x, y, True, env, err, from, Match) : f))
149 lift $ tfail err
152 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
153 h2 <- un bnames vx vy
154 combine bnames h1 h2
155 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
156 uB bnames (Pi _ tx _) (Pi _ ty _) = un bnames tx ty
157 uB bnames x y = do UI s f <- get
158 let r = recoverable (normalise ctxt env (binderTy x))
159 (normalise ctxt env (binderTy y))
160 let err = cantUnify from r topx topy
161 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
162 (errEnv env) s
163 put (UI s ((binderTy x, binderTy y,
164 False,
165 env, err, from, Match) : f))
166 return []
168 notHole (Hole _) = False
169 notHole _ = True
171 -- TODO: there's an annoying amount of repetition between this and the
172 -- main unification function. Consider lifting it out.
173 -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721
175 sc i = do UI s f <- get
176 put (UI (s+i) f)
178 unifyFail x y = do UI s f <- get
179 let r = recoverable (normalise ctxt env x)
180 (normalise ctxt env y)
181 let err = cantUnify from r
182 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
183 put (UI s ((x, y, True, env, err, from, Match) : f))
184 lift $ tfail err
185 combine bnames as [] = return as
186 combine bnames as ((n, t) : bs)
187 = case lookup n as of
188 Nothing -> combine bnames (as ++ [(n,t)]) bs
189 Just t' -> do ns <- un bnames t t'
190 let ns' = filter (\ (x, _) -> x/=n) ns
191 sc 1
192 combine bnames as (ns' ++ bs)
194-- substN n tm (var, sol) = (var, subst n tm sol)
196 checkCycle ns p@(x, P _ x' _) | x == x' = return []
197 checkCycle ns p@(x, P _ _ _) = return [p]
198 checkCycle ns (x, tm)
199 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
200 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
202 checkScope ns (x, tm) =
203-- case boundVs (envPos x 0 env) tm of
204-- [] -> return [(x, tm)]
205-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
206-- (inst ns tm) (errEnv env))
207 let v = highV (-1) tm in
208 if v >= length ns
209 then lift $ tfail (Msg "SCOPE ERROR")
210 else return [(x, bind v ns tm)]
211 where inst [] tm = tm
212 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
214 bind i ns tm
215 | i < 0 = tm
216 | otherwise = let ((x,y),ty) = ns!!i in
217 App (Bind y (Lam ty) (bind (i-1) ns tm))
218 (P Bound x ty)
220renameBinders env (x, t) = (x, renameBindersTm env t)
222renameBindersTm :: Env -> TT Name -> TT Name
223renameBindersTm env tm = uniqueBinders (map fst env) tm
224 where
225 uniqueBinders env (Bind n b sc)
226 | n `elem` env
227 = let n' = uniqueName n env in
228 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
229 (uniqueBinders (n':env) (rename n n' sc))
230 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
231 (uniqueBinders (n:env) sc)
232 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)
233 uniqueBinders env t = t
235 rename n n' (P nt x ty) | n == x = P nt n' ty
236 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
237 rename n n' (App f a) = App (rename n n' f) (rename n n' a)
238 rename n n' t = t
240 explicitHole (Bind n (Hole ty) sc)
241 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
242 explicitHole t = t
244trimSolutions topx topy from env topns = followSols [] (dropPairs topns)
245 where dropPairs [] = []
246 dropPairs (n@(x, P _ x' _) : ns)
247 | x == x' = dropPairs ns
248 | otherwise
249 = n : dropPairs
250 (filter (\t -> case t of
251 (n, P _ n' _) -> not (n == x' && n' == x)
252 _ -> True) ns)
253 dropPairs (n : ns) = n : dropPairs ns
255 followSols vs [] = return []
256 followSols vs ((n, P _ t _) : ns)
257 | Just t' <- lookup t ns
258 = do vs' <- case t' of
259 P _ tn _ ->
260 if (n, tn) `elem` vs then -- cycle
261 tfail (cantUnify from False topx topy
262 (Msg "") (errEnv env) 0)
263 else return ((n, tn) : vs)
264 _ -> return vs
265 followSols vs' ((n, t') : ns)
266 followSols vs (n : ns) = do ns' <- followSols vs ns
267 return $ n : ns'
269expandLets env (x, tm) = (x, doSubst (reverse env) tm)
270 where
271 doSubst [] tm = tm
272 doSubst ((n, Let v t) : env) tm
273 = doSubst env (subst n v tm)
274 doSubst (_ : env) tm
275 = doSubst env tm
277hasv :: TT Name -> Bool
278hasv (V x) = True
279hasv (App f a) = hasv f || hasv a
280hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
281hasv _ = False
283unify :: Context -> Env -> TT Name -> TT Name ->
284 [Name] -> [Name] -> [Name] -> [FailContext] ->
285 TC ([(Name, TT Name)], Fails)
286unify ctxt env topx topy inj holes usersupp from =
287-- traceWhen (hasv topx || hasv topy)
288-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
289 -- don't bother if topx and topy are different at the head
290 case runStateT (un False [] (renameBindersTm env topx)
291 (renameBindersTm env topy)) (UI 0 []) of
292 OK (v, UI _ []) -> do v' <- trimSolutions topx topy from env v
293 return (map (renameBinders env) v', [])
294 res ->
295 let topxn = renameBindersTm env (normalise ctxt env topx)
296 topyn = renameBindersTm env (normalise ctxt env topy) in
297-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
298 case runStateT (un False [] topxn topyn)
299 (UI 0 []) of
300 OK (v, UI _ fails) ->
301 do v' <- trimSolutions topx topy from env v
302 return (map (renameBinders env) v', reverse fails)
303-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
304 Error e -> tfail e
305 where
306 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
307 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
308 headDiff _ _ = False
310 injective (P (DCon _ _ _) _ _) = True
311 injective (P (TCon _ _) _ _) = True
312-- injective (App f (P _ _ _)) = injective f
313-- injective (App f (Constant _)) = injective f
314 injective (App f a) = injective f -- && injective a
315 injective _ = False
317-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
318 injectiveVar (P _ n _) = n `elem` inj
319 injectiveVar (App f a) = injectiveVar f -- && injective a
320 injectiveVar _ = False
322 injectiveApp x = injective x || injectiveVar x
324 notP (P _ _ _) = False
325 notP _ = True
327 sc i = do UI s f <- get
328 put (UI (s+i) f)
330 errors :: StateT UInfo TC Bool
331 errors = do UI s f <- get
332 return (not (null f))
334 uplus u1 u2 = do UI s f <- get
335 r <- u1
336 UI s f' <- get
337 if (length f == length f')
338 then return r
339 else do put (UI s f); u2
341 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
342 StateT UInfo
343 TC [(Name, TT Name)]
344 un = un'
345-- un fn names x y
346-- = let (xf, _) = unApply x
347-- (yf, _) = unApply y in
348-- if headDiff xf yf then unifyFail x y else
349-- uplus (un' fn names x y)
350-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
352 un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
353 StateT UInfo
354 TC [(Name, TT Name)]
355 un' fn names x y | x == y = return [] -- shortcut
356 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
357 | x /= y = unifyFail topx topy
358 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
359 | x /= y = unifyFail topx topy
360 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
361 = unifyFail topx topy
362 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
363 = unifyFail topx topy
364 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
365 = unifyFail topx topy
366 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
367 = unifyFail topx topy
368 un' fn bnames tx@(P _ x _) ty@(P _ y _)
369 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
370 | injective tx && not (holeIn env y || y `elem` holes)
371 = unifyTmpFail tx ty
372 | injective ty && not (holeIn env x || x `elem` holes)
373 = unifyTmpFail tx ty
374 -- pick the one bound earliest if both are holes
375 | tx /= ty && (holeIn env x || x `elem` holes)
376 && (holeIn env y || y `elem` holes)
377 = case compare (envPos 0 x env) (envPos 0 y env) of
378 LT -> do sc 1; checkCycle bnames (x, ty)
379 _ -> do sc 1; checkCycle bnames (y, tx)
380 where envPos i n ((n',_):env) | n == n' = i
381 envPos i n (_:env) = envPos (i+1) n env
382 envPos _ _ _ = 100000
383 un' fn bnames xtm@(P _ x _) tm
384 | pureTerm tm, holeIn env x || x `elem` holes
385 = do UI s f <- get
386 -- injectivity check
387 x <- checkCycle bnames (x, tm)
388 if (notP tm && fn)
389-- trace (show (x, tm, normalise ctxt env tm)) $
390-- put (UI s ((tm, topx, topy) : i) f)
391 then unifyTmpFail xtm tm
392 else do sc 1
393 return x
394 | pureTerm tm, not (injective xtm) && injective tm
395 = do checkCycle bnames (x, tm)
396 unifyTmpFail xtm tm
397 un' fn bnames tm ytm@(P _ y _)
398 | pureTerm tm, holeIn env y || y `elem` holes
399 = do UI s f <- get
400 -- injectivity check
401 x <- checkCycle bnames (y, tm)
402 if (notP tm && fn)
403-- trace (show (y, tm, normalise ctxt env tm)) $
404-- put (UI s ((tm, topx, topy) : i) f)
405 then unifyTmpFail tm ytm
406 else do sc 1
407 return x
408 | pureTerm tm, not (injective ytm) && injective tm
409 = do checkCycle bnames (y, tm)
410 unifyTmpFail tm ytm
411 un' fn bnames (V i) (P _ x _)
412 | length bnames > i,
413 fst ((map fst bnames)!!i) == x ||
414 snd ((map fst bnames)!!i) == x = do sc 1; return []
415 un' fn bnames (P _ x _) (V i)
416 | length bnames > i,
417 fst ((map fst bnames)!!i) == x ||
418 snd ((map fst bnames)!!i) == x = do sc 1; return []
420 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
421 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
423 un' fn bnames appx@(App _ _) appy@(App _ _)
424 = unApp fn bnames appx appy
425-- = uplus (unApp fn bnames appx appy)
426-- (unifyTmpFail appx appy) -- take the whole lot
428 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
429 | n == n' = un' False bnames x y
430 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
431 | n == n' = un' False bnames x y
432 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
433 = un' False bnames x y
434 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
435 = un' False bnames x y
436-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
437-- = un' False ((x,y):bnames) sx sy
438-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
439-- = un' False ((x,y):bnames) sx sy
441 -- f D unifies with t -> D. This is dubious, but it helps with type
442 -- class resolution for type classes over functions.
444 un' fn bnames (App f x) (Bind n (Pi i t k) y)
445 | noOccurrence n y && injectiveApp f
446 = do ux <- un' False bnames x y
447 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
448 (Bind n (Pi i t k) (V 1)))
449 combine bnames ux uf
451 un' fn bnames (Bind n (Pi i t k) y) (App f x)
452 | noOccurrence n y && injectiveApp f
453 = do ux <- un' False bnames y x
454 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
455 (Bind n (Pi i t k) (V 1))) f
456 combine bnames ux uf
458 un' fn bnames (Bind x bx sx) (Bind y by sy)
459 | sameBinder bx by
460 = do h1 <- uB bnames bx by
461 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
462 combine bnames h1 h2
463 where sameBinder (Lam _) (Lam _) = True
464 sameBinder (Pi _ _ _) (Pi _ _ _) = True
465 sameBinder _ _ = False
466 un' fn bnames x y
467 | OK True <- convEq' ctxt holes x y = do sc 1; return []
468 | isUniverse x && isUniverse y = do sc 1; return []
469 | otherwise = do UI s f <- get
470 let r = recoverable (normalise ctxt env x)
471 (normalise ctxt env y)
472 let err = cantUnify from r
473 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
474 if (not r) then lift $ tfail err
475 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
476 return [] -- lift $ tfail err
478 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
479 -- shortcut for the common case where we just want to check the
480 -- arguments are correct
481 | (injectiveApp fx && fx == fy)
482 = un' False bnames ax ay
483 | (injectiveApp fx && injectiveApp fy)
484 || (injectiveApp fx && metavarApp fy && ax == ay)
485 || (injectiveApp fy && metavarApp fx && ax == ay)
486 = do let (headx, _) = unApply fx
487 let (heady, _) = unApply fy
488 -- fail quickly if the heads are disjoint
489 checkHeads headx heady
490 uplus
491 (do hf <- un' True bnames fx fy
492 let ax' = hnormalise hf ctxt env (substNames hf ax)
493 let ay' = hnormalise hf ctxt env (substNames hf ay)
494 ha <- un' False bnames ax' ay'
495 sc 1
496 combine bnames hf ha)
497 (do ha <- un' False bnames ax ay
498 let fx' = hnormalise ha ctxt env (substNames ha fx)
499 let fy' = hnormalise ha ctxt env (substNames ha fy)
500 hf <- un' False bnames fx' fy'
501 sc 1
502 combine bnames hf ha)
503 | otherwise = unifyTmpFail appx appy
504 where hnormalise [] _ _ t = t
505 hnormalise ns ctxt env t = normalise ctxt env t
506 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
507 | x /= y = unifyFail appx appy
508 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
509 | x /= y = unifyFail appx appy
510 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
511 = unifyFail appx appy
512 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
513 = unifyFail appx appy
514 checkHeads _ _ = return []
516 unArgs as [] [] = return as
517 unArgs as (x : xs) (y : ys)
518 = do let x' = hnormalise as ctxt env (substNames as x)
519 let y' = hnormalise as ctxt env (substNames as y)
520 as' <- un' False bnames x' y'
521 vs <- combine bnames as as'
522 unArgs vs xs ys
524 numArgs tm = let (f, args) = unApply tm in length args
526 metavarApp tm = let (f, args) = unApply tm in
527 (metavar f &&
528 all (\x -> metavarApp x) args
529 && nub args == args) ||
530 globmetavar tm
531 metavarArgs tm = let (f, args) = unApply tm in
532 all (\x -> metavar x || inenv x) args
533 && nub args == args
534 metavarApp' tm = let (f, args) = unApply tm in
535 all (\x -> pat x || metavar x) (f : args)
536 && nub args == args
538 rigid (P (DCon _ _ _) _ _) = True
539 rigid (P (TCon _ _) _ _) = True
540 rigid t@(P Ref _ _) = inenv t || globmetavar t
541 rigid (Constant _) = True
542 rigid (App f a) = rigid f && rigid a
543 rigid t = not (metavar t) || globmetavar t
545 globmetavar t = case unApply t of
546 (P _ x _, _) ->
547 case lookupDef x ctxt of
548 [TyDecl _ _] -> True
549 _ -> False
550 _ -> False
552 metavar t = case t of
553 P _ x _ -> (x `notElem` usersupp &&
554 (x `elem` holes || holeIn env x))
555 || globmetavar t
556 _ -> False
557 pat t = case t of
558 P _ x _ -> x `elem` holes || patIn env x
559 _ -> False
560 inenv t = case t of
561 P _ x _ -> x `elem` (map fst env)
562 _ -> False
564 notFn t = injective t || metavar t || inenv t
567 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
568 unifyTmpFail x y
569 = do UI s f <- get
570 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
571 let err = cantUnify from r
572 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
573 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
574 return []
576 -- shortcut failure, if we *know* nothing can fix it
577 unifyFail x y = do UI s f <- get
578 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
579 let err = cantUnify from r
580 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
581 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
582 lift $ tfail err
585 uB bnames (Let tx vx) (Let ty vy)
586 = do h1 <- un' False bnames tx ty
587 h2 <- un' False bnames vx vy
588 sc 1
589 combine bnames h1 h2
590 uB bnames (Guess tx vx) (Guess ty vy)
591 = do h1 <- un' False bnames tx ty
592 h2 <- un' False bnames vx vy
593 sc 1
594 combine bnames h1 h2
595 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
596 uB bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' False bnames tx ty
597 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
598 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
599 uB bnames x y = do UI s f <- get
600 let r = recoverable (normalise ctxt env (binderTy x))
601 (normalise ctxt env (binderTy y))
602 let err = cantUnify from r topx topy
603 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
604 (errEnv env) s
605 put (UI s ((binderTy x, binderTy y,
606 False,
607 env, err, from, Unify) : f))
608 return [] -- lift $ tfail err
610 checkCycle ns p@(x, P _ _ _) = return [p]
611 checkCycle ns (x, tm)
612 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
613 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
615 checkScope ns (x, tm) | pureTerm tm =
616-- case boundVs (envPos x 0 env) tm of
617-- [] -> return [(x, tm)]
618-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
619-- (inst ns tm) (errEnv env))
620 let v = highV (-1) tm in
621 if v >= length ns
622 then lift $ tfail (Msg "SCOPE ERROR")
623 else return [(x, bind v ns tm)]
624 where inst [] tm = tm
625 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
626 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
628 bind i ns tm
629 | i < 0 = tm
630 | otherwise = let ((x,y),ty) = ns!!i in
631 App (Bind y (Lam ty) (bind (i-1) ns tm))
632 (P Bound x ty)
634 combineArgs bnames args = ca [] args where
635 ca acc [] = return acc
636 ca acc (x : xs) = do x' <- combine bnames acc x
637 ca x' xs
639 combine bnames as [] = return as
640 combine bnames as ((n, t) : bs)
641 = case lookup n as of
642 Nothing -> combine bnames (as ++ [(n,t)]) bs
643 Just t' -> do ns <- un' False bnames t t'
644 -- make sure there's n mapping from n in ns
645 let ns' = filter (\ (x, _) -> x/=n) ns
646 sc 1
647 combine bnames as (ns' ++ bs)
649boundVs :: Int -> Term -> [Int]
650boundVs i (V j) | j < i = []
651 | otherwise = [j]
652boundVs i (Bind n b sc) = boundVs (i + 1) sc
653boundVs i (App f x) = let fs = boundVs i f
654 xs = boundVs i x in
655 nub (fs ++ xs)
656boundVs i _ = []
658highV :: Int -> Term -> Int
659highV i (V j) | j > i = j
660 | otherwise = i
661highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
662highV i (App f x) = max (highV i f) (highV i x)
663highV i _ = i
665envPos x i [] = 0
666envPos x i ((y, _) : ys) | x == y = i
667 | otherwise = envPos x (i + 1) ys
670-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
671-- more work may help.
672-- FIXME: Depending on how overloading gets used, this may cause problems. Better
673-- rethink overloading properly...
674-- ASSUMPTION: inputs are in normal form
675--
676-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
677--
678recoverable t@(App _ _) _
679 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
680recoverable _ t@(App _ _)
681 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
682recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
683recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
684recoverable (Constant _) (P (DCon _ _ _) y _) = False
685recoverable (Constant x) (Constant y) = x == y
686recoverable (P (DCon _ _ _) x _) (Constant _) = False
687recoverable (Constant _) (P (TCon _ _) y _) = False
688recoverable (P (TCon _ _) x _) (Constant _) = False
689recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
690recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
691recoverable p@(Constant _) (App f a) = recoverable p f
692recoverable (App f a) p@(Constant _) = recoverable f p
693recoverable p@(P _ n _) (App f a) = recoverable p f
694recoverable (App f a) p@(P _ _ _) = recoverable f p
695recoverable (App f a) (App f' a')
696 | f == f' = recoverable a a'
697recoverable (App f a) (App f' a')
698 = recoverable f f' -- && recoverable a a'
699recoverable f (Bind _ (Pi _ _ _) sc)
700 | (P (DCon _ _ _) _ _, _) <- unApply f = False
701 | (P (TCon _ _) _ _, _) <- unApply f = False
702recoverable (Bind _ (Pi _ _ _) sc) f
703 | (P (DCon _ _ _) _ _, _) <- unApply f = False
704 | (P (TCon _ _) _ _, _) <- unApply f = False
705recoverable (Bind _ (Lam _) sc) f = recoverable sc f
706recoverable f (Bind _ (Lam _) sc) = recoverable f sc
707recoverable x y = True
709errEnv :: [(a, Binder b)] -> [(a, b)]
710errEnv = map (\(x, b) -> (x, binderTy b))
712holeIn :: Env -> Name -> Bool
713holeIn env n = case lookup n env of
714 Just (Hole _) -> True
715 Just (Guess _ _) -> True
716 _ -> False
718patIn :: Env -> Name -> Bool
719patIn env n = case lookup n env of
720 Just (PVar _) -> True
721 Just (PVTy _) -> True
722 _ -> False