@@ -1630,7 +1630,8 @@ pruneByType env (P _ n _) goalty ist as
1630 ctxt = tt_ctxt ist
1630 ctxt = tt_ctxt ist
1632 -- Get the function at the head of the alternative and see if it's
1632 -- 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.
1634 headIs var f (PRef _ _ f') = typeHead var f f'
1635 headIs var f (PRef _ _ f') = typeHead var f f'
1635 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1636 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1636 | l == txt "Delay" = headIs var f (getTm arg)
1637 | l == txt "Delay" = headIs var f (getTm arg)
@@ -1652,6 +1653,7 @@ pruneByType env (P _ n _) goalty ist as
1652 (V _, _) ->
1653 (V _, _) ->
1653 isPlausible ist var env n ty
1654 isPlausible ist var env n ty
1654 _ -> matching (getRetTy ty') goalty
1655 _ -> matching (getRetTy ty') goalty
1656+ || isCoercion (getRetTy ty') goalty
1655-- May be useful to keep for debugging purposes for a bit:
1657-- May be useful to keep for debugging purposes for a bit:
1656-- let res = matching (getRetTy ty') goalty in
1658-- let res = matching (getRetTy ty') goalty in
1657-- traceWhen (not res)
1659-- traceWhen (not res)
@@ -1679,6 +1681,30 @@ pruneByType env (P _ n _) goalty ist as
1679 matching (UType _) (UType _) = True
1681 matching (UType _) (UType _) = True
1680 matching l r = l == r
1682 matching l r = l == r
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
1690+ getCoercionsBetween :: Name -> Type -> [Name]
1691+ getCoercionsBetween r goal
1692+ = let cs = getCoercionsTo ist goal in
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
1700+ ps ++ findCoercions t ns
1703+ case unApply (getRetTy ty) of
1704+ (P _ t _, _) -> t == r
1682pruneByType _ t _ _ as = as
1708pruneByType _ t _ _ as = as
1684-- Could the name feasibly be the return type?
1710-- Could the name feasibly be the return type?