From edefd543f703547834a006220183040277d5579b Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 20 Jul 2021 16:21:40 +0100 Subject: [PATCH] A bit of refactoring of argument elaboration order In theory argument elaboration order doesn't matter, but in practice we sometimes make choices for performance reasons, like helping with disambiguation by knowing the target type. This was kind of messy, now we can more clearly see what's going on. Also, more importantly, it gives us a bit more control which we sometimes need. For example, if we go choose to go right to left for some performance heuristic it might turn out we don't have enough information yet, in which case we need to delay and try again later. Fixes #1743 --- src/TTImp/Elab/Ambiguity.idr | 4 ++-- src/TTImp/Elab/App.idr | 32 ++++++++++++++++++++++++++++++-- src/TTImp/Elab/Delayed.idr | 12 ++++++++++-- src/TTImp/Elab/Lazy.idr | 2 +- src/TTImp/Elab/Record.idr | 2 +- src/TTImp/Elab/Rewrite.idr | 2 +- tests/Main.idr | 2 +- tests/idris2/error018/expected | 2 +- tests/idris2/reg049/expected | 1 + tests/idris2/reg049/lettype.idr | 15 +++++++++++++++ tests/idris2/reg049/run | 2 ++ 11 files changed, 65 insertions(+), 11 deletions(-) create mode 100644 tests/idris2/reg049/expected create mode 100644 tests/idris2/reg049/lettype.idr create mode 100755 tests/idris2/reg049/run diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 6426a31b9..53c99030b 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -353,7 +353,7 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected let solvemode = case elabMode elabinfo of InLHS c => inLHS _ => inTerm - delayOnFailure fc rig env expected ambiguous Ambiguity $ + delayOnFailure fc rig env (Just expected) ambiguous Ambiguity $ \delayed => do solveConstraints solvemode Normal defs <- get Ctxt @@ -406,7 +406,7 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected let solvemode = case elabMode elabinfo of InLHS c => inLHS _ => inTerm - delayOnFailure fc rig env expected ambiguous Ambiguity $ + delayOnFailure fc rig env (Just expected) ambiguous Ambiguity $ \delayed => do defs <- get Ctxt exp <- getTerm expected diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 89d0881f6..1d8ba4a26 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -422,7 +422,30 @@ mutual then pure True else do sc' <- sc defs (toClosure defaultOpts env (Erased fc False)) concrete defs env sc' - if (isHole aty && kr) || !(needsDelay (elabMode elabinfo) kr arg_in) then do + -- In theory we can check the arguments in any order. But it turns + -- out that it's sometimes better to do the rightmost arguments + -- first to give ambiguity resolution more to work with. So + -- we do that if the target type is unknown, or if we see that + -- the raw term is otherwise worth delaying. + if (isHole aty && kr) || !(needsDelay (elabMode elabinfo) kr arg_in) + then handle (checkRtoL kr arg) + -- if the type isn't resolved, we might encounter an + -- implicit that we can't use yet because we don't know + -- about it. In that case, revert to LtoR + (\err => if invalidArg err + then checkLtoR kr arg + else throw err) + else checkLtoR kr arg + where + invalidArg : Error -> Bool + invalidArg (InvalidArgs{}) = True + invalidArg _ = False + + checkRtoL : Bool -> -- return type is known + RawImp -> -- argument currently being checked + Core (Term vars, Glued vars) + checkRtoL kr arg + = do defs <- get Ctxt nm <- genMVName x empty <- clearDefs defs metaty <- quote empty env aty @@ -483,7 +506,12 @@ mutual _ => pure () removeHole idx pure (tm, gty) - else do + + checkLtoR : Bool -> -- return type is known + RawImp -> -- argument currently being checked + Core (Term vars, Glued vars) + checkLtoR kr arg + = do defs <- get Ctxt logNF "elab" 10 ("Argument type " ++ show x) env aty logNF "elab" 10 ("Full function type") env (NBind fc x (Pi fc argRig Explicit aty) sc) diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index e56db38a8..97b113775 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -63,18 +63,19 @@ delayOnFailure : {vars : _} -> {auto u : Ref UST UState} -> {auto e : Ref EST (EState vars)} -> FC -> RigCount -> Env Term vars -> - (expected : Glued vars) -> + (expected : Maybe (Glued vars)) -> (Error -> Bool) -> (pri : DelayReason) -> (Bool -> Core (Term vars, Glued vars)) -> Core (Term vars, Glued vars) -delayOnFailure fc rig env expected pred pri elab +delayOnFailure fc rig env exp pred pri elab = do est <- get EST ust <- get UST let nos = noSolve ust -- remember the holes we shouldn't solve handle (elab False) (\err => do est <- get EST + expected <- mkExpected exp if pred err then do nm <- genName "delayed" @@ -99,6 +100,13 @@ delayOnFailure fc rig env expected pred pri elab ust) pure (dtm, expected) else throw err) + where + mkExpected : Maybe (Glued vars) -> Core (Glued vars) + mkExpected (Just ty) = pure ty + mkExpected Nothing + = do nm <- genName "delayTy" + ty <- metaVar fc erased env nm (TType fc) + pure (gnf env ty) export delayElab : {vars : _} -> diff --git a/src/TTImp/Elab/Lazy.idr b/src/TTImp/Elab/Lazy.idr index 25b33251d..1e7d20bdf 100644 --- a/src/TTImp/Elab/Lazy.idr +++ b/src/TTImp/Elab/Lazy.idr @@ -50,7 +50,7 @@ checkDelay rig elabinfo nest env fc tm mexpected solveConstraints solvemode Normal -- Can only check if we know the expected type already because we -- need to infer the delay reason - delayOnFailure fc rig env expected delayError LazyDelay + delayOnFailure fc rig env (Just expected) delayError LazyDelay (\delayed => case !(getNF expected) of NDelayed _ r expnf => diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index d44957ef0..f8c5f7664 100644 --- a/src/TTImp/Elab/Record.idr +++ b/src/TTImp/Elab/Record.idr @@ -221,7 +221,7 @@ checkUpdate rig elabinfo nest env fc upds rec expected let solvemode = case elabMode elabinfo of InLHS c => inLHS _ => inTerm - delayOnFailure fc rig env recty needType RecordUpdate $ + delayOnFailure fc rig env (Just recty) needType RecordUpdate $ \delayed => do solveConstraints solvemode Normal exp <- getTerm recty diff --git a/src/TTImp/Elab/Rewrite.idr b/src/TTImp/Elab/Rewrite.idr index 952244370..7efb5fe46 100644 --- a/src/TTImp/Elab/Rewrite.idr +++ b/src/TTImp/Elab/Rewrite.idr @@ -108,7 +108,7 @@ checkRewrite : {vars : _} -> checkRewrite rigc elabinfo nest env fc rule tm Nothing = throw (GenericMsg fc "Can't infer a type for rewrite") checkRewrite {vars} rigc elabinfo nest env ifc rule tm (Just expected) - = delayOnFailure ifc rigc env expected rewriteErr Rewrite $ \delayed => + = delayOnFailure ifc rigc env (Just expected) rewriteErr Rewrite $ \delayed => do let vfc = virtualiseFC ifc (rulev, grulet) <- check erased elabinfo nest env rule Nothing rulet <- getTerm grulet diff --git a/tests/Main.idr b/tests/Main.idr index 1637adbe4..c6dd8ce13 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -128,7 +128,7 @@ idrisTestsRegression = MkTestPool "Various regressions" [] Nothing "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035", "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042", - "reg043", "reg044", "reg045", "reg046", "reg047", "reg048"] + "reg043", "reg044", "reg045", "reg046", "reg047", "reg048", "reg049"] idrisTestsData : TestPool idrisTestsData = MkTestPool "Data and record types" [] Nothing diff --git a/tests/idris2/error018/expected b/tests/idris2/error018/expected index b0316837e..01945db43 100644 --- a/tests/idris2/error018/expected +++ b/tests/idris2/error018/expected @@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7 1/1: Building Issue1031-4 (Issue1031-4.idr) Error: While processing left hand side of nice. Unsolved holes: -Main.{dotTm:373} introduced at: +Main.{dotTm:404} introduced at: Issue1031-4:4:6--4:10 1 | %default total 2 | diff --git a/tests/idris2/reg049/expected b/tests/idris2/reg049/expected new file mode 100644 index 000000000..a2cd4d4f6 --- /dev/null +++ b/tests/idris2/reg049/expected @@ -0,0 +1 @@ +1/1: Building lettype (lettype.idr) diff --git a/tests/idris2/reg049/lettype.idr b/tests/idris2/reg049/lettype.idr new file mode 100644 index 000000000..aaa9703ef --- /dev/null +++ b/tests/idris2/reg049/lettype.idr @@ -0,0 +1,15 @@ +works : (n : (Nat, Nat)) -> + let mk = n in + {y : Bool} -> (z : Bool) -> String +works (m, k) {y} z = ?h1 + +FailType : (Nat, Nat) -> Type +FailType (m, k) = {y : Bool} -> (z : Bool) -> String + +fails : (n : (Nat, Nat)) -> FailType n +fails (m, k) {y} z = ?h2 + +fails2 : (n : (Nat, Nat)) -> + let (m, k) = n in + {y : Bool} -> (z : Bool) -> String +fails2 (m, k) {y} z = ?h3 diff --git a/tests/idris2/reg049/run b/tests/idris2/reg049/run new file mode 100755 index 000000000..d10f3201c --- /dev/null +++ b/tests/idris2/reg049/run @@ -0,0 +1,2 @@ +rm -rf build +$1 --no-banner --no-color --console-width 0 lettype.idr --check -p contrib