@@ -349,10 +349,29 @@ recoverableCoverage :: Context -> Err -> Bool
349349recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
350350 = let topx' = normalise ctxt [] topx
351351 topy' = normalise ctxt [] topy in
352− checkRec topx' topy'
352+ evalState (checkRec topx' topy') []
353353 where -- different notion of recoverable than in unification, since we
354354 -- have no metavars -- just looking to see if a constructor is failing
355− -- to unify with a function that may be reduced later
355+ -- to unify with a function that may be reduced later, or if any
356+ -- variables need to have two different constructor forms
357+
358+ -- The state is a mapping of name to what it has failed to unify
359+ -- with
360+ checkRec :: Term -> Term -> State [(Name, Term)] Bool
361+ checkRec (P Bound x _) tm
362+ | (P yt _ _, _) <- unApply tm,
363+ conType yt = do nmap <- get
364+ case lookup x nmap of
365+ Nothing -> do put ((x, tm) : nmap)
366+ return True
367+ Just y' -> checkRec tm y'
368+ checkRec tm (P Bound y _)
369+ | (P xt _ _, _) <- unApply tm,
370+ conType xt = do nmap <- get
371+ case lookup y nmap of
372+ Nothing -> do put ((y, tm) : nmap)
373+ return True
374+ Just x' -> checkRec tm x'
356375 checkRec (App _ f a) p@(P _ _ _) = checkRec f p
357376 checkRec p@(P _ _ _) (App _ f a) = checkRec p f
358377 checkRec fa@(App _ _ _) fa'@(App _ _ _)
@@ -360,13 +379,29 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
360379 (f', as') <- unApply fa'
361380 = if (length as /= length as')
362381 then checkRec f f'
363− else checkRec f f' && and (zipWith checkRec as as')
364− checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
365− checkRec _ _ = False
366−
382+ else checkRecs (f : as) (f' : as')
383+ where
384+ checkRecs [] [] = return True
385+ checkRecs (a : as) (b : bs) = do aok <- checkRec a b
386+ asok <- checkRecs as bs
387+ return (aok && asok)
388+ checkRec (P xt x _) (P yt y _)
389+ | x == y = return True
390+ | ntRec xt yt = return True
391+ checkRec _ _ = return False
392+
393+ conType (DCon _ _ _) = True
394+ conType (TCon _ _) = True
395+ conType _ = False
396+
397+ -- If either name is a reference or a bound variable, then further
398+ -- development may fix the error, so consider it recoverable.
399+ -- If both names are constructors, and the name is different, then
400+ -- it's not recoverable
367401 ntRec x y | Ref <- x = True
368402 | Ref <- y = True
369− | (Bound, Bound) <- (x, y) = True
403+ | Bound <- x = True
404+ | Bound <- y = True
370405 | otherwise = False -- name is different, unrecoverable
371406recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
372407recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e