Merge pull request #3306 from dunhamsteve/implicitParam

[ fix ] implicits are not in scope under an implicit parameter block

src/TTImp/TTImp.idr

@@ -726,9 +726,10 @@ implicitsAs n defs ns tm
                    Core (List (Name, PiInfo RawImp))
         -- #834 When we are in a local definition, we have an explicit telescope
         -- corresponding to the variables bound in the parent function.
-        -- So we first peel off all of the explicit quantifiers corresponding
-        -- to these variables.
-        findImps ns es (_ :: locals) (NBind fc x (Pi _ _ Explicit _) sc)
+        -- Parameter blocks also introduce additional telescope of implicit, auto,
+        -- and explicit variables. So we first peel off all of the quantifiers
+        -- corresponding to these variables.
+        findImps ns es (_ :: locals) (NBind fc x (Pi _ _ _ _) sc)
           = do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
                findImps ns es locals body
                -- ^ TODO? check that name of the pi matches name of local?

tests/idris2/reg/reg053/ImplicitParam.idr

@@ -0,0 +1,7 @@
+import Data.Vect
+
+-- m was not in scope when n is implicit
+parameters {n : Nat}
+    foo : Vect m Nat -> Nat
+    foo xs = ?hole
+

tests/idris2/reg/reg053/Issue2444.idr

@@ -0,0 +1,4 @@
+parameters {0 res : Type}
+    fun : {x : Nat} -> Nat
+    fun = x
+

tests/idris2/reg/reg053/expected

@@ -0,0 +1,8 @@
+1/1: Building ImplicitParam (ImplicitParam.idr)
+Main>    {n : Nat}
+ 0 m : Nat
+   xs : Vect m Nat
+------------------------------
+hole : Nat
+Main> Bye for now!
+1/1: Building Issue2444 (Issue2444.idr)

tests/idris2/reg/reg053/input

@@ -0,0 +1,2 @@
+:ti hole
+:q

tests/idris2/reg/reg053/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+idris2 ImplicitParam.idr < input
+check Issue2444.idr