@@ -276,11 +276,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
276276 case lookupCtxtExact n (idris_datatypes ist) of
277277 Just t -> do
278278 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
284279 tryCons d locs tys (others ++ getFn d fn)
285280 Nothing -> typeNotSearchable t
286281 _ -> typeNotSearchable t
@@ -341,23 +336,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
341336 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
342337 _ -> []
343338
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
353− where
354− conIndexed t = let (_, args) = unApply (getRetTy t) in
355− any conHead args
356− conHead t | (P _ n _, _) <- unApply t = case lookupDefExact n (tt_ctxt ist) of
357− Just _ -> True
358− _ -> False
359− | otherwise = False
360−
361339-- | Resolve type classes. This will only pick up 'normal' instances, never
362340-- named instances (which is enforced by 'findInstances').
363341resolveTC :: Bool -- ^ using default Int