diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index fc48e29845..c3087d4d7a 100644 --- a/src/TTImp/TTImp.idr +++ b/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? diff --git a/tests/idris2/reg/reg053/ImplicitParam.idr b/tests/idris2/reg/reg053/ImplicitParam.idr new file mode 100644 index 0000000000..bb8ea518d1 --- /dev/null +++ b/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 + diff --git a/tests/idris2/reg/reg053/Issue2444.idr b/tests/idris2/reg/reg053/Issue2444.idr new file mode 100644 index 0000000000..ed1fa0eb42 --- /dev/null +++ b/tests/idris2/reg/reg053/Issue2444.idr @@ -0,0 +1,4 @@ +parameters {0 res : Type} + fun : {x : Nat} -> Nat + fun = x + diff --git a/tests/idris2/reg/reg053/expected b/tests/idris2/reg/reg053/expected new file mode 100644 index 0000000000..d2cad0378a --- /dev/null +++ b/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) diff --git a/tests/idris2/reg/reg053/input b/tests/idris2/reg/reg053/input new file mode 100644 index 0000000000..371e366b7c --- /dev/null +++ b/tests/idris2/reg/reg053/input @@ -0,0 +1,2 @@ +:ti hole +:q diff --git a/tests/idris2/reg/reg053/run b/tests/idris2/reg/reg053/run new file mode 100644 index 0000000000..1cdbbf80f7 --- /dev/null +++ b/tests/idris2/reg/reg053/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh +idris2 ImplicitParam.idr < input +check Issue2444.idr