@@ -476,7 +476,7 @@ elab ist info emode opts fn tm
476476 ty <- goal
477477 let (tc, _) = unApply (unDelay ty)
478478 env <- get_env
479− return $ pruneByType env tc ist as
479+ return $ pruneByType env tc (unDelay ty) ist as
480480
481481 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
482482 l == txt "Lazy'" = unDelay arg
@@ -1566,9 +1566,10 @@ pruneAlt xs = map prune xs
15661566-- Rule out alternatives that don't return the same type as the head of the goal
15671567-- (If there are none left as a result, do nothing)
15681568pruneByType :: Env -> Term -> -- head of the goal
1569+ Type -> -- goal
15691570 IState -> [PTerm] -> [PTerm]
15701571-- 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
15721573 | Just a <- locallyBound as = [a]
15731574 where
15741575 locallyBound [] = Nothing
@@ -1584,7 +1585,7 @@ pruneByType env t c as
15841585 getName _ = Nothing
15851586
15861587-- '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
15881589-- if the goal type is polymorphic, keep everything
15891590 | Nothing <- lookupTyExact n ctxt = as
15901591-- if the goal type is a ?metavariable, keep everything
@@ -1598,6 +1599,8 @@ pruneByType env (P _ n _) ist as
15981599 where
15991600 ctxt = tt_ctxt ist
16001601
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.
16011604 headIs var f (PRef _ _ f') = typeHead var f f'
16021605 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
16031606 | l == txt "Delay" = headIs var f (getTm arg)
@@ -1611,19 +1614,39 @@ pruneByType env (P _ n _) ist as
16111614 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
16121615 case lookupTyExact f' ctxt of
16131616 Just ty -> case unApply (getRetTy ty) of
1614− (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f
1617+ (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
1618+ -> False
16151619 _ -> let ty' = normalise ctxt [] ty in
1620+-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $
16161621 case unApply (getRetTy ty') of
1617− (P _ ftyn _, _) -> ftyn == f
16181622 (V _, _) ->
1619− -- keep, variable
1620−-- trace ("Keeping " ++ show (f', ty')
1621−-- ++ " for " ++ show n) $
16221623 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
16241629 _ -> False
16251630
1626−pruneByType _ t _ as = as
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'
1634+ | otherwise = True
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
1648+
1649+pruneByType _ t _ _ as = as
16271650
16281651-- Could the name feasibly be the return type?
16291652-- If there is a type class constraint on the return type, and no instance