Runtime crash when solving relevant meta in irrelevant position

[kontheocharis]

Steps to Reproduce

import Data.Fin

%default total

parameters (0 bang : Nat -> Nat)
  foo : Nat -> Nat
  foo = ?

  bar : (n : Nat) -> Fin (foo n)
  bar n = FZ {k = bang n}

main : IO ()
main = putStrLn $ show $ foo (\x => x) 3

Expected Behavior

Should not typecheck because hole in foo cannot be solved with an irrelevant term bang

Observed Behavior

Typechecks fine, program crashes with

Exception: invalid memory reference.  Some debugging context lost

Something is not right with the quantity check after metas have been solved.

[kontheocharis]

Actually seems like a duplicate of

https://github.com/idris-lang/Idris2/issues/3367

[dunhamsteve]

Here is a version with the parameters desugared. I wanted to double check there wasn't a parameters bug involved here:

import Data.Fin

%default total

foo : (0 bang : Nat -> Nat) -> Nat -> Nat
foo bang = ?

bar : (0 bang : Nat -> Nat) -> (n : Nat) -> Fin (foo bang n)
bar bang n = FZ {k = bang n}

main : IO ()
main = putStrLn $ show $ foo (\x => x) 3