git.iko.soy/Idris-dev
on 008fb1f help sign in
Idris-dev/src/Idris/Core/Unify.hs
786 lines 35 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 (x, tm)
109 un names tm ty@(P _ y _)
110 | ty /= tm && holeIn env y || y `elem` holes
111 = do sc 1; checkCycle names (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 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-- (impl 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 impl [] tm = tm
202 impl ((n, _) : ns) tm = impl 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 MaybeHoles (Bind y (Lam RigW 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 fstEnv 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 s f a) = App s (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 s f a) = App s (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, xfrom) (topy, yfrom) 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, xfrom) (topy, yfrom)
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 ->
274 (TT Name, Maybe Provenance) ->
275 (TT Name, Maybe Provenance) ->
276 [Name] -> [Name] -> [Name] -> [FailContext] ->
277 TC ([(Name, TT Name)], Fails)
278unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
279-- traceWhen (hasv topx || hasv topy)
280-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
281 -- don't bother if topx and topy are different at the head
282 case runStateT (un False [] (renameBindersTm env topx)
283 (renameBindersTm env topy)) (UI 0 []) of
284 OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
285 return (map (renameBinders env) v', [])
286 res ->
287 let topxn = renameBindersTm env (normalise ctxt env topx)
288 topyn = renameBindersTm env (normalise ctxt env topy) in
289-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $
290 case runStateT (un False [] topxn topyn)
291 (UI 0 []) of
292 OK (v, UI _ fails) ->
293 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
294-- trace ("OK " ++ show (topxn, topyn, v, holes)) $
295 return (map (renameBinders env) v', reverse fails)
296-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
297 Error e -> tfail e
298 where
299 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
300 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
301 headDiff _ _ = False
303 injective (P (DCon _ _ _) _ _) = True
304 injective (P (TCon _ _) _ _) = True
305 injective (P Ref n _)
306 | Just i <- lookupInjectiveExact n ctxt = i
307 injective (App _ f a) = injective f -- && injective a
308 injective _ = False
310-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
311 injectiveVar (P _ n _) = n `elem` inj
312 injectiveVar (App _ f a) = injectiveVar f -- && injective a
313 injectiveVar _ = False
315 injectiveApp x = injective x || injectiveVar x
317 notP (P _ _ _) = False
318 notP _ = True
320 sc i = do UI s f <- get
321 put (UI (s+i) f)
323 errors :: StateT UInfo TC Bool
324 errors = do UI s f <- get
325 return (not (null f))
327 uplus u1 u2 = do UI s f <- get
328 r <- u1
329 UI s f' <- get
330 if (length f == length f')
331 then return r
332 else do put (UI s f); u2
334 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
335 StateT UInfo
336 TC [(Name, TT Name)]
337 un = un' env
338-- un fn names x y
339-- = let (xf, _) = unApply x
340-- (yf, _) = unApply y in
341-- if headDiff xf yf then unifyFail x y else
342-- uplus (un' fn names x y)
343-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
345 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
346 StateT UInfo
347 TC [(Name, TT Name)]
348 un' env fn names x y | x == y = return [] -- shortcut
349 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
350 | x /= y = unifyFail topx topy
351 un' env fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
352 | x /= y = unifyFail topx topy
353 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
354 = unifyFail topx topy
355 un' env fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
356 = unifyFail topx topy
357 un' env fn names topx@(Constant _) topy@(P (TCon _ _) y _)
358 = unifyFail topx topy
359 un' env fn names topx@(P (TCon _ _) x _) topy@(Constant _)
360 = unifyFail topx topy
361 un' env fn bnames tx@(P _ x _) ty@(P _ y _)
362 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
363 | injective tx && not (holeIn env y || y `elem` holes)
364 = unifyTmpFail tx ty
365 | injective ty && not (holeIn env x || x `elem` holes)
366 = unifyTmpFail tx ty
367 -- pick the one bound earliest if both are holes
368 | tx /= ty && (holeIn env x || x `elem` holes)
369 && (holeIn env y || y `elem` holes)
370 = case compare (envPos 0 x env) (envPos 0 y env) of
371 LT -> do sc 1; checkCycle bnames (x, ty)
372 _ -> do sc 1; checkCycle bnames (y, tx)
373 where envPos i n ((n',_,_):env) | n == n' = i
374 envPos i n (_:env) = envPos (i+1) n env
375 envPos _ _ _ = 100000
376 un' env fn bnames xtm@(P _ x _) tm
377 | pureTerm tm, holeIn env x || x `elem` holes
378 = do UI s f <- get
379 -- injectivity check
380 x <- checkCycle bnames (x, tm)
381 if (notP tm && fn)
382-- trace (show (x, tm, normalise ctxt env tm)) $
383-- put (UI s ((tm, topx, topy) : i) f)
384 then unifyTmpFail xtm tm
385 else do sc 1
386 return x
387 | pureTerm tm, not (injective xtm) && injective tm
388 = do checkCycle bnames (x, tm)
389 unifyTmpFail xtm tm
390 un' env fn bnames tm ytm@(P _ y _)
391 | pureTerm tm, holeIn env y || y `elem` holes
392 = do UI s f <- get
393 -- injectivity check
394 x <- checkCycle bnames (y, tm)
395 if (notP tm && fn)
396-- trace (show (y, tm, normalise ctxt env tm)) $
397-- put (UI s ((tm, topx, topy) : i) f)
398 then unifyTmpFail tm ytm
399 else do sc 1
400 return x
401 | pureTerm tm, not (injective ytm) && injective tm
402 = do checkCycle bnames (y, tm)
403 unifyTmpFail tm ytm
404 un' env fn bnames (V i) (P _ x _)
405 | length bnames > i,
406 fst ((map fst bnames)!!i) == x ||
407 snd ((map fst bnames)!!i) == x = do sc 1; return []
408 un' env fn bnames (P _ x _) (V i)
409 | length bnames > i,
410 fst ((map fst bnames)!!i) == x ||
411 snd ((map fst bnames)!!i) == x = do sc 1; return []
413 un' env fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
414 un' env fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
416-- Pattern unification rule
417 un' env fn bnames tm app@(App _ _ _)
418 | (P _ mv _, args) <- unApply app,
419 holeIn env mv || mv `elem` holes,
420 all rigid args,
421 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
422 -- && TODO: tm does not refer to any variables other than those
423 -- in 'args'
424 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
425 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))
426 where rigid (V i) = True
427 rigid (P _ t _) = t `elem` map fstEnv env &&
428 not (holeIn env t || t `elem` holes)
429 rigid _ = False
431 getV (V i) = Just i
432 getV _ = Nothing
434 getname (P _ n _) = Just n
435 getname _ = Nothing
437 containsOnly args vs (V i) = i `elem` vs
438 containsOnly args vs (P Bound n ty)
439 = n `elem` args && containsOnly args vs ty
440 containsOnly args vs (P _ n ty)
441 = not (holeIn env n || n `elem` holes)
442 && containsOnly args vs ty
443 containsOnly args vs (App _ f a)
444 = containsOnly args vs f && containsOnly args vs a
445 containsOnly args vs (Bind _ b sc)
446 = containsOnly args vs (binderTy b) &&
447 containsOnly args (0 : map (+1) vs) sc
448 containsOnly args vs _ = True
450 bindLams [] tm = tm
451 bindLams (a : as) tm = bindLam a (bindLams as tm)
453 bindLam (V i) tm = Bind (fstEnv (env !! i))
454 (Lam RigW (binderTy (sndEnv (env !! i))))
455 tm
456 bindLam (P _ n ty) tm = Bind n (Lam RigW ty) tm
457 bindLam _ tm = error "Can't happen [non rigid bindLam]"
459 substEnv [] tm = tm
460 substEnv ((n, _, t) : env) tm
461 = substEnv env (substV (P Bound n (binderTy t)) tm)
463 -- remove any unnecessary lambdas (helps with interface
464 -- resolution later).
465 eta ks (Bind n (Lam r ty) sc) = eta ((n, r, ty) : ks) sc
466 eta ks t = rebind ks t
468 rebind ((n, r, ty) : ks) (App _ f (P _ n' _))
469 | n == n' = eta ks f
470 rebind ((n, r, ty) : ks) t = rebind ks (Bind n (Lam r ty) t)
471 rebind _ t = t
473 un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)
474 = unApp env fn bnames appx appy
475-- = uplus (unApp fn bnames appx appy)
476-- (unifyTmpFail appx appy) -- take the whole lot
478 un' env fn bnames x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
479 | n == n' = un' env False bnames x y
480 un' env fn bnames (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
481 | n == n' = un' env False bnames x y
482 un' env fn bnames x (Bind n (Lam _ t) (App _ y (V 0)))
483 = un' env False bnames x y
484 un' env fn bnames (Bind n (Lam _ t) (App _ x (V 0))) y
485 = un' env False bnames x y
486-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
487-- = un' env False ((x,y):bnames) sx sy
488-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
489-- = un' env False ((x,y):bnames) sx sy
491 -- f D unifies with t -> D. This is dubious, but it helps with
492 -- interface resolution for interfaces over functions.
494 un' env fn bnames (App _ f x) (Bind n (Pi r i t k) y)
495 | noOccurrence n y && injectiveApp f
496 = do ux <- un' env False bnames x y
497 uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))
498 (Bind n (Pi r i t k) (V 1)))
499 combine env bnames ux uf
501 un' env fn bnames (Bind n (Pi r i t k) y) (App _ f x)
502 | noOccurrence n y && injectiveApp f
503 = do ux <- un' env False bnames y x
504 uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))
505 (Bind n (Pi r i t k) (V 1))) f
506 combine env bnames ux uf
508 un' env fn bnames (Bind x bx sx) (Bind y by sy)
509 | sameBinder bx by
510 = do h1 <- uB env bnames bx by
511 h2 <- un' ((x, RigW, bx) : env) False (((x,y),binderTy bx):bnames) sx sy
512 combine env bnames h1 h2
513 where sameBinder (Lam _ _) (Lam _ _) = True
514 sameBinder (Pi _ i _ _) (Pi _ i' _ _) = True
515 sameBinder _ _ = False -- never unify holes/guesses/etc
516 un' env fn bnames x y
517 | OK True <- convEq' ctxt holes x y = do sc 1; return []
518 | isUniverse x && isUniverse y = do sc 1; return []
519 | otherwise = do UI s f <- get
520 let r = recoverable (normalise ctxt env x)
521 (normalise ctxt env y)
522 let err = cantUnify from r
523 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
524 if (not r) then lift $ tfail err
525 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
526 return [] -- lift $ tfail err
528 unApp env fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
529 -- shortcut for the common case where we just want to check the
530 -- arguments are correct
531 | (injectiveApp fx && fx == fy)
532 = un' env False bnames ax ay
533 | (injectiveApp fx && injectiveApp fy)
534 || (injectiveApp fx && metavarApp fy && ax == ay)
535 || (injectiveApp fy && metavarApp fx && ax == ay)
536 = do let (headx, _) = unApply fx
537 let (heady, _) = unApply fy
538 -- fail quickly if the heads are disjoint
539 checkHeads headx heady
540 uplus
541 (do hf <- un' env True bnames fx fy
542 let ax' = hnormalise hf ctxt env (substNames hf ax)
543 let ay' = hnormalise hf ctxt env (substNames hf ay)
544 -- Don't normalise if we don't have to
545 ha <- uplus (un' env False bnames (substNames hf ax)
546 (substNames hf ay))
547 (un' env False bnames ax' ay')
548 sc 1
549 combine env bnames hf ha)
550 (do ha <- un' env False bnames ax ay
551 let fx' = hnormalise ha ctxt env (substNames ha fx)
552 let fy' = hnormalise ha ctxt env (substNames ha fy)
553 -- Don't normalise if we don't have to
554 hf <- uplus (un' env False bnames (substNames ha fx)
555 (substNames ha fy))
556 (un' env False bnames fx' fy')
557 sc 1
558 combine env bnames hf ha)
559 | otherwise = unifyTmpFail appx appy
560 where hnormalise [] _ _ t = t
561 hnormalise ns ctxt env t = normalise ctxt env t
562 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
563 | x /= y = unifyFail appx appy
564 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
565 | x /= y = unifyFail appx appy
566 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
567 = unifyFail appx appy
568 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
569 = unifyFail appx appy
570 checkHeads _ _ = return []
572 numArgs tm = let (f, args) = unApply tm in length args
574 metavarApp tm = let (f, args) = unApply tm in
575 (metavar f &&
576 all (\x -> metavarApp x) args
577 && nub args == args) ||
578 globmetavar tm
579 metavarArgs tm = let (f, args) = unApply tm in
580 all (\x -> metavar x || inenv x) args
581 && nub args == args
582 metavarApp' tm = let (f, args) = unApply tm in
583 all (\x -> pat x || metavar x) (f : args)
584 && nub args == args
586 rigid (P (DCon _ _ _) _ _) = True
587 rigid (P (TCon _ _) _ _) = True
588 rigid t@(P Ref _ _) = inenv t || globmetavar t
589 rigid (Constant _) = True
590 rigid (App _ f a) = rigid f && rigid a
591 rigid t = not (metavar t) || globmetavar t
593 globmetavar t = case unApply t of
594 (P _ x _, _) ->
595 case lookupDef x ctxt of
596 [TyDecl _ _] -> True
597 _ -> False
598 _ -> False
600 metavar t = case t of
601 P _ x _ -> (x `notElem` usersupp &&
602 (x `elem` holes || holeIn env x))
603 || globmetavar t
604 _ -> False
605 pat t = case t of
606 P _ x _ -> x `elem` holes || patIn env x
607 _ -> False
608 inenv t = case t of
609 P _ x _ -> x `elem` (map fstEnv env)
610 _ -> False
612 notFn t = injective t || metavar t || inenv t
615 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
616 unifyTmpFail x y
617 = do UI s f <- get
618 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
619 let err = cantUnify from r
620 (topx, xfrom) (topy, yfrom)
621 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
622 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
623 return []
625 -- shortcut failure, if we *know* nothing can fix it
626 unifyFail x y = do UI s f <- get
627 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
628 let err = cantUnify from r
629 (topx, xfrom) (topy, yfrom)
630 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
631 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
632 lift $ tfail err
635 uB env bnames (Let tx vx) (Let ty vy)
636 = do h1 <- un' env False bnames tx ty
637 h2 <- un' env False bnames vx vy
638 sc 1
639 combine env bnames h1 h2
640 uB env bnames (Guess tx vx) (Guess ty vy)
641 = do h1 <- un' env False bnames tx ty
642 h2 <- un' env False bnames vx vy
643 sc 1
644 combine env bnames h1 h2
645 uB env bnames (Lam _ tx) (Lam _ ty) = do sc 1; un' env False bnames tx ty
646 uB env bnames (Pi _ _ tx _) (Pi _ _ ty _) = do sc 1; un' env False bnames tx ty
647 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
648 uB env bnames (PVar _ tx) (PVar _ ty) = un' env False bnames tx ty
649 uB env bnames x y
650 = do UI s f <- get
651 let r = recoverable (normalise ctxt env (binderTy x))
652 (normalise ctxt env (binderTy y))
653 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
654 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
655 (errEnv env) s
656 put (UI s ((binderTy x, binderTy y,
657 False,
658 env, err, from, Unify) : f))
659 return [] -- lift $ tfail err
661 checkCycle ns p@(x, P _ _ _) = return [p]
662 checkCycle ns (x, tm)
663 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
664 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
666 checkScope ns (x, tm) | pureTerm tm =
667-- case boundVs (envPos x 0 env) tm of
668-- [] -> return [(x, tm)]
669-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
670-- (impl ns tm) (errEnv env))
671 let v = highV (-1) tm in
672 if v >= length ns
673 then lift $ tfail (Msg "SCOPE ERROR")
674 else return [(x, bind v ns tm)]
675 where impl [] tm = tm
676 impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
677 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
679 bind i ns tm
680 | i < 0 = tm
681 | otherwise = let ((x,y),ty) = ns!!i in
682 App MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))
683 (P Bound x ty)
685 combine env bnames as [] = return as
686 combine env bnames as ((n, t) : bs)
687 = case lookup n as of
688 Nothing -> combine env bnames (as ++ [(n,t)]) bs
689 Just t' -> do ns <- un' env False bnames t t'
690 -- make sure there's n mapping from n in ns
691 let ns' = filter (\ (x, _) -> x/=n) ns
692 sc 1
693 combine env bnames as (ns' ++ bs)
695boundVs :: Int -> Term -> [Int]
696boundVs i (V j) | j < i = []
697 | otherwise = [j]
698boundVs i (Bind n b sc) = boundVs (i + 1) sc
699boundVs i (App _ f x) = let fs = boundVs i f
700 xs = boundVs i x in
701 nub (fs ++ xs)
702boundVs i _ = []
704highV :: Int -> Term -> Int
705highV i (V j) | j > i = j
706 | otherwise = i
707highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
708highV i (App _ f x) = max (highV i f) (highV i x)
709highV i _ = i
711envPos x i [] = 0
712envPos x i ((y, _) : ys) | x == y = i
713 | otherwise = envPos x (i + 1) ys
716-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
717-- more work may help.
718-- FIXME: Depending on how overloading gets used, this may cause problems. Better
719-- rethink overloading properly...
720-- ASSUMPTION: inputs are in normal form
721--
722-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
723--
724recoverable t@(App _ _ _) _
725 | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
726recoverable _ t@(App _ _ _)
727 | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
728recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
729recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
730recoverable (TType _) (P (DCon _ _ _) y _) = False
731recoverable (UType _) (P (DCon _ _ _) y _) = False
732recoverable (Constant _) (P (DCon _ _ _) y _) = False
733recoverable (Constant x) (Constant y) = x == y
734recoverable (P (DCon _ _ _) x _) (TType _) = False
735recoverable (P (DCon _ _ _) x _) (UType _) = False
736recoverable (P (DCon _ _ _) x _) (Constant _) = False
737recoverable (TType _) (P (TCon _ _) y _) = False
738recoverable (UType _) (P (TCon _ _) y _) = False
739recoverable (Constant _) (P (TCon _ _) y _) = False
740recoverable (P (TCon _ _) x _) (TType _) = False
741recoverable (P (TCon _ _) x _) (UType _) = False
742recoverable (P (TCon _ _) x _) (Constant _) = False
743recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
744recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
745recoverable p@(TType _) (App _ f a) = recoverable p f
746recoverable p@(UType _) (App _ f a) = recoverable p f
747recoverable p@(Constant _) (App _ f a) = recoverable p f
748recoverable (App _ f a) p@(TType _) = recoverable f p
749recoverable (App _ f a) p@(UType _) = recoverable f p
750recoverable (App _ f a) p@(Constant _) = recoverable f p
751recoverable p@(P _ n _) (App _ f a) = recoverable p f
752recoverable (App _ f a) p@(P _ _ _) = recoverable f p
753recoverable (App _ f a) (App _ f' a')
754 | f == f' = recoverable a a'
755recoverable (App _ f a) (App _ f' a')
756 = recoverable f f' -- && recoverable a a'
757recoverable f (Bind _ (Pi _ _ _ _) sc)
758 | (P (DCon _ _ _) _ _, _) <- unApply f = False
759 | (P (TCon _ _) _ _, _) <- unApply f = False
760 | (Constant _) <- f = False
761 | TType _ <- f = False
762 | UType _ <- f = False
763recoverable (Bind _ (Pi _ _ _ _) sc) f
764 | (P (DCon _ _ _) _ _, _) <- unApply f = False
765 | (P (TCon _ _) _ _, _) <- unApply f = False
766 | (Constant _) <- f = False
767 | TType _ <- f = False
768 | UType _ <- f = False
769recoverable (Bind _ (Lam _ _) sc) f = recoverable sc f
770recoverable f (Bind _ (Lam _ _) sc) = recoverable f sc
771recoverable x y = True
773errEnv :: [(a, r, Binder b)] -> [(a, b)]
774errEnv = map (\(x, _, b) -> (x, binderTy b))
776holeIn :: Env -> Name -> Bool
777holeIn env n = case lookupBinder n env of
778 Just (Hole _) -> True
779 Just (Guess _ _) -> True
780 _ -> False
782patIn :: Env -> Name -> Bool
783patIn env n = case lookupBinder n env of
784 Just (PVar _ _) -> True
785 Just (PVTy _) -> True
786 _ -> False