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