Holes at unerased quantity produce bad code

[dunhamsteve]

Steps to Reproduce

The compiler produces produces bad scheme code for the following:

total
fun : Nat -> Nat
fun k = ?fun_rhs

total
fun_proof : (x : Nat) -> fun x = x + 2
fun_proof x = Refl

main : IO ()
main = do
  let x = fun 42
  putStrLn . show $ x

The scheme output is:

(define Main-fun_rhs (lambda (ext-0) (+ ext-0 2)))
(define Main-fun (lambda (arg-0) (Main-fun_rhs 'erased)))

Here ?fun_rhs is being solved when checking the Refl and then substituted into fun with 'erased as an argument instead of arg-0. This also happens when _ or ? is used in place of ?fun_rhs.

Observed Behavior

The code compiles without error or warning and crashes with Exception in +: erased is not a number (and s similar message on javasacript).

Expected Behavior

I believe correct code should be produced or a warning / error should be presented. I'm not sure if we intend for named holes to be solved. I see a SolvedNameHole error in Idris, but it is never thrown.

If _ and ? are allowed to be used at a non-erased quantity, we should get the arguments right. Otherwise, we should emit an error when they are used at a non-erased quantity.

Are named holes allowed to be solved? And are we allowed to use _ and ? to be used in unerased contexts?