Inscrutable error message when using case with security co-effect

[vollmerm]

The following program:

incr : Int [Private] → List (Int [Private]) → List (Int [Private])
incr [i] ls =
  case ls of
    Nil → Nil;
    Cons [car] cdr → Cons [car + i] (incr [i] cdr)

Gives this error:

The following theorem associated with `incr` is falsifiable:
	∃ i.0 : Level . (i.0 ≤ Private) ∧ ((0 : Level) ⊔ Private + Private = i.0) ∧ ((((Private × (1 : Nat))) * (((1 : Level) × 1))) + (((Private × (1 : Nat))) * (((1 : Level) × 1))) ≤ ((1 : Level) × 1)) ∧ (Private ≤ Private) ∧ (Private ≤ Private) ∧ ((0 : Nat) = 1)

But the error disappears when folding the case into the function definition:

incr : Int [Private] → List (Int [Private]) → List (Int [Private])
incr [i] Nil = Nil;
incr [i] (Cons [car] cdr) = Cons [car + i] (incr [i] cdr)

At the end of the error message, it seems to be trying to compare 1 to 0, but why is it talking about Nat to begin with?

This is on the dev-minor branch.