Check current holes only at end of elaboration

Fixes #1140 - when checking holes were solved, we checked all of them,
but there may still be some open if there's a local definition.

src/Core/UnifyState.idr

@@ -576,12 +576,12 @@ checkDelayedHoles
 -- not guarded by a unification problem (in which case, report that the unification
 -- problem is unsolved) and it doesn't depend on an implicit pattern variable
 -- (in which case, perhaps suggest binding it explicitly)
-export
 checkValidHole : {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
-                 (Int, (FC, Name)) -> Core ()
-checkValidHole (idx, (fc, n))
-    = do defs <- get Ctxt
+                 Int -> (Int, (FC, Name)) -> Core ()
+checkValidHole base (idx, (fc, n))
+  = if base > idx then pure () else
+      do defs <- get Ctxt
          ust <- get UST
          Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
               | Nothing => pure ()
@@ -622,14 +622,14 @@ checkValidHole (idx, (fc, n))
 -- Also throw an error if there are unresolved guarded constants or
 -- unsolved searches
 export
-checkUserHoles : {auto u : Ref UST UState} ->
-                 {auto c : Ref Ctxt Defs} ->
-                 Bool -> Core ()
-checkUserHoles now
+checkUserHolesAfter : {auto u : Ref UST UState} ->
+                      {auto c : Ref Ctxt Defs} ->
+                      Int -> Bool -> Core ()
+checkUserHolesAfter base now
     = do gs_map <- getGuesses
          let gs = toList gs_map
          log "unify.unsolved" 10 $ "Unsolved guesses " ++ show gs
-         traverse_ checkValidHole gs
+         traverse_ (checkValidHole base) gs
          hs_map <- getCurrentHoles
          let hs = toList hs_map
          let hs' = if any isUserName (map (snd . snd) hs)
@@ -643,6 +643,12 @@ checkUserHoles now
     nameEq : (a, b, Name) -> (a, b, Name) -> Bool
     nameEq (_, _, x) (_, _, y) = x == y
 
+export
+checkUserHoles : {auto u : Ref UST UState} ->
+                 {auto c : Ref Ctxt Defs} ->
+                 Bool -> Core ()
+checkUserHoles = checkUserHolesAfter 0
+
 export
 checkNoGuards : {auto u : Ref UST UState} ->
                 {auto c : Ref Ctxt Defs} ->

src/TTImp/Elab.idr

@@ -157,15 +157,15 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
          -- Linearity and hole checking.
          -- on the LHS, all holes need to have been solved
          chktm <- the (Core (Term vars)) $ case mode of
-              InLHS _ => do when (not incase) $ checkUserHoles True
+              InLHS _ => do when (not incase) $ checkUserHolesAfter constart True
                             pure chktm
-              InTransform => do when (not incase) $ checkUserHoles True
+              InTransform => do when (not incase) $ checkUserHolesAfter constart True
                                 pure chktm
               -- elsewhere, all unification problems must be
               -- solved, though we defer that if it's a case block since we
               -- might learn a bit more later.
               _ => if (not incase)
-                      then do checkUserHoles (inTrans || inPE)
+                      then do checkUserHolesAfter constart (inTrans || inPE)
                               linearCheck (getFC tm) rigc False env chktm
                           -- Linearity checking looks in case blocks, so no
                           -- need to check here.

tests/Main.idr

@@ -122,7 +122,7 @@ idrisTestsRegression = MkTestPool []
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
        "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
-       "reg036"]
+       "reg036", "reg037"]
 
 idrisTests : TestPool
 idrisTests = MkTestPool []

tests/idris2/reg037/Test.idr

@@ -0,0 +1,21 @@
+module Test
+
+data A = A0
+
+giveA : HasIO io => io A
+giveA = pure A0
+
+please : HasIO io => io ()
+please = do
+     value_a <- giveA
+
+     let a : A
+         a = value_a
+
+     pure ()
+
+interface Cool a where cool : a -> a
+implementation Cool A where cool x = x
+
+help : A
+help = cool (let x : String; x = "hello" in A0)

tests/idris2/reg037/expected

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

tests/idris2/reg037/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 Test.idr --check
+
+rm -rf build