git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Core/Unify.hs
804 lines 36 kB history raw
1{-|
2Module : Idris.Core.Unify
3Description : Idris' unification code.
4Copyright :
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 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
26import Control.Monad.State.Strict
27import Data.List
28import Data.Maybe
29import Debug.Trace
31-- terms which need to be injective, with the things we're trying to unify
32-- at the time
33data FailAt = Match | Unify
34 deriving (Show, Eq)
36data FailContext = FailContext { fail_sourceloc :: FC,
37 fail_fn :: Name,
38 fail_param :: Name
39 }
40 deriving (Eq, Show)
42type Injs = [(TT Name, TT Name, TT Name)]
43type Fails = [(TT Name, TT Name, -- unification error
44 Bool, -- ready to retry yet
45 Env, Err, [FailContext], FailAt)]
47unrecoverable :: Fails -> Bool
48unrecoverable = any bad
49 where bad (_,_,_,_, err, _, _) = unrec err
51 unrec (CantUnify r _ _ _ _ _) = not r
52 unrec (At _ e) = unrec e
53 unrec (Elaborating _ _ _ e) = unrec e
54 unrec (ElaboratingArg _ _ _ e) = unrec e
55 unrec _ = False
57data UInfo = UI Int Fails
58 deriving Show
60data UResult a = UOK a
61 | UPartOK a
62 | UFail Err
64-- | Smart constructor for unification errors that takes into account the FailContext
65cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
66cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
67cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
68 At fc (ElaboratingArg f x
69 (map (\(FailContext _ f' x') -> (f', x')) prev)
70 (CantUnify r t1 t2 e ctxt i))
72-- Solve metavariables by matching terms against each other
73-- Not really unification, of course!
75match_unify :: Context -> Env ->
76 (TT Name, Maybe Provenance) ->
77 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
78 TC [(Name, TT Name)]
79match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
80 case runStateT (un [] (renameBindersTm env topx)
81 (renameBindersTm env topy)) (UI 0 []) of
82 OK (v, UI _ []) ->
83 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
84 return (map (renameBinders env) v')
85 res ->
86 let topxn = renameBindersTm env (normalise ctxt env topx)
87 topyn = renameBindersTm env (normalise ctxt env topy) in
88 case runStateT (un [] topxn topyn)
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 Error e ->
94 -- just normalise the term we're matching against
95 case runStateT (un [] topxn topy)
96 (UI 0 []) of
97 OK (v, UI _ fails) ->
98 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
99 return (map (renameBinders env) v')
100 _ -> tfail e
101 where
102 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
103 StateT UInfo
104 TC [(Name, TT Name)]
106 un names tx@(P _ x _) tm
107 | tx /= tm && holeIn env x || x `elem` holes
108 = do sc 1; checkCycle names tx (x, tm)
109 un names tm ty@(P _ y _)
110 | ty /= tm && holeIn env y || y `elem` holes
111 = do sc 1; checkCycle names ty (y, tm)
112 un bnames (V i) (P _ x _)
113 | length bnames > i,
114 fst (fst (bnames!!i)) == x ||
115 snd (fst (bnames!!i)) == x = do sc 1; return []
116 un bnames (P _ x _) (V i)
117 | length bnames > i,
118 fst (fst (bnames!!i)) == x ||
119 snd (fst (bnames!!i)) == x = do sc 1; return []
120 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
121 = do h1 <- uB bnames bx by
122 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
123 combine bnames h1 h2
124 un names (App _ fx ax) (App _ fy ay)
125 = do hf <- un names fx fy
126 ha <- un names ax ay
127 combine names hf ha
128 un names x y
129 | OK True <- convEq' ctxt holes x y = do sc 1; return []
130 | otherwise = do UI s f <- get
131 let r = recoverable (normalise ctxt env x)
132 (normalise ctxt env y)
133 let err = cantUnify from r
134 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
135 if (not r) then lift $ tfail err
136 else do put (UI s ((x, y, True, env, err, from, Match) : f))
137 lift $ tfail err
140 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
141 h2 <- un bnames vx vy
142 combine bnames h1 h2
143 uB bnames (Lam _ tx) (Lam _ ty) = un bnames tx ty
144 uB bnames (Pi r i tx _) (Pi r' i' ty _) = un bnames tx ty
145 uB bnames x y = do UI s f <- get
146 let r = recoverable (normalise ctxt env (binderTy x))
147 (normalise ctxt env (binderTy y))
148 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
149 (CantUnify r (binderTy x, Nothing)
150 (binderTy y, Nothing) (Msg "") (errEnv env) s)
151 (errEnv env) s
152 put (UI s ((binderTy x, binderTy y,
153 False,
154 env, err, from, Match) : f))
155 return []
157 notHole (Hole _) = False
158 notHole _ = True
160 -- TODO: there's an annoying amount of repetition between this and the
161 -- main unification function. Consider lifting it out.
162 -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721
164 sc i = do UI s f <- get
165 put (UI (s+i) f)
167 unifyFail x y = do UI s f <- get
168 let r = recoverable (normalise ctxt env x)
169 (normalise ctxt env y)
170 let err = cantUnify from r
171 (topx, xfrom) (topy, yfrom)
172 (CantUnify r (x, Nothing) (y, Nothing) (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 xtm p@(x, P _ x' _) | x == x' = return []
187 checkCycle ns xtm p@(x, P _ _ _) = return [p]
188 checkCycle ns xtm (x, tm)
189 | conGuarded ctxt x tm = lift $ tfail (InfiniteUnify x tm (errEnv env))
190 | x `elem` freeNames tm = unifyFail xtm tm
191 | otherwise = checkScope ns (x, tm)
193 checkScope ns (x, tm) =
194-- case boundVs (envPos x 0 env) tm of
195-- [] -> return [(x, tm)]
196-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
197-- (impl ns tm) (errEnv env))
198 let v = highV (-1) tm in
199 if v >= length ns
200 then lift $ tfail (Msg "SCOPE ERROR")
201 else return [(x, bind v ns tm)]
202 where impl [] tm = tm
203 impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
205 bind i ns tm
206 | i < 0 = tm
207 | otherwise = let ((x,y),ty) = ns!!i in
208 App MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))
209 (P Bound x ty)
211renameBinders env (x, t) = (x, renameBindersTm env t)
213renameBindersTm :: Env -> TT Name -> TT Name
214renameBindersTm env tm = uniqueBinders (map fstEnv env) tm
215 where
216 uniqueBinders env (Bind n b sc)
217 | n `elem` env
218 = let n' = uniqueName n env in
219 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
220 (uniqueBinders (n':env) (rename n n' sc))
221 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
222 (uniqueBinders (n:env) sc)
223 uniqueBinders env (App s f a) = App s (uniqueBinders env f) (uniqueBinders env a)
224 uniqueBinders env t = t
226 rename n n' (P nt x ty) | n == x = P nt n' ty
227 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
228 rename n n' (App s f a) = App s (rename n n' f) (rename n n' a)
229 rename n n' t = t
231 explicitHole (Bind n (Hole ty) sc)
232 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
233 explicitHole t = t
235trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)
236 where dropPairs [] = []
237 dropPairs (n@(x, P _ x' _) : ns)
238 | x == x' = dropPairs ns
239 | otherwise
240 = n : dropPairs
241 (filter (\t -> case t of
242 (n, P _ n' _) -> not (n == x' && n' == x)
243 _ -> True) ns)
244 dropPairs (n : ns) = n : dropPairs ns
246 followSols vs [] = return []
247 followSols vs ((n, P _ t _) : ns)
248 | Just t' <- lookup t ns
249 = do vs' <- case t' of
250 P _ tn _ ->
251 if (n, tn) `elem` vs then -- cycle
252 tfail (cantUnify from False (topx, xfrom) (topy, yfrom)
253 (Msg "") (errEnv env) 0)
254 else return ((n, tn) : vs)
255 _ -> return vs
256 followSols vs' ((n, t') : ns)
257 followSols vs (n : ns) = do ns' <- followSols vs ns
258 return $ n : ns'
260expandLets env (x, tm) = (x, doSubst (reverse env) tm)
261 where
262 doSubst [] tm = tm
263 doSubst ((n, Let v t) : env) tm
264 = doSubst env (subst n v tm)
265 doSubst (_ : env) tm
266 = doSubst env tm
268hasv :: TT Name -> Bool
269hasv (V x) = True
270hasv (App _ f a) = hasv f || hasv a
271hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
272hasv _ = False
274unify :: Context -> Env ->
275 (TT Name, Maybe Provenance) ->
276 (TT Name, Maybe Provenance) ->
277 [Name] -> [Name] -> [Name] -> [FailContext] ->
278 TC ([(Name, TT Name)], Fails)
279unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
280-- traceWhen (hasv topx || hasv topy)
281-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
282 -- don't bother if topx and topy are different at the head
283 case runStateT (un False [] (renameBindersTm env topx)
284 (renameBindersTm env topy)) (UI 0 []) of
285 OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
286 return (map (renameBinders env) v', [])
287 res ->
288 let topxn = renameBindersTm env (normalise ctxt env topx)
289 topyn = renameBindersTm env (normalise ctxt env topy) in
290-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $
291 case runStateT (un False [] topxn topyn)
292 (UI 0 []) of
293 OK (v, UI _ fails) ->
294 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
295-- trace ("OK " ++ show (topxn, topyn, v, holes)) $
296 return (map (renameBinders env) v', reverse fails)
297-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
298 Error e -> tfail e
299 where
300 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
301 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
302 headDiff _ _ = False
304 injective (P (DCon _ _ _) _ _) = True
305 injective (P (TCon _ _) _ _) = True
306-- injective (P Ref n _)
307-- | Just i <- lookupInjectiveExact n ctxt = i
308 injective (App _ f a) = injective f -- && injective a
309 injective _ = False
311-- injectiveTC (P Ref n _) (P Ref n' _)
312-- | Just i <- lookupInjectiveExact n ctxt,
313-- n == n' = i
314-- injectiveTC (App _ f a) (App _ f' a') = injectiveTC f a
315-- injectiveTC _ _ = 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' env
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' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
353 StateT UInfo
354 TC [(Name, TT Name)]
355 un' env fn names x y | x == y = return [] -- shortcut
356 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
357 | x /= y = unifyFail topx topy
358 un' env fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
359 | x /= y = unifyFail topx topy
360 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
361 = unifyFail topx topy
362 un' env fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
363 = unifyFail topx topy
364 un' env fn names topx@(Constant _) topy@(P (TCon _ _) y _)
365 = unifyFail topx topy
366 un' env fn names topx@(P (TCon _ _) x _) topy@(Constant _)
367 = unifyFail topx topy
368 un' env 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 tx (x, ty)
379 _ -> do sc 1; checkCycle bnames ty (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' env 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 xtm (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 xtm (x, tm)
396 unifyTmpFail xtm tm
397 un' env 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 ytm (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 ytm (y, tm)
410 unifyTmpFail tm ytm
411 un' env 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' env 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' env fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
421 un' env fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
423-- Pattern unification rule
424 un' env fn bnames tm app@(App _ _ _)
425 | (mvtm@(P _ mv _), args) <- unApply app,
426 holeIn env mv || mv `elem` holes,
427 all rigid args,
428 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
429 -- && TODO: tm does not refer to any variables other than those
430 -- in 'args'
431 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
432 checkCycle bnames mvtm (mv, eta [] $ bindLams args (substEnv env tm))
433 where rigid (V i) = True
434 rigid (P _ t _) = t `elem` map fstEnv env &&
435 not (holeIn env t || t `elem` holes)
436 rigid _ = False
438 getV (V i) = Just i
439 getV _ = Nothing
441 getname (P _ n _) = Just n
442 getname _ = Nothing
444 containsOnly args vs (V i) = i `elem` vs
445 containsOnly args vs (P Bound n ty)
446 = n `elem` args && containsOnly args vs ty
447 containsOnly args vs (P _ n ty)
448 = not (holeIn env n || n `elem` holes)
449 && containsOnly args vs ty
450 containsOnly args vs (App _ f a)
451 = containsOnly args vs f && containsOnly args vs a
452 containsOnly args vs (Bind _ b sc)
453 = containsOnly args vs (binderTy b) &&
454 containsOnly args (0 : map (+1) vs) sc
455 containsOnly args vs _ = True
457 bindLams [] tm = tm
458 bindLams (a : as) tm = bindLam a (bindLams as tm)
460 bindLam (V i) tm = Bind (fstEnv (env !! i))
461 (Lam RigW (binderTy (sndEnv (env !! i))))
462 tm
463 bindLam (P _ n ty) tm = Bind n (Lam RigW ty) tm
464 bindLam _ tm = error "Can't happen [non rigid bindLam]"
466 substEnv [] tm = tm
467 substEnv ((n, _, t) : env) tm
468 = substEnv env (substV (P Bound n (binderTy t)) tm)
470 -- remove any unnecessary lambdas (helps with interface
471 -- resolution later).
472 eta ks (Bind n (Lam r ty) sc) = eta ((n, r, ty) : ks) sc
473 eta ks t = rebind ks t
475 rebind ((n, r, ty) : ks) (App _ f (P _ n' _))
476 | n == n' = eta ks f
477 rebind ((n, r, ty) : ks) t = rebind ks (Bind n (Lam r ty) t)
478 rebind _ t = t
480 un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)
481 = unApp env fn bnames appx appy
482-- = uplus (unApp fn bnames appx appy)
483-- (unifyTmpFail appx appy) -- take the whole lot
485 un' env fn bnames x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
486 | n == n' = un' env False bnames x y
487 un' env fn bnames (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
488 | n == n' = un' env False bnames x y
489 un' env fn bnames x (Bind n (Lam _ t) (App _ y (V 0)))
490 = un' env False bnames x y
491 un' env fn bnames (Bind n (Lam _ t) (App _ x (V 0))) y
492 = un' env False bnames x y
493-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
494-- = un' env False ((x,y):bnames) sx sy
495-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
496-- = un' env False ((x,y):bnames) sx sy
498 -- f D unifies with t -> D. This is dubious, but it helps with
499 -- interface resolution for interfaces over functions.
501 un' env fn bnames (App _ f x) (Bind n (Pi r i t k) y)
502 | noOccurrence n y && injectiveApp f
503 = do ux <- un' env False bnames x y
504 uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))
505 (Bind n (Pi r i t k) (V 1)))
506 combine env bnames ux uf
508 un' env fn bnames (Bind n (Pi r i t k) y) (App _ f x)
509 | noOccurrence n y && injectiveApp f
510 = do ux <- un' env False bnames y x
511 uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))
512 (Bind n (Pi r i t k) (V 1))) f
513 combine env bnames ux uf
515 un' env fn bnames (Bind x bx sx) (Bind y by sy)
516 | sameBinder bx by
517 = do h1 <- uB env bnames bx by
518 h2 <- un' ((x, RigW, bx) : env) False (((x,y),binderTy bx):bnames) sx sy
519 combine env bnames h1 h2
520 where sameBinder (Lam _ _) (Lam _ _) = True
521 sameBinder (Pi _ i _ _) (Pi _ i' _ _) = True
522 sameBinder _ _ = False -- never unify holes/guesses/etc
523 un' env fn bnames x y
524 | OK True <- convEq' ctxt holes x y = do sc 1; return []
525 | isUniverse x && isUniverse y = do sc 1; return []
526 | otherwise = do UI s f <- get
527 let r = recoverable (normalise ctxt env x)
528 (normalise ctxt env y)
529 let err = cantUnify from r
530 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
531 if (not r) then lift $ tfail err
532 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
533 return [] -- lift $ tfail err
535 unApp env fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
536 -- shortcut for the common case where we just want to check the
537 -- arguments are correct
538 | (injectiveApp fx && fx == fy)
539 = un' env False bnames ax ay
540 | (injectiveApp fx && injectiveApp fy)
541 || (injectiveApp fx && metavarApp fy && ax == ay)
542 || (injectiveApp fy && metavarApp fx && ax == ay)
543 || (injectiveTC fx fy) -- data interface method
544 = do let (headx, _) = unApply fx
545 let (heady, _) = unApply fy
546 -- fail quickly if the heads are disjoint
547 checkHeads headx heady
548 uplus
549 (do hf <- un' env True bnames fx fy
550 let ax' = hnormalise hf ctxt env (substNames hf ax)
551 let ay' = hnormalise hf ctxt env (substNames hf ay)
552 -- Don't normalise if we don't have to
553 ha <- uplus (un' env False bnames (substNames hf ax)
554 (substNames hf ay))
555 (un' env False bnames ax' ay')
556 sc 1
557 combine env bnames hf ha)
558 (do ha <- un' env False bnames ax ay
559 let fx' = hnormalise ha ctxt env (substNames ha fx)
560 let fy' = hnormalise ha ctxt env (substNames ha fy)
561 -- Don't normalise if we don't have to
562 hf <- uplus (un' env False bnames (substNames ha fx)
563 (substNames ha fy))
564 (un' env False bnames fx' fy')
565 sc 1
566 combine env bnames hf ha)
567 | otherwise = unifyTmpFail appx appy
568 where hnormalise [] _ _ t = t
569 hnormalise ns ctxt env t = normalise ctxt env t
570 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
571 | x /= y = unifyFail appx appy
572 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
573 | x /= y = unifyFail appx appy
574 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
575 = unifyFail appx appy
576 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
577 = unifyFail appx appy
578 checkHeads _ _ = return []
580 numArgs tm = let (f, args) = unApply tm in length args
582 metavarApp tm = let (f, args) = unApply tm in
583 (metavar f &&
584 all (\x -> metavarApp x) args
585 && nub args == args) ||
586 globmetavar tm
587 metavarArgs tm = let (f, args) = unApply tm in
588 all (\x -> metavar x || inenv x) args
589 && nub args == args
590 metavarApp' tm = let (f, args) = unApply tm in
591 all (\x -> pat x || metavar x) (f : args)
592 && nub args == args
594 rigid (P (DCon _ _ _) _ _) = True
595 rigid (P (TCon _ _) _ _) = True
596 rigid t@(P Ref _ _) = inenv t || globmetavar t
597 rigid (Constant _) = True
598 rigid (App _ f a) = rigid f && rigid a
599 rigid t = not (metavar t) || globmetavar t
601 globmetavar t = case unApply t of
602 (P _ x _, _) ->
603 case lookupDef x ctxt of
604 [TyDecl _ _] -> True
605 _ -> False
606 _ -> False
608 metavar t = case t of
609 P _ x _ -> (x `notElem` usersupp &&
610 (x `elem` holes || holeIn env x))
611 || globmetavar t
612 _ -> False
613 pat t = case t of
614 P _ x _ -> x `elem` holes || patIn env x
615 _ -> False
616 inenv t = case t of
617 P _ x _ -> x `elem` (map fstEnv env)
618 _ -> False
620 notFn t = injective t || metavar t || inenv t
622 injectiveTC t@(P Ref n _) t'@(P Ref n' _)
623 | Just ni <- lookupInjectiveExact n ctxt,
624 Just ni' <- lookupInjectiveExact n' ctxt
625 = (n == n' && ni) ||
626 (ni && metavar t') ||
627 (metavar t && ni')
628 injectiveTC (App _ f a) (App _ f' a') = injectiveTC f f'
629 injectiveTC _ _ = False
632 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
633 unifyTmpFail x y
634 = do UI s f <- get
635 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
636 let err = cantUnify from r
637 (topx, xfrom) (topy, yfrom)
638 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
639 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
640 return []
642 -- shortcut failure, if we *know* nothing can fix it
643 unifyFail x y = do UI s f <- get
644 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
645 let err = cantUnify from r
646 (topx, xfrom) (topy, yfrom)
647 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
648 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
649 lift $ tfail err
652 uB env bnames (Let tx vx) (Let ty vy)
653 = do h1 <- un' env False bnames tx ty
654 h2 <- un' env False bnames vx vy
655 sc 1
656 combine env bnames h1 h2
657 uB env bnames (Guess tx vx) (Guess ty vy)
658 = do h1 <- un' env False bnames tx ty
659 h2 <- un' env False bnames vx vy
660 sc 1
661 combine env bnames h1 h2
662 uB env bnames (Lam _ tx) (Lam _ ty) = do sc 1; un' env False bnames tx ty
663 uB env bnames (Pi _ _ tx _) (Pi _ _ ty _) = do sc 1; un' env False bnames tx ty
664 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
665 uB env bnames (PVar _ tx) (PVar _ ty) = un' env False bnames tx ty
666 uB env bnames x y
667 = do UI s f <- get
668 let r = recoverable (normalise ctxt env (binderTy x))
669 (normalise ctxt env (binderTy y))
670 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
671 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
672 (errEnv env) s
673 put (UI s ((binderTy x, binderTy y,
674 False,
675 env, err, from, Unify) : f))
676 return [] -- lift $ tfail err
678 checkCycle ns xtm p@(x, P _ _ _) = return [p]
679 checkCycle ns xtm (x, tm)
680 | conGuarded ctxt x tm = lift $ tfail (InfiniteUnify x tm (errEnv env))
681 | x `elem` freeNames tm = unifyTmpFail xtm tm
682 | otherwise = checkScope ns (x, tm)
684 checkScope ns (x, tm) | pureTerm tm =
685-- case boundVs (envPos x 0 env) tm of
686-- [] -> return [(x, tm)]
687-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
688-- (impl ns tm) (errEnv env))
689 let v = highV (-1) tm in
690 if v >= length ns
691 then lift $ tfail (Msg "SCOPE ERROR")
692 else return [(x, bind v ns tm)]
693 where impl [] tm = tm
694 impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
695 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
697 bind i ns tm
698 | i < 0 = tm
699 | otherwise = let ((x,y),ty) = ns!!i in
700 App MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))
701 (P Bound x ty)
703 combine env bnames as [] = return as
704 combine env bnames as ((n, t) : bs)
705 = case lookup n as of
706 Nothing -> combine env bnames (as ++ [(n,t)]) bs
707 Just t' -> do ns <- un' env False bnames t t'
708 -- make sure there's n mapping from n in ns
709 let ns' = filter (\ (x, _) -> x/=n) ns
710 sc 1
711 combine env bnames as (ns' ++ bs)
713boundVs :: Int -> Term -> [Int]
714boundVs i (V j) | j < i = []
715 | otherwise = [j]
716boundVs i (Bind n b sc) = boundVs (i + 1) sc
717boundVs i (App _ f x) = let fs = boundVs i f
718 xs = boundVs i x in
719 nub (fs ++ xs)
720boundVs i _ = []
722highV :: Int -> Term -> Int
723highV i (V j) | j > i = j
724 | otherwise = i
725highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
726highV i (App _ f x) = max (highV i f) (highV i x)
727highV i _ = i
729envPos x i [] = 0
730envPos x i ((y, _) : ys) | x == y = i
731 | otherwise = envPos x (i + 1) ys
734-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
735-- more work may help.
736-- FIXME: Depending on how overloading gets used, this may cause problems. Better
737-- rethink overloading properly...
738-- ASSUMPTION: inputs are in normal form
739--
740-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
741--
742recoverable t@(App _ _ _) _
743 | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
744recoverable _ t@(App _ _ _)
745 | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
746recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
747recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
748recoverable (TType _) (P (DCon _ _ _) y _) = False
749recoverable (UType _) (P (DCon _ _ _) y _) = False
750recoverable (Constant _) (P (DCon _ _ _) y _) = False
751recoverable (Constant x) (Constant y) = x == y
752recoverable (P (DCon _ _ _) x _) (TType _) = False
753recoverable (P (DCon _ _ _) x _) (UType _) = False
754recoverable (P (DCon _ _ _) x _) (Constant _) = False
755recoverable (TType _) (P (TCon _ _) y _) = False
756recoverable (UType _) (P (TCon _ _) y _) = False
757recoverable (Constant _) (P (TCon _ _) y _) = False
758recoverable (P (TCon _ _) x _) (TType _) = False
759recoverable (P (TCon _ _) x _) (UType _) = False
760recoverable (P (TCon _ _) x _) (Constant _) = False
761recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
762recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
763recoverable p@(TType _) (App _ f a) = recoverable p f
764recoverable p@(UType _) (App _ f a) = recoverable p f
765recoverable p@(Constant _) (App _ f a) = recoverable p f
766recoverable (App _ f a) p@(TType _) = recoverable f p
767recoverable (App _ f a) p@(UType _) = recoverable f p
768recoverable (App _ f a) p@(Constant _) = recoverable f p
769recoverable p@(P _ n _) (App _ f a) = recoverable p f
770recoverable (App _ f a) p@(P _ _ _) = recoverable f p
771recoverable (App _ f a) (App _ f' a')
772 | f == f' = recoverable a a'
773recoverable (App _ f a) (App _ f' a')
774 = recoverable f f' -- && recoverable a a'
775recoverable f (Bind _ (Pi _ _ _ _) sc)
776 | (P (DCon _ _ _) _ _, _) <- unApply f = False
777 | (P (TCon _ _) _ _, _) <- unApply f = False
778 | (Constant _) <- f = False
779 | TType _ <- f = False
780 | UType _ <- f = False
781recoverable (Bind _ (Pi _ _ _ _) sc) f
782 | (P (DCon _ _ _) _ _, _) <- unApply f = False
783 | (P (TCon _ _) _ _, _) <- unApply f = False
784 | (Constant _) <- f = False
785 | TType _ <- f = False
786 | UType _ <- f = False
787recoverable (Bind _ (Lam _ _) sc) f = recoverable sc f
788recoverable f (Bind _ (Lam _ _) sc) = recoverable f sc
789recoverable x y = True
791errEnv :: [(a, r, Binder b)] -> [(a, b)]
792errEnv = map (\(x, _, b) -> (x, binderTy b))
794holeIn :: Env -> Name -> Bool
795holeIn env n = case lookupBinder n env of
796 Just (Hole _) -> True
797 Just (Guess _ _) -> True
798 _ -> False
800patIn :: Env -> Name -> Bool
801patIn env n = case lookupBinder n env of
802 Just (PVar _ _) -> True
803 Just (PVTy _) -> True
804 _ -> False