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

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

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

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 ()
 

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