Match breaking with match_pattern function

Stream: new members

[Jacob]

Any reason why Char.ofNat 0 breaks the pattern matching? When replaced with the Char literal it works as expected. Thank you.

def foo (x : Char) : Nat :=
  match x with
  | Char.ofNat 0 => 1
  | 'a' => 2
  | _ => 0

Lean 4: unknown free variable '_uniq.1738'

def foo (x : Char) : Nat :=
  match x with
  | Char.ofNat 1 => 1
  | Char.ofNat 0 => 2
  | _ => 3

Lean 4: tactic 'cases' failed, nested error: tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop

def foo (x : Char) : Nat :=
  match x with
  | 'a' => 1
  | 'b' => 2
  | _ => 3

Works as expected

[Mario Carneiro]

Is Char.ofNat even a constructor?

[Henrik Böving]

No but it is marked with match_pattern

[Jacob]

Mario Carneiro said:

Is Char.ofNat even a constructor?

Yes you are right, not a constructor. But a helpful individual on a lean discord channel did mention that the function being tagged with match_pattern should mean it works? But I am very new to lean, so I don't understand it really.

[Mario Carneiro]

match_pattern means it is not immediately rejected, but it is unfolded and the resulting expression might not be suitable as a pattern

[Mario Carneiro]

I guess from the annotation that there is some expectation that this works in at least some cases

[Mario Carneiro]

I think there must be some shenanigans going on because 'a' expands to Char.ofNat 97 yet using one in place of the other in pattern position changes the pattern match behavior

[Mario Carneiro]

It's probably directly matching the syntax looking for a char literal

[Mario Carneiro]

note that using the basic match compiler here would generate a really bad implementation, containing 97 case splits on the underlying Nat

[Mario Carneiro]

I believe matches on characters and strings are handled specially, to produce an if-else-if split

[Mario Carneiro]

I wonder if you can get a Char pattern match to be exhaustive if you list all 1114112 possibilities

[Henrik Böving]

I would say that the Lean compiler would pprobably give in long before that match size