Fix possible loop in auto implicit search

A local variable can't be applied to itself when searching (otherwise,
for example, we could end up trying something like id id id id id id etc
forever). So remove it from the environment before searching for its
arguments.

This and the previous patch fix #24. (Or, at least, the minimised cases
reported as part of it!)
This commit is contained in:
Edwin Brady 2019-07-22 11:19:10 +01:00
parent 0e4c610f56
commit 91262b4800
6 changed files with 31 additions and 4 deletions

View File

@ -217,6 +217,17 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env ((prf, ty) :: r
findPos defs prf id nty target)
(searchLocalWith fc rigc defaults trying depth def top env rest target)
where
clearEnvType : {idx : Nat} -> .(IsVar name idx vs) ->
FC -> Env Term vs -> Env Term vs
clearEnvType First fc (b :: env)
= Lam (multiplicity b) Explicit (Erased fc) :: env
clearEnvType (Later p) fc (b :: env) = b :: clearEnvType p fc env
clearEnv : Term vars -> Env Term vars -> Env Term vars
clearEnv (Local fc _ idx p) env
= clearEnvType p fc env
clearEnv _ env = env
findDirect : Defs -> Term vars ->
(Term vars -> Term vars) ->
NF vars -> -- local's type
@ -225,6 +236,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env ((prf, ty) :: r
findDirect defs prf f ty target
= do (args, appTy) <- mkArgs fc rigc env ty
logNF 10 "Trying" env ty
logNF 10 "For target" env target
ures <- unify InTerm fc env target appTy
let [] = constraints ures
| _ => throw (CantSolveGoal fc [] top)
@ -233,9 +245,12 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env ((prf, ty) :: r
then do
let candidate = apply fc (f prf) (map metaApp args)
logTermNF 10 "Local var candidate " env candidate
-- Clear the local from the environment to avoid getting
-- into a loop repeatedly applying it
let env' = clearEnv prf env
-- Work right to left, because later arguments may solve
-- earlier ones by unification
traverse (searchIfHole fc defaults trying False depth def top env)
traverse (searchIfHole fc defaults trying False depth def top env')
(reverse args)
pure candidate
else do logNF 10 "Can't use " env ty

View File

@ -222,7 +222,8 @@ checkLHS {vars} mult hashit n opts nest env fc lhs_in
autoImplicits autoimp
lhs <- implicitsAs defs vars lhs_bound
log 5 $ "Checking " ++ show lhs
log 5 $ "Checking LHS of " ++ show !(getFullName (Resolved n)) ++
" " ++ show lhs
logEnv 5 "In env" env
(lhstm, lhstyg) <-
wrapError (InLHS fc !(getFullName (Resolved n))) $

View File

@ -37,7 +37,7 @@ idrisTests
"interactive005", "interactive006", "interactive007", "interactive008",
"interactive009", "interactive010", "interactive011", "interactive012",
"interface001", "interface002", "interface003", "interface004",
"interface005", "interface006",
"interface005", "interface006", "interface007",
"lazy001",
"linear001", "linear002", "linear003", "linear004", "linear005",
"linear006", "linear007",

View File

@ -0,0 +1,7 @@
module A
-- Check that this doesn't go into a loop when resolving Show. because
-- f itself is a candidate when elaborating the top level f function!
public export
interface F (p : Type -> Type) where
f : Show a => p a -> a

View File

@ -0,0 +1 @@
1/1: Building A (A.idr)

3
tests/idris2/interface007/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check A.idr
rm -rf build