@@ -476,7 +476,7 @@ elab ist info emode opts fn tm
476 ty <- goal
476 ty <- goal
477 let (tc, _) = unApply (unDelay ty)
477 let (tc, _) = unApply (unDelay ty)
478 env <- get_env
478 env <- get_env
479− return $ pruneByType env tc ist as
479+ return $ pruneByType env tc (unDelay ty) ist as
481 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
481 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
482 l == txt "Lazy'" = unDelay arg
482 l == txt "Lazy'" = unDelay arg
@@ -1566,9 +1566,10 @@ pruneAlt xs = map prune xs
1566-- Rule out alternatives that don't return the same type as the head of the goal
1566-- Rule out alternatives that don't return the same type as the head of the goal
1567-- (If there are none left as a result, do nothing)
1567-- (If there are none left as a result, do nothing)
1568pruneByType :: Env -> Term -> -- head of the goal
1568pruneByType :: Env -> Term -> -- head of the goal
1569 IState -> [PTerm] -> [PTerm]
1570 IState -> [PTerm] -> [PTerm]
1570-- if an alternative has a locally bound name at the head, take it
1571-- if an alternative has a locally bound name at the head, take it
1571−pruneByType env t c as
1572+pruneByType env t goalty c as
1572 | Just a <- locallyBound as = [a]
1573 | Just a <- locallyBound as = [a]
1574 locallyBound [] = Nothing
1575 locallyBound [] = Nothing
@@ -1584,7 +1585,7 @@ pruneByType env t c as
1584 getName _ = Nothing
1585 getName _ = Nothing
1586-- 'n' is the name at the head of the goal type
1587-- 'n' is the name at the head of the goal type
1587−pruneByType env (P _ n _) ist as
1588+pruneByType env (P _ n _) goalty ist as
1588-- if the goal type is polymorphic, keep everything
1589-- if the goal type is polymorphic, keep everything
1589 | Nothing <- lookupTyExact n ctxt = as
1590 | Nothing <- lookupTyExact n ctxt = as
1590-- if the goal type is a ?metavariable, keep everything
1591-- if the goal type is a ?metavariable, keep everything
@@ -1598,6 +1599,8 @@ pruneByType env (P _ n _) ist as
1599 ctxt = tt_ctxt ist
1600 ctxt = tt_ctxt ist
1602+ -- Get the function at the head of the alternative and see if it's
1603+ -- a plausible match against the goal type. Keep if so.
1601 headIs var f (PRef _ _ f') = typeHead var f f'
1604 headIs var f (PRef _ _ f') = typeHead var f f'
1602 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1605 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1603 | l == txt "Delay" = headIs var f (getTm arg)
1606 | l == txt "Delay" = headIs var f (getTm arg)
@@ -1611,19 +1614,39 @@ pruneByType env (P _ n _) ist as
1611 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
1614 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
1612 case lookupTyExact f' ctxt of
1615 case lookupTyExact f' ctxt of
1613 Just ty -> case unApply (getRetTy ty) of
1616 Just ty -> case unApply (getRetTy ty) of
1614− (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f
1617+ (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
1615 _ -> let ty' = normalise ctxt [] ty in
1619 _ -> let ty' = normalise ctxt [] ty in
1620+-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $
1616 case unApply (getRetTy ty') of
1621 case unApply (getRetTy ty') of
1617− (P _ ftyn _, _) -> ftyn == f
1618 (V _, _) ->
1622 (V _, _) ->
1620−-- trace ("Keeping " ++ show (f', ty')
1621−-- ++ " for " ++ show n) $
1622 isPlausible ist var env n ty
1623 isPlausible ist var env n ty
1623− _ -> False
1624+ _ -> matching (getRetTy ty') goalty
1625+-- May be useful to keep for debugging purposes for a bit:
1626+-- let res = matching (getRetTy ty') goalty in
1627+-- traceWhen (not res)
1628+-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
1624 _ -> False
1629 _ -> False
1631+ -- If the goal is a constructor, it must match the suggested function type
1632+ matching (P _ ctyn _) (P _ n' _)
1633+ | isTConName n' ctxt = ctyn == n'
1635+ -- Variables match anything
1636+ matching (V _) _ = True
1637+ matching _ (V _) = True
1638+ matching _ (P _ n _) = not (isTConName n ctxt)
1639+ matching (P _ n _) _ = not (isTConName n ctxt)
1640+ -- Binders are a plausible match, so keep them
1641+ matching (Bind n _ sc) _ = True
1642+ matching _ (Bind n _ sc) = True
1643+ -- Otherwise, match the rest of the structure
1644+ matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
1645+ matching (TType _) (TType _) = True
1646+ matching (UType _) (UType _) = True
1647+ matching l r = l == r
1626−pruneByType _ t _ as = as
1649+pruneByType _ t _ _ as = as
1628-- Could the name feasibly be the return type?
1651-- Could the name feasibly be the return type?
1629-- If there is a type class constraint on the return type, and no instance
1652-- If there is a type class constraint on the return type, and no instance