Type checking issue with Idris2 Load instruction in dependent context

[weiserhase]

I've encountered a potential type checking bug in Idris2. The issue arises specifically with the Load instruction when it takes an Int argument and operates within a dependent type context. (I did report the issue in the idris2 discord)

Steps to Reproduce

Attempt to compile the provided code snippet.

data Heap : (fs : Maybe a) -> Type where 
data Instr : Heap ht -> Type where
  Load : Int -> Instr hp

Expected Behavior

The code should compile successfully.

Observed Behavior

The type checker produces an error regarding the Load instruction.
Removing the Int -> portion of the Load type signature allows the code to compile.
This issue was initially discovered within a larger Bytecode Interpreter project.
User @dunham provided this simplified example and offered some analysis.

[dunhamsteve]

So this compiles fine:

data Heap : (fs : Maybe a) -> Type where 
data Instr : Heap ht -> Type where
  Load : Instr hp

but this gives us an error:

data Heap : (fs : Maybe a) -> Type where 
data Instr : Heap ht -> Type where
  Load : (z : Int) -> Instr hp

The error shows we can't implicitly bind ht because its type uses an implicit which is abstracted over z. and z is no longer in scope.

Error: While processing constructor Load. 
Can't bind implicit Main.{ht:829} of type (Prelude.Types.Maybe ?Main.{a:828}_[z[0]])

Aside from "oh well", one idea that comes to mind is to solve a:828 with a new implicit a that doesn't depend on z (if the type of a:828 doesn't reference z). I don't know if this is correct or worth the complexity.