@@ -276,11 +276,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
276 case lookupCtxtExact n (idris_datatypes ist) of
276 case lookupCtxtExact n (idris_datatypes ist) of
277 Just t -> do
277 Just t -> do
278 let others = hints ++ con_names t ++ autohints
278 let others = hints ++ con_names t ++ autohints
279− when (not fromProver && length (con_names t) > 1)
280− -- in interactive mode,
281− -- don't just guess (fine for 'auto',
282− -- since that's part of the point...)
283− $ checkConstructor ist others
284 tryCons d locs tys (others ++ getFn d fn)
279 tryCons d locs tys (others ++ getFn d fn)
285 Nothing -> typeNotSearchable t
280 Nothing -> typeNotSearchable t
286 _ -> typeNotSearchable t
281 _ -> typeNotSearchable t
@@ -341,23 +336,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
341 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
336 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
344−-- In interactive mode, only search for things if there is some
345−-- index to help pick a relevant constructor
346−checkConstructor :: IState -> [Name] -> ElabD ()
347−checkConstructor ist [] = return ()
348−checkConstructor ist (n : ns) =
349− case lookupTyExact n (tt_ctxt ist) of
350− Just t -> if not (conIndexed t)
351− then fail "Overlapping constructor types"
352− else checkConstructor ist ns
354− conIndexed t = let (_, args) = unApply (getRetTy t) in
356− conHead t | (P _ n _, _) <- unApply t = case lookupDefExact n (tt_ctxt ist) of
361-- | Resolve type classes. This will only pick up 'normal' instances, never
339-- | Resolve type classes. This will only pick up 'normal' instances, never
362-- named instances (which is enforced by 'findInstances').
340-- named instances (which is enforced by 'findInstances').
363resolveTC :: Bool -- ^ using default Int
341resolveTC :: Bool -- ^ using default Int