@@ -99,10 +99,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
9999 conArgsOK ty
100100 = let (f, as) = unApply ty in
101101 case f of
102− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
103− [t] -> do rs <- mapM (conReady as) (con_names t)
104− return (and rs)
105− _ -> fail "Ambiguous name"
102+ P _ n _ -> case lookupCtxtExact n (idris_datatypes ist) of
103+ Just t -> do rs <- mapM (conReady as) (con_names t)
104+ return (and rs)
105+ Nothing -> -- local variable, go for it
106+ return True
106107 TType _ -> return True
107108 _ -> fail "Not a data type"
108109
@@ -158,12 +159,12 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
158159 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
159160 Nothing -> []
160161 Just hs -> hs
161− case lookupCtxt n (idris_datatypes ist) of
162− [t] -> tryCons d locs (hints ++
163− con_names t ++
164− autohints ++
165− getFn d fn)
166− _ -> fail "Not a data type"
162+ case lookupCtxtExact n (idris_datatypes ist) of
163+ Just t -> tryCons d locs (hints ++
164+ con_names t ++
165+ autohints ++
166+ getFn d fn)
167+ Nothing -> fail "Not a data type"
167168 _ -> fail "Not a data type"
168169
169170 -- 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
191192 -- Like type class resolution, but searching with constructors
192193 tryCon d locs n =
193194 do ty <- goal
194− let imps = case lookupCtxtName n (idris_implicits ist) of
195− [] -> []
196− [args] -> map isImp (snd args)
197− _ -> fail "Ambiguous name"
195+ let imps = case lookupCtxtExact n (idris_implicits ist) of
196+ Nothing -> []
197+ Just args -> map isImp args
198198 ps <- get_probs
199199 hs <- get_holes
200200 args <- map snd <$> try' (apply (Var n) imps)