@@ -1630,7 +1630,8 @@ pruneByType env (P _ n _) goalty ist as
16301630 ctxt = tt_ctxt ist
16311631
16321632 -- Get the function at the head of the alternative and see if it's
1633− -- a plausible match against the goal type. Keep if so.
1633+ -- a plausible match against the goal type. Keep if so. Also keep if
1634+ -- there is a possible coercion to the goal type.
16341635 headIs var f (PRef _ _ f') = typeHead var f f'
16351636 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
16361637 | l == txt "Delay" = headIs var f (getTm arg)
@@ -1652,6 +1653,7 @@ pruneByType env (P _ n _) goalty ist as
16521653 (V _, _) ->
16531654 isPlausible ist var env n ty
16541655 _ -> matching (getRetTy ty') goalty
1656+ || isCoercion (getRetTy ty') goalty
16551657-- May be useful to keep for debugging purposes for a bit:
16561658-- let res = matching (getRetTy ty') goalty in
16571659-- traceWhen (not res)
@@ -1679,6 +1681,30 @@ pruneByType env (P _ n _) goalty ist as
16791681 matching (UType _) (UType _) = True
16801682 matching l r = l == r
16811683
1684+ -- Return whether there is a possible coercion between the return type
1685+ -- of an alternative and the goal type
1686+ isCoercion rty gty | (P _ r _, _) <- unApply rty
1687+ = not (null (getCoercionsBetween r gty))
1688+ isCoercion _ _ = False
1689+
1690+ getCoercionsBetween :: Name -> Type -> [Name]
1691+ getCoercionsBetween r goal
1692+ = let cs = getCoercionsTo ist goal in
1693+ findCoercions r cs
1694+ where findCoercions t [] = []
1695+ findCoercions t (n : ns) =
1696+ let ps = case lookupTy n (tt_ctxt ist) of
1697+ [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in
1698+ [n | any useR as]
1699+ _ -> [] in
1700+ ps ++ findCoercions t ns
1701+
1702+ useR ty =
1703+ case unApply (getRetTy ty) of
1704+ (P _ t _, _) -> t == r
1705+ _ -> False
1706+
1707+
16821708pruneByType _ t _ _ as = as
16831709
16841710-- Could the name feasibly be the return type?