git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/Unify.hs
715 lines 32 kB history raw
1{-|
2Module : Idris.Core.Unify
3Description : Idris' unification code.
5License : BSD3
6Maintainer : The Idris Community.
8Unification is applied inside the theorem prover. We're looking for holes
9which can be filled in, by matching one term's normal form against another.
10Returns a list of hole names paired with the term which solves them, and
11a list of things which need to be injective.
13-}
14{-# LANGUAGE FlexibleContexts, PatternGuards #-}
16module Idris.Core.Unify(
17 match_unify, unify
18 , Fails, FailContext(..), FailAt(..)
19 , unrecoverable
20 ) where
22import Idris.Core.Evaluate
23import Idris.Core.TT
25import Control.Monad.State.Strict
26import Data.List
27import Data.Maybe
29-- terms which need to be injective, with the things we're trying to unify
30-- at the time
31data FailAt = Match | Unify
32 deriving (Show, Eq)
34data FailContext = FailContext { fail_sourceloc :: FC,
35 fail_fn :: Name,
36 fail_param :: Name
37 }
38 deriving (Eq, Show)
40type Fails = [(TT Name, TT Name, -- unification error
41 Bool, -- ready to retry yet
42 Env, Err, [FailContext], FailAt)]
44unrecoverable :: Fails -> Bool
45unrecoverable = any bad
46 where bad (_,_,_,_, err, _, _) = unrec err
48 unrec (CantUnify r _ _ _ _ _) = not r
49 unrec (At _ e) = unrec e
50 unrec (Elaborating _ _ _ e) = unrec e
51 unrec (ElaboratingArg _ _ _ e) = unrec e
52 unrec _ = False
54data UInfo = UI Int Fails
55 deriving Show
57-- | Smart constructor for unification errors that takes into account the FailContext
58cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
59cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
60cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
61 At fc (ElaboratingArg f x
62 (map (\(FailContext _ f' x') -> (f', x')) prev)
63 (CantUnify r t1 t2 e ctxt i))
65-- Solve metavariables by matching terms against each other
66-- Not really unification, of course!
68match_unify :: Context -> Env ->
69 (TT Name, Maybe Provenance) ->
70 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
71 TC [(Name, TT Name)]
72match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
73 case runStateT (un [] (renameBindersTm env topx)
74 (renameBindersTm env topy)) (UI 0 []) of
75 OK (v, UI _ []) ->
76 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
77 return (map (renameBinders env) v')
78 res ->
79 let topxn = renameBindersTm env (normalise ctxt env topx)
80 topyn = renameBindersTm env (normalise ctxt env topy) in
81 case runStateT (un [] topxn topyn)
82 (UI 0 []) of
83 OK (v, UI _ fails) ->
84 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
85 return (map (renameBinders env) v')
86 Error e ->
87 -- just normalise the term we're matching against
88 case runStateT (un [] topxn topy)
89 (UI 0 []) of
90 OK (v, UI _ fails) ->
91 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
92 return (map (renameBinders env) v')
93 _ -> tfail e
94 where
95 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
96 StateT UInfo
97 TC [(Name, TT Name)]
99 un names tx@(P _ x _) tm
100 | tx /= tm && holeIn env x || x `elem` holes
101 = do sc 1; checkCycle names tx (x, tm)
102 un names tm ty@(P _ y _)
103 | ty /= tm && holeIn env y || y `elem` holes
104 = do sc 1; checkCycle names ty (y, tm)
105 un bnames (V i) (P _ x _)
106 | length bnames > i,
107 fst (fst (bnames!!i)) == x ||
108 snd (fst (bnames!!i)) == x = do sc 1; return []
109 un bnames (P _ x _) (V i)
110 | length bnames > i,
111 fst (fst (bnames!!i)) == x ||
112 snd (fst (bnames!!i)) == x = do sc 1; return []
113 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
114 = do h1 <- uB bnames bx by
115 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
116 combine bnames h1 h2
117 un names (App _ fx ax) (App _ fy ay)
118 = do hf <- un names fx fy
119 ha <- un names ax ay
120 combine names hf ha
121 un names x y
122 | OK True <- convEq' ctxt holes x y = do sc 1; return []
123 | otherwise = do UI s f <- get
124 let r = recoverable (normalise ctxt env x)
125 (normalise ctxt env y)
126 let err = cantUnify from r
127 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
128 if (not r) then lift $ tfail err
129 else do put (UI s ((x, y, True, env, err, from, Match) : f))
130 lift $ tfail err
133 uB bnames (Let _ tx vx) (Let _ ty vy)
134 = do h1 <- un bnames tx ty
135 h2 <- un bnames vx vy
136 combine bnames h1 h2
137 uB bnames (Lam _ tx) (Lam _ ty) = un bnames tx ty
138 uB bnames (Pi r i tx _) (Pi r' i' ty _) = un bnames tx ty
139 uB bnames x y = do UI s f <- get
140 let r = recoverable (normalise ctxt env (binderTy x))
141 (normalise ctxt env (binderTy y))
142 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
143 (CantUnify r (binderTy x, Nothing)
144 (binderTy y, Nothing) (Msg "") (errEnv env) s)
145 (errEnv env) s
146 put (UI s ((binderTy x, binderTy y,
147 False,
148 env, err, from, Match) : f))
149 return []
151 notHole (Hole _) = False
152 notHole _ = True
154 -- TODO: there's an annoying amount of repetition between this and the
155 -- main unification function. Consider lifting it out.
156 -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721
158 sc i = do UI s f <- get
159 put (UI (s+i) f)
161 unifyFail x y = do UI s f <- get
162 let r = recoverable (normalise ctxt env x)
163 (normalise ctxt env y)
164 let err = cantUnify from r
165 (topx, xfrom) (topy, yfrom)
166 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
167 put (UI s ((x, y, True, env, err, from, Match) : f))
168 lift $ tfail err
169 combine bnames as [] = return as
170 combine bnames as ((n, t) : bs)
171 = case lookup n as of
172 Nothing -> combine bnames (as ++ [(n,t)]) bs
173 Just t' -> do ns <- un bnames t t'
174 let ns' = filter (\ (x, _) -> x/=n) ns
175 sc 1
176 combine bnames as (ns' ++ bs)
178-- substN n tm (var, sol) = (var, subst n tm sol)
180 checkCycle ns xtm p@(x, P _ x' _) | x == x' = return []
181 checkCycle ns xtm p@(x, P _ _ _) = return [p]
182 checkCycle ns xtm (x, tm)
183 | conGuarded ctxt x tm = lift $ tfail (InfiniteUnify x tm (errEnv env))
184 | x `elem` freeNames tm = unifyFail xtm tm
185 | otherwise = checkScope ns (x, tm)
187 checkScope ns (x, tm) =
188 let v = highV (-1) tm in
189 if v >= length ns
190 then lift $ tfail (Msg "SCOPE ERROR")
191 else return [(x, bind v ns tm)]
193 bind i ns tm
194 | i < 0 = tm
195 | otherwise = let ((x,y),ty) = ns!!i in
196 App MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))
197 (P Bound x ty)
199renameBinders env (x, t) = (x, renameBindersTm env t)
201renameBindersTm :: Env -> TT Name -> TT Name
202renameBindersTm env tm = uniqueBinders (map fstEnv env) tm
203 where
204 uniqueBinders env (Bind n b sc)
205 | n `elem` env
206 = let n' = uniqueName n env in
207 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
208 (uniqueBinders (n':env) (rename n n' sc))
209 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
210 (uniqueBinders (n:env) sc)
211 uniqueBinders env (App s f a) = App s (uniqueBinders env f) (uniqueBinders env a)
212 uniqueBinders env t = t
214 rename n n' (P nt x ty) | n == x = P nt n' ty
215 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
216 rename n n' (App s f a) = App s (rename n n' f) (rename n n' a)
217 rename n n' t = t
219 explicitHole (Bind n (Hole ty) sc)
220 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
221 explicitHole t = t
223trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)
224 where dropPairs [] = []
225 dropPairs (n@(x, P _ x' _) : ns)
226 | x == x' = dropPairs ns
227 | otherwise
228 = n : dropPairs
229 (filter (\t -> case t of
230 (n, P _ n' _) -> not (n == x' && n' == x)
231 _ -> True) ns)
232 dropPairs (n : ns) = n : dropPairs ns
234 followSols vs [] = return []
235 followSols vs ((n, P _ t _) : ns)
236 | Just t' <- lookup t ns
237 = do vs' <- case t' of
238 P _ tn _ ->
239 if (n, tn) `elem` vs then -- cycle
240 tfail (cantUnify from False (topx, xfrom) (topy, yfrom)
241 (Msg "") (errEnv env) 0)
242 else return ((n, tn) : vs)
243 _ -> return vs
244 followSols vs' ((n, t') : ns)
245 followSols vs (n : ns) = do ns' <- followSols vs ns
246 return $ n : ns'
248unify :: Context -> Env ->
249 (TT Name, Maybe Provenance) ->
250 (TT Name, Maybe Provenance) ->
251 [Name] -> [Name] -> [Name] -> [FailContext] ->
252 TC ([(Name, TT Name)], Fails)
253unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
254-- traceWhen (hasv topx || hasv topy)
255-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
256 -- don't bother if topx and topy are different at the head
257 case runStateT (un False [] (renameBindersTm env topx)
258 (renameBindersTm env topy)) (UI 0 []) of
259 OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
260 return (map (renameBinders env) v', [])
261 res ->
262 let topxn = renameBindersTm env (normalise ctxt env topx)
263 topyn = renameBindersTm env (normalise ctxt env topy) in
264-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $
265 case runStateT (un False [] topxn topyn)
266 (UI 0 []) of
267 OK (v, UI _ fails) ->
268 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
269-- trace ("OK " ++ show (topxn, topyn, v, holes)) $
270 return (map (renameBinders env) v', reverse fails)
271-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
272 Error e -> tfail e
273 where
274 injective (P (DCon _ _ _) _ _) = True
275 injective (P (TCon _ _) _ _) = True
276-- injective (P Ref n _)
277-- | Just i <- lookupInjectiveExact n ctxt = i
278 injective (App _ f a) = injective f -- && injective a
279 injective _ = False
281-- injectiveTC (P Ref n _) (P Ref n' _)
282-- | Just i <- lookupInjectiveExact n ctxt,
283-- n == n' = i
284-- injectiveTC (App _ f a) (App _ f' a') = injectiveTC f a
285-- injectiveTC _ _ = False
287-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
288 injectiveVar (P _ n _) = n `elem` inj
289 injectiveVar (App _ f a) = injectiveVar f -- && injective a
290 injectiveVar _ = False
292 injectiveApp x = injective x || injectiveVar x
294 notP (P _ _ _) = False
295 notP _ = True
297 sc i = do UI s f <- get
298 put (UI (s+i) f)
300 uplus u1 u2 = do UI s f <- get
301 r <- u1
302 UI s f' <- get
303 if (length f == length f')
304 then return r
305 else do put (UI s f); u2
307 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
308 StateT UInfo
309 TC [(Name, TT Name)]
310 un = un' env
312 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
313 StateT UInfo
314 TC [(Name, TT Name)]
315 un' env fn names x y | x == y = return [] -- shortcut
316 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
317 | x /= y = unifyFail topx topy
318 un' env fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
319 | x /= y = unifyFail topx topy
320 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
321 = unifyFail topx topy
322 un' env fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
323 = unifyFail topx topy
324 un' env fn names topx@(Constant _) topy@(P (TCon _ _) y _)
325 = unifyFail topx topy
326 un' env fn names topx@(P (TCon _ _) x _) topy@(Constant _)
327 = unifyFail topx topy
328 un' env fn bnames tx@(P _ x _) ty@(P _ y _)
329 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
330 | injective tx && not (holeIn env y || y `elem` holes)
331 = unifyTmpFail tx ty
332 | injective ty && not (holeIn env x || x `elem` holes)
333 = unifyTmpFail tx ty
334 -- pick the one bound earliest if both are holes
335 | tx /= ty && (holeIn env x || x `elem` holes)
336 && (holeIn env y || y `elem` holes)
337 = case compare (envPos 0 x env) (envPos 0 y env) of
338 LT -> do sc 1; checkCycle bnames tx (x, ty)
339 _ -> do sc 1; checkCycle bnames ty (y, tx)
340 where envPos i n ((n',_,_):env) | n == n' = i
341 envPos i n (_:env) = envPos (i+1) n env
342 envPos _ _ _ = 100000
343 un' env fn bnames xtm@(P _ x _) tm
344 | pureTerm tm, holeIn env x || x `elem` holes
345 = do UI s f <- get
346 -- injectivity check
347 x <- checkCycle bnames xtm (x, tm)
348 if (notP tm && fn)
349-- trace (show (x, tm, normalise ctxt env tm)) $
350-- put (UI s ((tm, topx, topy) : i) f)
351 then unifyTmpFail xtm tm
352 else do sc 1
353 return x
354 | pureTerm tm, not (injective xtm) && injective tm
355 = do checkCycle bnames xtm (x, tm)
356 unifyTmpFail xtm tm
357 un' env fn bnames tm ytm@(P _ y _)
358 | pureTerm tm, holeIn env y || y `elem` holes
359 = do UI s f <- get
360 -- injectivity check
361 x <- checkCycle bnames ytm (y, tm)
362 if (notP tm && fn)
363-- trace (show (y, tm, normalise ctxt env tm)) $
364-- put (UI s ((tm, topx, topy) : i) f)
365 then unifyTmpFail tm ytm
366 else do sc 1
367 return x
368 | pureTerm tm, not (injective ytm) && injective tm
369 = do checkCycle bnames ytm (y, tm)
370 unifyTmpFail tm ytm
371 un' env fn bnames (V i) (P _ x _)
372 | length bnames > i,
373 fst ((map fst bnames)!!i) == x ||
374 snd ((map fst bnames)!!i) == x = do sc 1; return []
375 un' env fn bnames (P _ x _) (V i)
376 | length bnames > i,
377 fst ((map fst bnames)!!i) == x ||
378 snd ((map fst bnames)!!i) == x = do sc 1; return []
380 un' env fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
381 un' env fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
383-- Pattern unification rule
384 un' env fn bnames tm app@(App _ _ _)
385 | (mvtm@(P _ mv _), args) <- unApply app,
386 holeIn env mv || mv `elem` holes,
387 all rigid args,
388 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
389 -- && TODO: tm does not refer to any variables other than those
390 -- in 'args'
391 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
392 checkCycle bnames mvtm (mv, eta [] $ bindLams args (substEnv env tm))
393 where rigid (V i) = True
394 rigid (P _ t _) = t `elem` map fstEnv env &&
395 not (holeIn env t || t `elem` holes)
396 rigid _ = False
398 getV (V i) = Just i
399 getV _ = Nothing
401 getname (P _ n _) = Just n
402 getname _ = Nothing
404 containsOnly args vs (V i) = i `elem` vs
405 containsOnly args vs (P Bound n ty)
406 = n `elem` args && containsOnly args vs ty
407 containsOnly args vs (P _ n ty)
408 = not (holeIn env n || n `elem` holes)
409 && containsOnly args vs ty
410 containsOnly args vs (App _ f a)
411 = containsOnly args vs f && containsOnly args vs a
412 containsOnly args vs (Bind _ b sc)
413 = containsOnly args vs (binderTy b) &&
414 containsOnly args (0 : map (+1) vs) sc
415 containsOnly args vs _ = True
417 bindLams [] tm = tm
418 bindLams (a : as) tm = bindLam a (bindLams as tm)
420 bindLam (V i) tm = Bind (fstEnv (env !! i))
421 (Lam RigW (binderTy (sndEnv (env !! i))))
422 tm
423 bindLam (P _ n ty) tm = Bind n (Lam RigW ty) tm
424 bindLam _ tm = error "Can't happen [non rigid bindLam]"
426 substEnv [] tm = tm
427 substEnv ((n, _, t) : env) tm
428 = substEnv env (substV (P Bound n (binderTy t)) tm)
430 -- remove any unnecessary lambdas (helps with interface
431 -- resolution later).
432 eta ks (Bind n (Lam r ty) sc) = eta ((n, r, ty) : ks) sc
433 eta ks t = rebind ks t
435 rebind ((n, r, ty) : ks) (App _ f (P _ n' _))
436 | n == n' = eta ks f
437 rebind ((n, r, ty) : ks) t = rebind ks (Bind n (Lam r ty) t)
438 rebind _ t = t
440 un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)
441 = unApp env fn bnames appx appy
442-- = uplus (unApp fn bnames appx appy)
443-- (unifyTmpFail appx appy) -- take the whole lot
445 un' env fn bnames x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
446 | n == n' = un' env False bnames x y
447 un' env fn bnames (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
448 | n == n' = un' env False bnames x y
449 un' env fn bnames x (Bind n (Lam _ t) (App _ y (V 0)))
450 = un' env False bnames x y
451 un' env fn bnames (Bind n (Lam _ t) (App _ x (V 0))) y
452 = un' env False bnames x y
453-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
454-- = un' env False ((x,y):bnames) sx sy
455-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
456-- = un' env False ((x,y):bnames) sx sy
458 -- f D unifies with t -> D. This is dubious, but it helps with
459 -- interface resolution for interfaces over functions.
461 un' env fn bnames (App _ f x) (Bind n (Pi r i t k) y)
462 | noOccurrence n y && injectiveApp f
463 = do ux <- un' env False bnames x y
464 uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))
465 (Bind n (Pi r i t k) (V 1)))
466 combine env bnames ux uf
468 un' env fn bnames (Bind n (Pi r i t k) y) (App _ f x)
469 | noOccurrence n y && injectiveApp f
470 = do ux <- un' env False bnames y x
471 uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))
472 (Bind n (Pi r i t k) (V 1))) f
473 combine env bnames ux uf
475 un' env fn bnames (Bind x bx sx) (Bind y by sy)
476 | sameBinder bx by
477 = do h1 <- uB env bnames bx by
478 h2 <- un' ((x, RigW, bx) : env) False (((x,y),binderTy bx):bnames) sx sy
479 combine env bnames h1 h2
480 where sameBinder (Lam _ _) (Lam _ _) = True
481 sameBinder (Pi _ i _ _) (Pi _ i' _ _) = True
482 sameBinder _ _ = False -- never unify holes/guesses/etc
483 un' env fn bnames x y
484 | OK True <- convEq' ctxt holes x y = do sc 1; return []
485 | isUniverse x && isUniverse y = do sc 1; return []
486 | otherwise = do UI s f <- get
487 let r = recoverable (normalise ctxt env x)
488 (normalise ctxt env y)
489 let err = cantUnify from r
490 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
491 if (not r) then lift $ tfail err
492 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
493 return [] -- lift $ tfail err
495 unApp env fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
496 -- shortcut for the common case where we just want to check the
497 -- arguments are correct
498 | (injectiveApp fx && fx == fy)
499 = un' env False bnames ax ay
500 | (injectiveApp fx && injectiveApp fy)
501 || (injectiveApp fx && metavarApp fy && ax == ay)
502 || (injectiveApp fy && metavarApp fx && ax == ay)
503 || (injectiveTC fx fy) -- data interface method
504 = do let (headx, _) = unApply fx
505 let (heady, _) = unApply fy
506 -- fail quickly if the heads are disjoint
507 checkHeads headx heady
508 uplus
509 (do hf <- un' env True bnames fx fy
510 let ax' = hnormalise hf ctxt env (substNames hf ax)
511 let ay' = hnormalise hf ctxt env (substNames hf ay)
512 -- Don't normalise if we don't have to
513 ha <- uplus (un' env False bnames (substNames hf ax)
514 (substNames hf ay))
515 (un' env False bnames ax' ay')
516 sc 1
517 combine env bnames hf ha)
518 (do ha <- un' env False bnames ax ay
519 let fx' = hnormalise ha ctxt env (substNames ha fx)
520 let fy' = hnormalise ha ctxt env (substNames ha fy)
521 -- Don't normalise if we don't have to
522 hf <- uplus (un' env False bnames (substNames ha fx)
523 (substNames ha fy))
524 (un' env False bnames fx' fy')
525 sc 1
526 combine env bnames hf ha)
527 | otherwise = unifyTmpFail appx appy
528 where hnormalise [] _ _ t = t
529 hnormalise ns ctxt env t = normalise ctxt env t
530 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
531 | x /= y = unifyFail appx appy
532 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
533 | x /= y = unifyFail appx appy
534 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
535 = unifyFail appx appy
536 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
537 = unifyFail appx appy
538 checkHeads _ _ = return []
540 metavarApp tm = let (f, args) = unApply tm in
541 (metavar f &&
542 all (\x -> metavarApp x) args
543 && nub args == args) ||
544 globmetavar tm
546 globmetavar t = case unApply t of
547 (P _ x _, _) ->
548 case lookupDef x ctxt of
549 [TyDecl _ _] -> True
550 _ -> False
551 _ -> False
553 metavar t = case t of
554 P _ x _ -> (x `notElem` usersupp &&
555 (x `elem` holes || holeIn env x))
556 || globmetavar t
557 _ -> False
559 injectiveTC t@(P Ref n _) t'@(P Ref n' _)
560 | Just ni <- lookupInjectiveExact n ctxt,
561 Just ni' <- lookupInjectiveExact n' ctxt
562 = (n == n' && ni) ||
563 (ni && metavar t') ||
564 (metavar t && ni')
565 injectiveTC (App _ f a) (App _ f' a') = injectiveTC f f'
566 injectiveTC _ _ = False
569 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
570 unifyTmpFail x y
571 = do UI s f <- get
572 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
573 let err = cantUnify from r
574 (topx, xfrom) (topy, yfrom)
575 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
576 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
577 return []
579 -- shortcut failure, if we *know* nothing can fix it
580 unifyFail x y = do UI s f <- get
581 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
582 let err = cantUnify from r
583 (topx, xfrom) (topy, yfrom)
584 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
585 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
586 lift $ tfail err
589 uB env bnames (Let _ tx vx) (Let _ ty vy)
590 = do h1 <- un' env False bnames tx ty
591 h2 <- un' env False bnames vx vy
592 sc 1
593 combine env bnames h1 h2
594 uB env bnames (Guess tx vx) (Guess ty vy)
595 = do h1 <- un' env False bnames tx ty
596 h2 <- un' env False bnames vx vy
597 sc 1
598 combine env bnames h1 h2
599 uB env bnames (Lam _ tx) (Lam _ ty) = do sc 1; un' env False bnames tx ty
600 uB env bnames (Pi _ _ tx _) (Pi _ _ ty _) = do sc 1; un' env False bnames tx ty
601 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
602 uB env bnames (PVar _ tx) (PVar _ ty) = un' env False bnames tx ty
603 uB env bnames x y
604 = do UI s f <- get
605 let r = recoverable (normalise ctxt env (binderTy x))
606 (normalise ctxt env (binderTy y))
607 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
608 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
609 (errEnv env) s
610 put (UI s ((binderTy x, binderTy y,
611 False,
612 env, err, from, Unify) : f))
613 return [] -- lift $ tfail err
615 checkCycle ns xtm p@(x, P _ _ _) = return [p]
616 checkCycle ns xtm (x, tm)
617 | conGuarded ctxt x tm = lift $ tfail (InfiniteUnify x tm (errEnv env))
618 | x `elem` freeNames tm = unifyTmpFail xtm tm
619 | otherwise = checkScope ns (x, tm)
621 checkScope ns (x, tm) | pureTerm tm =
622 let v = highV (-1) tm in
623 if v >= length ns
624 then lift $ tfail (Msg "SCOPE ERROR")
625 else return [(x, bind v ns 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 MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))
632 (P Bound x ty)
634 combine env bnames as [] = return as
635 combine env bnames as ((n, t) : bs)
636 = case lookup n as of
637 Nothing -> combine env bnames (as ++ [(n,t)]) bs
638 Just t' -> do ns <- un' env False bnames t t'
639 -- make sure there's n mapping from n in ns
640 let ns' = filter (\ (x, _) -> x/=n) ns
641 sc 1
642 combine env bnames as (ns' ++ bs)
644highV :: Int -> Term -> Int
645highV i (V j) | j > i = j
646 | otherwise = i
647highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
648highV i (App _ f x) = max (highV i f) (highV i x)
649highV i _ = i
651-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
652-- more work may help.
653-- FIXME: Depending on how overloading gets used, this may cause problems. Better
654-- rethink overloading properly...
655-- ASSUMPTION: inputs are in normal form
656--
657-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
658--
659recoverable t@(App _ _ _) _
660 | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
661recoverable _ t@(App _ _ _)
662 | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
663recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
664recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
665recoverable (TType _) (P (DCon _ _ _) y _) = False
666recoverable (UType _) (P (DCon _ _ _) y _) = False
667recoverable (Constant _) (P (DCon _ _ _) y _) = False
668recoverable (Constant x) (Constant y) = x == y
669recoverable (P (DCon _ _ _) x _) (TType _) = False
670recoverable (P (DCon _ _ _) x _) (UType _) = False
671recoverable (P (DCon _ _ _) x _) (Constant _) = False
672recoverable (TType _) (P (TCon _ _) y _) = False
673recoverable (UType _) (P (TCon _ _) y _) = False
674recoverable (Constant _) (P (TCon _ _) y _) = False
675recoverable (P (TCon _ _) x _) (TType _) = False
676recoverable (P (TCon _ _) x _) (UType _) = False
677recoverable (P (TCon _ _) x _) (Constant _) = False
678recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
679recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
680recoverable p@(TType _) (App _ f a) = recoverable p f
681recoverable p@(UType _) (App _ f a) = recoverable p f
682recoverable p@(Constant _) (App _ f a) = recoverable p f
683recoverable (App _ f a) p@(TType _) = recoverable f p
684recoverable (App _ f a) p@(UType _) = recoverable f p
685recoverable (App _ f a) p@(Constant _) = recoverable f p
686recoverable p@(P _ n _) (App _ f a) = recoverable p f
687recoverable (App _ f a) p@(P _ _ _) = recoverable f p
688recoverable (App _ f a) (App _ f' a')
689 | f == f' = recoverable a a'
690recoverable (App _ f a) (App _ f' a')
691 = recoverable f f' -- && recoverable a a'
692recoverable f (Bind _ (Pi _ _ _ _) sc)
693 | (P (DCon _ _ _) _ _, _) <- unApply f = False
694 | (P (TCon _ _) _ _, _) <- unApply f = False
695 | (Constant _) <- f = False
696 | TType _ <- f = False
697 | UType _ <- f = False
698recoverable (Bind _ (Pi _ _ _ _) sc) f
699 | (P (DCon _ _ _) _ _, _) <- unApply f = False
700 | (P (TCon _ _) _ _, _) <- unApply f = False
701 | (Constant _) <- f = False
702 | TType _ <- f = False
703 | UType _ <- f = False
704recoverable (Bind _ (Lam _ _) sc) f = recoverable sc f
705recoverable f (Bind _ (Lam _ _) sc) = recoverable f sc
706recoverable x y = True
708errEnv :: [(a, r, Binder b)] -> [(a, b)]
709errEnv = map (\(x, _, b) -> (x, binderTy b))
711holeIn :: Env -> Name -> Bool
712holeIn env n = case lookupBinder n env of
713 Just (Hole _) -> True
714 Just (Guess _ _) -> True
715 _ -> False