Miscompilation of `Nat` literals

[Z-snails]

toNat : Nat -> () -> Nat
toNat 0 () = 1
toNat _ _ = 1

Steps to Reproduce

Load this file in idris2, then run :di toNat

Expected Behavior

Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
  { 0 => 1
  ; _ => 1
  }

or

Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
  { 0 => 1 + 0
  ; _ => 1
  }

or similar

Observed Behavior

Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
  { 0 => Prelude.Types.S {tag = 1} [succ] 0
  ; _ => 1
  }

This produces the wrong thing, eg on chez you get (vector 1 0) instead of 1

[Z-snails]

Also one thing I noticed, the bug is fragile e.g. removing either argument or not pattern matching on either of them suddenly fixes it.