@@ -206,7 +206,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
206206 when (not fromProver) -- in interactive mode,
207207 -- don't just guess (fine for 'auto',
208208 -- since that's part of the point...)
209− $ checkDisjoint ist [] others
209+ $ checkConstructor ist others
210210 tryCons d locs tys (others ++ getFn d fn)
211211 Nothing -> fail "Not a data type"
212212 _ -> fail "Not a data type"
@@ -249,28 +249,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
249249 ps' <- get_probs
250250 hs' <- get_holes
251251 when (length ps < length ps') $ fail "Can't apply constructor"
252+ let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)
252253 mapM_ (\ (_, h) -> do focus h
253254 aty <- goal
254− psRec True d locs tys)
255− (filter (\ (x, y) -> not x) (zip (map fst imps) args))
255+ psRec True d locs tys) newhs
256256 solve
257257
258258 isImp (PImp p _ _ _ _) = (True, p)
259259 isImp arg = (False, priority arg)
260260
261−-- Fails if any of the given constructor/function names have the same
262−-- return type (ignoring local variables - we need to be able to distinguish
263−-- by constructor)
264−checkDisjoint :: IState -> [Type] -> [Name] -> ElabD ()
265−checkDisjoint ist ts [] = return ()
266−checkDisjoint ist ts (n : ns) =
261+-- In interactive mode, only search for things if there is some constructor
262+-- index to help pick a relevant constructor
263+checkConstructor :: IState -> [Name] -> ElabD ()
264+checkConstructor ist [] = return ()
265+checkConstructor ist (n : ns) =
267266 case lookupTyExact n (tt_ctxt ist) of
268− Just t -> if any (matchTypes (getRetTy t)) ts
267+ Just t -> if not (conIndexed t)
269268 then fail "Overlapping constructor types"
270− else checkDisjoint ist (getRetTy t : ts) ns
269+ else checkConstructor ist ns
271270 where
272− matchTypes (V _) (V _) = True
273− matchTypes (App _ f a) (App _ f' a') = matchTypes f f' && matchTypes a a'
274− matchTypes (Bind _ t sc) (Bind _ t' sc')
275− = matchTypes (binderTy t) (binderTy t') && matchTypes sc sc'
276− matchTypes x y = x == y
271+ conIndexed t = let (_, args) = unApply (getRetTy t) in
272+ any conHead args
273+ conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)
274+ | otherwise = False