From 4273c244348353c29daa189526856b9e8764ec47 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Fri, 22 May 2020 09:35:55 +0100
Subject: [PATCH] Don't rerun delayed elaborators so often

Run once ignoring errors to make progress on interfaces/determining
arguments, then again in full. Second step isn't needed since it was
just covering up an earlier bug.
This means that some errors under lots of delays are reported quicker,
though I still haven't completely got to the bottom of that one.
---
 src/Idris/Elab/Implementation.idr |  2 +-
 src/TTImp/Elab/Case.idr           |  8 ++++++++
 src/TTImp/Elab/Delayed.idr        | 26 +++++++++++---------------
 src/TTImp/Elab/Local.idr          |  8 ++++++++
 4 files changed, 28 insertions(+), 16 deletions(-)

diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index e0edbdadf..f7118ed7c 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -185,7 +185,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                fns <- topMethTypes [] impName methImps impsp (params cdata)
                                       (map fst (methods cdata))
                                       (methods cdata)
-               traverse (processDecl [] nest env) (map mkTopMethDecl fns)
+               traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
 
                -- 3. Build the record for the implementation
                let mtops = map (Builtin.fst . snd) fns
diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr
index b0e2e8897..ba1f55ca4 100644
--- a/src/TTImp/Elab/Case.idr
+++ b/src/TTImp/Elab/Case.idr
@@ -226,7 +226,15 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- Start with empty nested names, since we've extended the rhs with
          -- ICaseLocal so they'll get rebuilt with the right environment
          let nest' = MkNested []
+         ust <- get UST
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- case block, because they're not going to make progress until
+         -- we come out again, so save them
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          processDecl [InCase] nest' [] (IDef fc casen alts')
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
 
          pure (appTm, gnf env caseretty)
   where
diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr
index 5f076dd6b..0438449f0 100644
--- a/src/TTImp/Elab/Delayed.idr
+++ b/src/TTImp/Elab/Delayed.idr
@@ -71,7 +71,7 @@ delayOnFailure fc rig env expected pred pri elab
          handle (elab False)
           (\err =>
               do est <- get EST
-                 if pred err && delayDepth est < !getAmbigLimit
+                 if pred err
                     then
                       do nm <- genName "delayed"
                          (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
@@ -99,19 +99,16 @@ delayElab : {vars : _} ->
             Core (Term vars, Glued vars)
 delayElab {vars} fc rig env exp pri elab
     = do est <- get EST
-         if delayDepth est >= !getAmbigLimit
-            then elab
-            else do
-             nm <- genName "delayed"
-             expected <- mkExpected exp
-             (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
-             logGlueNF 5 ("Postponing elaborator " ++ show nm ++
-                          " for") env expected
-             ust <- get UST
-             put UST (record { delayedElab $=
-                     ((pri, ci, mkClosedElab fc env (deeper elab)) :: ) }
-                             ust)
-             pure (dtm, expected)
+         nm <- genName "delayed"
+         expected <- mkExpected exp
+         (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
+         logGlueNF 5 ("Postponing elaborator " ++ show nm ++
+                      " for") env expected
+         ust <- get UST
+         put UST (record { delayedElab $=
+                 ((pri, ci, mkClosedElab fc env elab) :: ) }
+                         ust)
+         pure (dtm, expected)
   where
     mkExpected : Maybe (Glued vars) -> Core (Glued vars)
     mkExpected (Just ty) = pure ty
@@ -196,7 +193,6 @@ retryDelayed : {vars : _} ->
 retryDelayed ds
     = do est <- get EST
          ds <- retryDelayed' NoError [] ds -- try everything again
-         ds <- retryDelayed' AmbigError [] ds -- fail on ambiguity error
          retryDelayed' AllErrors [] ds -- fail on all errors
          pure ()
 
diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr
index 2cb0e6337..917f4590e 100644
--- a/src/TTImp/Elab/Local.idr
+++ b/src/TTImp/Elab/Local.idr
@@ -37,7 +37,15 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
                                            -- fixes bug #115
          let nest' = record { names $= (names' ++) } nest
          let env' = dropLinear env
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- locals  block, because they're not going to make progress until
+         -- we come out again, so save them
+         ust <- get UST
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
          check rig elabinfo nest' env scope expty
   where
     -- For the local definitions, don't allow access to linear things