@@ -265,7 +265,8 @@ elab ist info pattern opts fn tm
265265 ty <- goal
266266 ctxt <- get_context
267267 let (tc, _) = unApply ty
268− let as' = pruneByType tc ctxt as
268+ env <- get_env
269+ let as' = pruneByType (map fst env) tc ctxt as
269270-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
270271 tryAll (zip (map (elab' ina) as') (map showHd as'))
271272 where showHd (PApp _ (PRef _ n) _) = show n
@@ -785,8 +786,21 @@ pruneAlt xs = map prune xs
785786
786787-- Rule out alternatives that don't return the same type as the head of the goal
787788-- (If there are none left as a result, do nothing)
788−pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
789−pruneByType (P _ n _) c as
789+pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]
790+-- if an alternative has a locally bound name at the head, take it
791+pruneByType env t c as
792+ | Just a <- locallyBound as = [a]
793+ where
794+ locallyBound [] = Nothing
795+ locallyBound (t:ts)
796+ | Just n <- getName t,
797+ n `elem` env = Just t
798+ | otherwise = locallyBound ts
799+ getName (PRef _ n) = Just n
800+ getName (PApp _ f _) = getName f
801+ getName _ = Nothing
802+
803+pruneByType env (P _ n _) c as
790804-- if the goal type is polymorphic, keep e
791805 | [] <- lookupTy n c = as
792806 | otherwise
@@ -812,7 +826,7 @@ pruneByType (P _ n _) c as
812826 _ -> False
813827 _ -> False
814828
815−pruneByType t _ as = as
829+pruneByType _ t _ as = as
816830
817831findInstances :: IState -> Term -> [Name]
818832findInstances ist t