git.iko.soy/Idris-dev
on db306ca help sign in
Idris-dev/src/Idris/Core/Unify.hs
608 lines 26 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Core.Unify(match_unify, unify, Fails, FailAt(..)) where
5import Idris.Core.TT
6import Idris.Core.Evaluate
8import Control.Monad
9import Control.Monad.State.Strict
10import Data.List
11import Debug.Trace
13-- Unification is applied inside the theorem prover. We're looking for holes
14-- which can be filled in, by matching one term's normal form against another.
15-- Returns a list of hole names paired with the term which solves them, and
16-- a list of things which need to be injective.
18-- terms which need to be injective, with the things we're trying to unify
19-- at the time
21data FailAt = Match | Unify
22 deriving (Show, Eq)
24type Injs = [(TT Name, TT Name, TT Name)]
25type Fails = [(TT Name, TT Name, Env, Err, FailAt)]
27data UInfo = UI Int Fails
28 deriving Show
30data UResult a = UOK a
31 | UPartOK a
32 | UFail Err
34-- Solve metavariables by matching terms against each other
35-- Not really unification, of course!
37match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
38 TC [(Name, TT Name)]
39match_unify ctxt env topx topy inj holes =
40 case runStateT (un [] (renameBindersTm env topx)
41 (renameBindersTm env topy)) (UI 0 []) of
42 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
43 res ->
44 let topxn = renameBindersTm env (normalise ctxt env topx)
45 topyn = renameBindersTm env (normalise ctxt env topy) in
46 case runStateT (un [] topxn topyn)
47 (UI 0 []) of
48 OK (v, UI _ fails) ->
49 return (map (renameBinders env) (trimSolutions v))
50 Error e ->
51 -- just normalise the term we're matching against
52 case runStateT (un [] topxn topy)
53 (UI 0 []) of
54 OK (v, UI _ fails) ->
55 return (map (renameBinders env) (trimSolutions v))
56 _ -> tfail e
57 where
60 un names (P _ x _) tm
61 | holeIn env x || x `elem` holes
62 = do sc 1; checkCycle names (x, tm)
63 un names tm (P _ y _)
64 | holeIn env y || y `elem` holes
65 = do sc 1; checkCycle names (y, tm)
66 un bnames (V i) (P _ x _)
67 | length bnames > i,
68 fst (fst (bnames!!i)) == x ||
69 snd (fst (bnames!!i)) == x = do sc 1; return []
70 un bnames (P _ x _) (V i)
71 | length bnames > i,
72 fst (fst (bnames!!i)) == x ||
73 snd (fst (bnames!!i)) == x = do sc 1; return []
74 un bnames (Bind x bx sx) (Bind y by sy)
75 = do h1 <- uB bnames bx by
76 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
77 combine bnames h1 h2
78 un names (App fx ax) (App fy ay)
79 = do hf <- un names fx fy
80 ha <- un names ax ay
81 combine names hf ha
82 un names x y
83 | OK True <- convEq' ctxt holes x y = do sc 1; return []
84 | otherwise = do UI s f <- get
85 let r = recoverable x y
86 let err = CantUnify r
87 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
88 if (not r) then lift $ tfail err
89 else do put (UI s ((x, y, env, err, Match) : f))
90 lift $ tfail err
93 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
94 h2 <- un bnames vx vy
95 combine bnames h1 h2
96 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
97 uB bnames (Pi tx) (Pi ty) = un bnames tx ty
98 uB bnames x y = do UI s f <- get
99 let r = recoverable (binderTy x) (binderTy y)
100 let err = CantUnify r topx topy
101 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
102 (errEnv env) s
103 put (UI s ((binderTy x, binderTy y, env, err, Match) : f))
104 return []
106 -- TODO: there's an annoying amount of repetition between this and the
107 -- main unification function. Consider lifting it out.
109 sc i = do UI s f <- get
110 put (UI (s+i) f)
112 unifyFail x y = do UI s f <- get
113 let r = recoverable x y
114 let err = CantUnify r
115 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
116 put (UI s ((x, y, env, err, Match) : f))
117 lift $ tfail err
118 combine bnames as [] = return as
119 combine bnames as ((n, t) : bs)
120 = case lookup n as of
121 Nothing -> combine bnames (as ++ [(n,t)]) bs
122 Just t' -> do ns <- un bnames t t'
123 -- make sure there's n mapping from n in ns
124 let ns' = filter (\ (x, _) -> x/=n) ns
125 sc 1
126 combine bnames as (ns' ++ bs)
128 checkCycle ns p@(x, P _ _ _) = return [p]
129 checkCycle ns (x, tm)
130 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
131 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
133 checkScope ns (x, tm) =
134-- case boundVs (envPos x 0 env) tm of
135-- [] -> return [(x, tm)]
136-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
137-- (inst ns tm) (errEnv env))
138 let v = highV (-1) tm in
139 if v >= length ns
140 then lift $ tfail (Msg "SCOPE ERROR")
141 else return [(x, bind v ns tm)]
142 where inst [] tm = tm
143 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
145 bind i ns tm
146 | i < 0 = tm
147 | otherwise = let ((x,y),ty) = ns!!i in
148 App (Bind y (Lam ty) (bind (i-1) ns tm))
149 (P Bound x ty)
151renameBinders env (x, t) = (x, renameBindersTm env t)
153renameBindersTm :: Env -> TT Name -> TT Name
154renameBindersTm env tm = uniqueBinders (map fst env) tm
155 where
156 uniqueBinders env (Bind n b sc)
157 | n `elem` env
158 = let n' = uniqueName n env in
159 Bind n' (fmap (uniqueBinders env) b)
160 (uniqueBinders (n':env) (rename n n' sc))
161 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
162 (uniqueBinders (n:env) sc)
163 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)
164 uniqueBinders env t = t
166 rename n n' (P nt x ty) | n == x = P nt n' ty
167 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
168 rename n n' (App f a) = App (rename n n' f) (rename n n' a)
169 rename n n' t = t
171trimSolutions ns = dropPairs ns
172 where dropPairs [] = []
173 dropPairs (n@(x, P _ x' _) : ns)
174 | x == x' = dropPairs ns
175 | otherwise
176 = n : dropPairs
177 (filter (\t -> case t of
178 (n, P _ n' _) -> not (n == x' && n' == x)
179 _ -> True) ns)
180 dropPairs (n : ns) = n : dropPairs ns
182expandLets env (x, tm) = (x, doSubst (reverse env) tm)
183 where
184 doSubst [] tm = tm
185 doSubst ((n, Let v t) : env) tm
186 = doSubst env (subst n v tm)
187 doSubst (_ : env) tm
188 = doSubst env tm
191unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
192 TC ([(Name, TT Name)], Fails)
193unify ctxt env topx topy inj holes =
194-- trace ("Unifying " ++ show (topx, topy)) $
195 -- don't bother if topx and topy are different at the head
196 case runStateT (un False [] (renameBindersTm env topx)
197 (renameBindersTm env topy)) (UI 0 []) of
198 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
199 [])
200 res ->
201 let topxn = renameBindersTm env (normalise ctxt env topx)
202 topyn = renameBindersTm env (normalise ctxt env topy) in
203-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
204 case runStateT (un False [] topxn topyn)
205 (UI 0 []) of
206 OK (v, UI _ fails) ->
207 return (map (renameBinders env) (trimSolutions v),
208 reverse fails)
209-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
210 Error e -> tfail e
211 where
212 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
213 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
214 headDiff _ _ = False
216 injective (P (DCon _ _) _ _) = True
217 injective (P (TCon _ _) _ _) = True
218-- injective (App f (P _ _ _)) = injective f
219-- injective (App f (Constant _)) = injective f
220 injective (App f a) = injective f -- && injective a
221 injective _ = False
223-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
224 injectiveVar (P _ n _) = n `elem` inj
225 injectiveVar (App f a) = injectiveVar f -- && injective a
226 injectiveVar _ = False
228 injectiveApp x = injective x || injectiveVar x
230 notP (P _ _ _) = False
231 notP _ = True
233 sc i = do UI s f <- get
234 put (UI (s+i) f)
236 errors :: StateT UInfo TC Bool
237 errors = do UI s f <- get
238 return (not (null f))
240 uplus u1 u2 = do UI s f <- get
241 r <- u1
242 UI s f' <- get
243 if (length f == length f')
244 then return r
245 else do put (UI s f); u2
247 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
248 StateT UInfo
249 TC [(Name, TT Name)]
250 un = un'
251-- un fn names x y
252-- = let (xf, _) = unApply x
253-- (yf, _) = unApply y in
254-- if headDiff xf yf then unifyFail x y else
255-- uplus (un' fn names x y)
256-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
258 un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
259 StateT UInfo
260 TC [(Name, TT Name)]
261 un' fn names x y | x == y = return [] -- shortcut
262 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
263 | x /= y = unifyFail topx topy
264 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
265 | x /= y = unifyFail topx topy
266 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
267 = unifyFail topx topy
268 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
269 = unifyFail topx topy
270 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
271 = unifyFail topx topy
272 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
273 = unifyFail topx topy
274 un' fn bnames tx@(P _ x _) ty@(P _ y _)
275 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
276 | injective tx && not (holeIn env y || y `elem` holes)
277 = unifyTmpFail tx ty
278 | injective ty && not (holeIn env x || x `elem` holes)
279 = unifyTmpFail tx ty
280 un' fn bnames xtm@(P _ x _) tm
281 | holeIn env x || x `elem` holes
282 = do UI s f <- get
283 -- injectivity check
284 x <- checkCycle bnames (x, tm)
285 if (notP tm && fn)
286-- trace (show (x, tm, normalise ctxt env tm)) $
287-- put (UI s ((tm, topx, topy) : i) f)
288 then unifyTmpFail xtm tm
289 else do sc 1
290 return x
291 | not (injective xtm) && injective tm
292 = do checkCycle bnames (x, tm)
293 unifyTmpFail xtm tm
294 un' fn bnames tm ytm@(P _ y _)
295 | holeIn env y || y `elem` holes
296 = do UI s f <- get
297 -- injectivity check
298 x <- checkCycle bnames (y, tm)
299 if (notP tm && fn)
300-- trace (show (y, tm, normalise ctxt env tm)) $
301-- put (UI s ((tm, topx, topy) : i) f)
302 then unifyTmpFail tm ytm
303 else do sc 1
304 return x
305 | not (injective ytm) && injective tm
306 = do checkCycle bnames (y, tm)
307 unifyTmpFail tm ytm
308 un' fn bnames (V i) (P _ x _)
309 | length bnames > i,
310 fst ((map fst bnames)!!i) == x ||
311 snd ((map fst bnames)!!i) == x = do sc 1; return []
312 un' fn bnames (P _ x _) (V i)
313 | length bnames > i,
314 fst ((map fst bnames)!!i) == x ||
315 snd ((map fst bnames)!!i) == x = do sc 1; return []
317 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
318 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
320 un' fn bnames appx@(App _ _) appy@(App _ _)
321 = unApp fn bnames appx appy
322-- = uplus (unApp fn bnames appx appy)
323-- (unifyTmpFail appx appy) -- take the whole lot
325 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
326 | n == n' = un' False bnames x y
327 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
328 | n == n' = un' False bnames x y
329 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
330 = un' False bnames x y
331 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
332 = un' False bnames x y
333-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
334-- = un' False ((x,y):bnames) sx sy
335-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
336-- = un' False ((x,y):bnames) sx sy
338 -- f D unifies with t -> D. This is dubious, but it helps with type
339 -- class resolution for type classes over functions.
341 un' fn bnames (App f x) (Bind n (Pi t) y)
342 | noOccurrence n y && injectiveApp f
343 = do ux <- un' False bnames x y
344 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
345 (Bind n (Pi t) (V 1)))
346 combine bnames ux uf
348 un' fn bnames (Bind n (Pi t) y) (App f x)
349 | noOccurrence n y && injectiveApp f
350 = do ux <- un' False bnames y x
351 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
352 (Bind n (Pi t) (V 1))) f
353 combine bnames ux uf
355 un' fn bnames (Bind x bx sx) (Bind y by sy)
356 | sameBinder bx by
357 = do h1 <- uB bnames bx by
358 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
359 combine bnames h1 h2
360 where sameBinder (Lam _) (Lam _) = True
361 sameBinder (Pi _) (Pi _) = True
362 sameBinder _ _ = False
363 un' fn bnames x y
364 | OK True <- convEq' ctxt holes x y = do sc 1; return []
365 | otherwise = do UI s f <- get
366 let r = recoverable x y
367 let err = CantUnify r
368 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
369 if (not r) then lift $ tfail err
370 else do put (UI s ((x, y, env, err, Unify) : f))
371 return [] -- lift $ tfail err
373 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
374 | (injectiveApp fx && injectiveApp fy)
375 || (injectiveApp fx && rigid appx && metavarApp appy)
376 || (injectiveApp fy && rigid appy && metavarApp appx)
377 || (injectiveApp fx && metavarApp fy && ax == ay)
378 || (injectiveApp fy && metavarApp fx && ax == ay)
379 = do let (headx, _) = unApply fx
380 let (heady, _) = unApply fy
381 -- fail quickly if the heads are disjoint
382 checkHeads headx heady
383-- if True then -- (injective fx || injective fy || fx == fy) then
384-- if (injective fx && metavarApp appy) ||
385-- (injective fy && metavarApp appx) ||
386-- (injective fx && injective fy) || fx == fy
387 uplus
388 (do hf <- un' True bnames fx fy
389 let ax' = hnormalise hf ctxt env (substNames hf ax)
390 let ay' = hnormalise hf ctxt env (substNames hf ay)
391 ha <- un' False bnames ax' ay'
392 sc 1
393 combine bnames hf ha)
394 (do ha <- un' False bnames ax ay
395 let fx' = hnormalise ha ctxt env (substNames ha fx)
396 let fy' = hnormalise ha ctxt env (substNames ha fy)
397 hf <- un' False bnames fx' fy'
398 sc 1
399 combine bnames hf ha)
400 | otherwise = unifyTmpFail appx appy
401 where hnormalise [] _ _ t = t
402 hnormalise ns ctxt env t = normalise ctxt env t
403 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
404 | x /= y = unifyFail appx appy
405 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
406 | x /= y = unifyFail appx appy
407 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
408 = unifyFail appx appy
409 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
410 = unifyFail appx appy
411 checkHeads _ _ = return []
413 unArgs as [] [] = return as
414 unArgs as (x : xs) (y : ys)
415 = do let x' = hnormalise as ctxt env (substNames as x)
416 let y' = hnormalise as ctxt env (substNames as y)
417 as' <- un' False bnames x' y'
418 vs <- combine bnames as as'
419 unArgs vs xs ys
421 metavarApp tm = let (f, args) = unApply tm in
422 (metavar f &&
423 all (\x -> metavarApp x) args
424 && nub args == args) ||
425 globmetavar tm
426 metavarArgs tm = let (f, args) = unApply tm in
427 all (\x -> metavar x || inenv x) args
428 && nub args == args
429 metavarApp' tm = let (f, args) = unApply tm in
430 all (\x -> pat x || metavar x) (f : args)
431 && nub args == args
433 rigid (P (DCon _ _) _ _) = True
434 rigid (P (TCon _ _) _ _) = True
435 rigid t@(P Ref _ _) = inenv t || globmetavar t
436 rigid (Constant _) = True
437 rigid (App f a) = rigid f && rigid a
438 rigid t = not (metavar t) || globmetavar t
440 globmetavar t = case unApply t of
441 (P _ x _, _) ->
442 case lookupDef x ctxt of
443 [TyDecl _ _] -> True
444 _ -> False
445 _ -> False
447 metavar t = case t of
448 P _ x _ -> (x `elem` holes || holeIn env x)
449 || globmetavar t
450 _ -> False
451 pat t = case t of
452 P _ x _ -> x `elem` holes || patIn env x
453 _ -> False
454 inenv t = case t of
455 P _ x _ -> x `elem` (map fst env)
456 _ -> False
458 notFn t = injective t || metavar t || inenv t
461 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
462 unifyTmpFail x y
463 = do UI s f <- get
464 let r = recoverable x y
465 let err = CantUnify r
466 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
467 put (UI s ((topx, topy, env, err, Unify) : f))
468 return []
470 -- shortcut failure, if we *know* nothing can fix it
471 unifyFail x y = do UI s f <- get
472 let r = recoverable x y
473 let err = CantUnify r
474 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
475 put (UI s ((topx, topy, env, err, Unify) : f))
476 lift $ tfail err
479 uB bnames (Let tx vx) (Let ty vy)
480 = do h1 <- un' False bnames tx ty
481 h2 <- un' False bnames vx vy
482 sc 1
483 combine bnames h1 h2
484 uB bnames (Guess tx vx) (Guess ty vy)
485 = do h1 <- un' False bnames tx ty
486 h2 <- un' False bnames vx vy
487 sc 1
488 combine bnames h1 h2
489 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
490 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
491 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
492 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
493 uB bnames x y = do UI s f <- get
494 let r = recoverable (binderTy x) (binderTy y)
495 let err = CantUnify r topx topy
496 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
497 (errEnv env) s
498 put (UI s ((binderTy x, binderTy y, env, err, Unify) : f))
499 return [] -- lift $ tfail err
501 checkCycle ns p@(x, P _ _ _) = return [p]
502 checkCycle ns (x, tm)
503 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
504 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
506 checkScope ns (x, tm) =
507-- case boundVs (envPos x 0 env) tm of
508-- [] -> return [(x, tm)]
509-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
510-- (inst ns tm) (errEnv env))
511 let v = highV (-1) tm in
512 if v >= length ns
513 then lift $ tfail (Msg "SCOPE ERROR")
514 else return [(x, bind v ns tm)]
515 where inst [] tm = tm
516 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
518 bind i ns tm
519 | i < 0 = tm
520 | otherwise = let ((x,y),ty) = ns!!i in
521 App (Bind y (Lam ty) (bind (i-1) ns tm))
522 (P Bound x ty)
524 combineArgs bnames args = ca [] args where
525 ca acc [] = return acc
526 ca acc (x : xs) = do x' <- combine bnames acc x
527 ca x' xs
529 combine bnames as [] = return as
530 combine bnames as ((n, t) : bs)
531 = case lookup n as of
532 Nothing -> combine bnames (as ++ [(n,t)]) bs
533 Just t' -> do ns <- un' False bnames t t'
534 -- make sure there's n mapping from n in ns
535 let ns' = filter (\ (x, _) -> x/=n) ns
536 sc 1
537 combine bnames as (ns' ++ bs)
539boundVs :: Int -> Term -> [Int]
540boundVs i (V j) | j < i = []
541 | otherwise = [j]
542boundVs i (Bind n b sc) = boundVs (i + 1) sc
543boundVs i (App f x) = let fs = boundVs i f
544 xs = boundVs i x in
545 nub (fs ++ xs)
546boundVs i _ = []
548highV :: Int -> Term -> Int
549highV i (V j) | j > i = j
550 | otherwise = i
551highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
552highV i (App f x) = max (highV i f) (highV i x)
553highV i _ = i
555envPos x i [] = 0
556envPos x i ((y, _) : ys) | x == y = i
557 | otherwise = envPos x (i + 1) ys
560-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
561-- more work may help.
562-- FIXME: Depending on how overloading gets used, this may cause problems. Better
563-- rethink overloading properly...
565recoverable t@(App _ _) _
566 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False
567recoverable _ t@(App _ _)
568 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False
569recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
570 | x == y = True
571 | otherwise = False
572recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
573 | x == y = True
574 | otherwise = False
575recoverable (Constant _) (P (DCon _ _) y _) = False
576recoverable (P (DCon _ _) x _) (Constant _) = False
577recoverable (Constant _) (P (TCon _ _) y _) = False
578recoverable (P (TCon _ _) x _) (Constant _) = False
579recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
580recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
581recoverable p@(Constant _) (App f a) = recoverable p f
582recoverable (App f a) p@(Constant _) = recoverable f p
583recoverable p@(P _ n _) (App f a) = recoverable p f
584-- recoverable (App f a) p@(P _ _ _) = recoverable f p
585recoverable (App f a) (App f' a')
586 = recoverable f f' -- && recoverable a a'
587recoverable f (Bind _ (Pi _) sc)
588 | (P (DCon _ _) _ _, _) <- unApply f = False
589 | (P (TCon _ _) _ _, _) <- unApply f = False
590recoverable (Bind _ (Pi _) sc) f
591 | (P (DCon _ _) _ _, _) <- unApply f = False
592 | (P (TCon _ _) _ _, _) <- unApply f = False
593recoverable _ _ = True
595errEnv = map (\(x, b) -> (x, binderTy b))
597holeIn :: Env -> Name -> Bool
598holeIn env n = case lookup n env of
599 Just (Hole _) -> True
600 Just (Guess _ _) -> True
601 _ -> False
603patIn :: Env -> Name -> Bool
604patIn env n = case lookup n env of
605 Just (PVar _) -> True
606 Just (PVTy _) -> True
607 _ -> False