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

@@ -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

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)

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 : _} ->

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 =>

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

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

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

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 | 

tests/idris2/reg049/expected

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

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

tests/idris2/reg049/run

@@ -0,0 +1,2 @@
+rm -rf build
+$1 --no-banner --no-color --console-width 0 lettype.idr --check -p contrib