@@ -201,11 +201,13 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
201 Nothing -> []
201 Nothing -> []
202 Just hs -> hs
202 Just hs -> hs
203 case lookupCtxtExact n (idris_datatypes ist) of
203 case lookupCtxtExact n (idris_datatypes ist) of
205+ let others = hints ++ con_names t ++ autohints
206+ when (not fromProver) -- in interactive mode,
207+ -- don't just guess (fine for 'auto',
208+ -- since that's part of the point...)
209+ $ checkDisjoint ist [] others
204− Just t -> tryCons d locs tys
210+ tryCons d locs tys (others ++ getFn d fn)
209 Nothing -> fail "Not a data type"
211 Nothing -> fail "Not a data type"
210 _ -> fail "Not a data type"
212 _ -> fail "Not a data type"
@@ -221,15 +223,9 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
221 | otherwise = try' (tryLocal d (x : locs) tys x t)
223 | otherwise = try' (tryLocal d (x : locs) tys x t)
222 (tryLocals d locs tys xs) True
224 (tryLocals d locs tys xs) True
224− tryCons d locs tys cs = do when (not fromProver) -- in interactive mode,
225− -- don't just guess (fine for 'auto',
226− -- since that's part of the point...)
227− $ checkDisjoint ist [] cs
228− tryCons' d locs tys cs
230− tryCons' d locs tys [] = fail "Constructors failed"
226+ tryCons d locs tys [] = fail "Constructors failed"
231− tryCons' d locs tys (c : cs)
227+ tryCons d locs tys (c : cs)
232− = try' (tryCon d locs tys c) (tryCons' d locs tys cs) True
228+ = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
234 tryLocal d locs tys n t
230 tryLocal d locs tys n t
235 = do let a = getPArity (delab ist (binderTy t))
231 = do let a = getPArity (delab ist (binderTy t))