From ff7c0fa3c24cfb2fdab56aa93f6b085677b8a029 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Tue, 6 Aug 2024 17:18:59 +0300 Subject: [PATCH] [ fix ] Make searching in pairs to not cause ambiguity when there isn't (#3366) * [ test ] Move wrongly placed test * [ cleanup ] Remove one unused argument * [ refactor ] Support normalisation inside the proof modification fun * [ fix ] Normalise `fst`s and `snd`s and remove duplicates in autosearch --- src/Core/AutoSearch.idr | 39 +++++++++--------- .../error031}/Issue1236.idr | 0 .../{error028 => error/error031}/expected | 0 tests/idris2/{error028 => error/error031}/run | 0 .../interface033/PairErroneouslyFound.idr | 40 +++++++++++++++++++ tests/idris2/interface/interface033/expected | 1 + tests/idris2/interface/interface033/run | 3 ++ 7 files changed, 64 insertions(+), 19 deletions(-) rename tests/idris2/{error028 => error/error031}/Issue1236.idr (100%) rename tests/idris2/{error028 => error/error031}/expected (100%) rename tests/idris2/{error028 => error/error031}/run (100%) create mode 100644 tests/idris2/interface/interface033/PairErroneouslyFound.idr create mode 100644 tests/idris2/interface/interface033/expected create mode 100644 tests/idris2/interface/interface033/run diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index ff9c8fe6f..2c4441c6d 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -181,7 +181,7 @@ exactlyOne fc env top target [elab] _ => throw $ CantSolveGoal fc (gamma !(get Ctxt)) [] top Nothing exactlyOne {vars} fc env top target all = do elabs <- successful all - case rights elabs of + case nubBy ((==) `on` fst) $ rights elabs of [(res, defs, ust)] => do put UST ust put Ctxt defs @@ -270,7 +270,7 @@ searchLocalWith : {vars : _} -> searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) target = do defs <- get Ctxt nty <- nf defs env ty - findPos defs prf id nty target + findPos defs pure nty target where clearEnvType : {idx : Nat} -> (0 p : IsVar nm idx vs) -> FC -> Env Term vs -> Env Term vs @@ -283,14 +283,15 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe = clearEnvType p fc env clearEnv _ env = env - findDirect : Defs -> Term vars -> - (Term vars -> Term vars) -> + findDirect : Defs -> + (Term vars -> Core (Term vars)) -> NF vars -> -- local's type (target : NF vars) -> Core (Term vars) - findDirect defs p f ty target + findDirect defs f ty target = do (args, appTy) <- mkArgs fc rigc env ty - logTermNF "auto" 10 "Trying" env (f prf) + fprf <- f prf + logTermNF "auto" 10 "Trying" env fprf logNF "auto" 10 "Type" env ty logNF "auto" 10 "For target" env target ures <- unify inTerm fc env target appTy @@ -299,7 +300,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe -- We can only use the local if its type is not an unsolved hole if !(usableLocal fc defaults env ty) then do - let candidate = apply fc (f prf) (map metaApp args) + let candidate = apply fc fprf (map metaApp args) logTermNF "auto" 10 "Local var candidate " env candidate -- Clear the local from the environment to avoid getting -- into a loop repeatedly applying it @@ -312,13 +313,13 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe else do logNF "auto" 10 "Can't use " env ty throw (CantSolveGoal fc (gamma defs) [] top Nothing) - findPos : Defs -> Term vars -> - (Term vars -> Term vars) -> + findPos : Defs -> + (Term vars -> Core (Term vars)) -> NF vars -> -- local's type (target : NF vars) -> Core (Term vars) - findPos defs p f nty@(NTCon pfc pn _ _ [(_, xty), (_, yty)]) target - = tryUnifyUnambig (findDirect defs prf f nty target) $ + findPos defs f nty@(NTCon pfc pn _ _ [(_, xty), (_, yty)]) target + = tryUnifyUnambig (findDirect defs f nty target) $ do fname <- maybe (throw (CantSolveGoal fc (gamma defs) [] top Nothing)) pure !fstName @@ -331,22 +332,22 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe ytytm <- quote empty env yty exactlyOne fc env top target [(do xtynf <- evalClosure defs xty - findPos defs p - (\arg => apply fc (Ref fc Func fname) + findPos defs + (\arg => normalise defs env $ apply fc (Ref fc Func fname) [xtytm, ytytm, - f arg]) + !(f arg)]) xtynf target), (do ytynf <- evalClosure defs yty - findPos defs p - (\arg => apply fc (Ref fc Func sname) + findPos defs + (\arg => normalise defs env $ apply fc (Ref fc Func sname) [xtytm, ytytm, - f arg]) + !(f arg)]) ytynf target)] else throw (CantSolveGoal fc (gamma defs) [] top Nothing) - findPos defs p f nty target - = findDirect defs p f nty target + findPos defs f nty target + = findDirect defs f nty target searchLocalVars : {vars : _} -> {auto c : Ref Ctxt Defs} -> diff --git a/tests/idris2/error028/Issue1236.idr b/tests/idris2/error/error031/Issue1236.idr similarity index 100% rename from tests/idris2/error028/Issue1236.idr rename to tests/idris2/error/error031/Issue1236.idr diff --git a/tests/idris2/error028/expected b/tests/idris2/error/error031/expected similarity index 100% rename from tests/idris2/error028/expected rename to tests/idris2/error/error031/expected diff --git a/tests/idris2/error028/run b/tests/idris2/error/error031/run similarity index 100% rename from tests/idris2/error028/run rename to tests/idris2/error/error031/run diff --git a/tests/idris2/interface/interface033/PairErroneouslyFound.idr b/tests/idris2/interface/interface033/PairErroneouslyFound.idr new file mode 100644 index 000000000..49c0bf15b --- /dev/null +++ b/tests/idris2/interface/interface033/PairErroneouslyFound.idr @@ -0,0 +1,40 @@ +data X = MkX + +useX : X => Nat + +v : (X, String) + +f : Nat +f = do + let (x, _) = v + useX + +f' : Nat +f' = do + let xx = v + useX + +g : Nat +g = do + let xx@(x, _) = v + useX + +g' : Monad m => m Nat +g' = do + (x, _) <- pure v + pure useX + +g'' : Monad m => m Nat +g'' = do + xx@(x, _) <- pure v + pure useX + +data Y = MkY + +failing "Multiple solutions found" + bad1 : X => Y => X => Nat + bad1 = useX + +failing "Multiple solutions found" + bad2 : (X, Y) => X => Nat + bad2 = useX diff --git a/tests/idris2/interface/interface033/expected b/tests/idris2/interface/interface033/expected new file mode 100644 index 000000000..93bb50bed --- /dev/null +++ b/tests/idris2/interface/interface033/expected @@ -0,0 +1 @@ +1/1: Building PairErroneouslyFound (PairErroneouslyFound.idr) diff --git a/tests/idris2/interface/interface033/run b/tests/idris2/interface/interface033/run new file mode 100644 index 000000000..144743eff --- /dev/null +++ b/tests/idris2/interface/interface033/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check PairErroneouslyFound.idr