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

[dunhamsteve]

Description

This PR fixes #2444, an issue with implicits not showing up under a parameter block containing an implicit parameter.

If a function is in the scope of a an implicit parameter block, its implicits are not visible in the body of the function. For example in this code:

parameters {n : Nat}
    foo : Vect m Nat -> Nat
    foo xs = ?hole

Idris reports the scope of ?hole as:

Main> :ti hole
   {n : Nat}
   xs : Vect m Nat
------------------------------
hole : Nat

Note that m is missing. It behaves the same way after explicitly adding {m : Nat} -> to the signature of foo. But if we change the parameter n to be explicit, m shows up in the hole.

The root cause is in findImps. It attempts to skip over locals, but assumes that they are Explicit. They are explicit in the case when the locals come from a surrounding function, but not necessarily the case when they come from a parameter block. In that case, the default case is hit and the function returns [].

[andrevidela]

looks good to me