@@ -99,10 +99,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
99 conArgsOK ty
99 conArgsOK ty
100 = let (f, as) = unApply ty in
100 = let (f, as) = unApply ty in
101 case f of
101 case f of
102− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
102+ P _ n _ -> case lookupCtxtExact n (idris_datatypes ist) of
103− [t] -> do rs <- mapM (conReady as) (con_names t)
103+ Just t -> do rs <- mapM (conReady as) (con_names t)
104− return (and rs)
104+ return (and rs)
105− _ -> fail "Ambiguous name"
105+ Nothing -> -- local variable, go for it
106 TType _ -> return True
107 TType _ -> return True
107 _ -> fail "Not a data type"
108 _ -> fail "Not a data type"
@@ -158,12 +159,12 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
158 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
159 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
159 Nothing -> []
160 Nothing -> []
160 Just hs -> hs
161 Just hs -> hs
161− case lookupCtxt n (idris_datatypes ist) of
162+ case lookupCtxtExact n (idris_datatypes ist) of
162− [t] -> tryCons d locs (hints ++
163+ Just t -> tryCons d locs (hints ++
163− con_names t ++
164+ con_names t ++
164− autohints ++
165+ autohints ++
165− getFn d fn)
166+ getFn d fn)
166− _ -> fail "Not a data type"
167+ Nothing -> fail "Not a data type"
167 _ -> fail "Not a data type"
168 _ -> fail "Not a data type"
169 -- if there are local variables which have a function type, try
170 -- if there are local variables which have a function type, try
@@ -191,10 +192,9 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
191 -- Like type class resolution, but searching with constructors
192 -- Like type class resolution, but searching with constructors
192 tryCon d locs n =
193 tryCon d locs n =
193 do ty <- goal
194 do ty <- goal
194− let imps = case lookupCtxtName n (idris_implicits ist) of
195+ let imps = case lookupCtxtExact n (idris_implicits ist) of
195− [] -> []
196+ Nothing -> []
196− [args] -> map isImp (snd args)
197+ Just args -> map isImp args
197− _ -> fail "Ambiguous name"
198 ps <- get_probs
198 ps <- get_probs
199 hs <- get_holes
199 hs <- get_holes
200 args <- map snd <$> try' (apply (Var n) imps)
200 args <- map snd <$> try' (apply (Var n) imps)