Broken matching when mixing literals and constructors?

Stream: general

[Alessandra Simmons]

If you match on a string, you can obviously match using a string literal pattern, but you can also match using its constructor:

def ctor_match :=
  match "Good" with
  | String.ofByteArray _ _ => some 1

However, if you try to mix both kinds of pattern, this seems to break:

def badMatch : Option Nat :=
  match "Bad" with
  | String.ofByteArray _ _ => some 1
  | "Eek" => some 2
  | _ => none -- unknown free variable `_fvar.149`

Notably, this also occurs in previous versions of Lean (from v4.24.0, pre-Unicode scalar changes):

def badMatchOld : Option Nat :=
  match "Bad" with
  | String.mk (List.cons 'B' _) => some 1
  | "Eek" => some 2
  | _ => none -- unknown free variable `_fvar.778`

Am I just misusing these match statements? If so, if I do want to match for just a part of a string, how should I do so?

[Aaron Liu]

String having literal matching is hard-coded into the matcher code, along with the other kinds of literal matching:

• docs#Nat literal matching
• docs#Int literal matching
• docs#Fin literal matching
• docs#BitVec literal matching
• docs#String literal matching
• docs#Char literal matching
• docs#UInt8 literal matching
• docs#UInt16 literal matching
• docs#UInt32 literal matching
• docs#UInt64 literal matching

You can see the list at docs#Lean.Meta.isMatchValue and it's used to determine which values get a docs#Lean.Meta.Match.Pattern.val

[Aaron Liu]

Does the same problem occur with the other kinds of literals or is it just strings?

[Alessandra Simmons]

It does seem to also happen with other literals, for example Char and UInt8:

def charMatch :=
  match 'X' with
  | Char.mk 5 _ => some 1
  | 'A' => some 2
  | _ => none -- unknown free variable `_fvar.836`

def uInt8Match :=
  match (5: UInt8) with
  | UInt8.ofBitVec (BitVec.ofFin 3) => some 1
  | 5 => some 2
  | _ => none -- unknown free variable `_fvar.1026`

[Robin Arnez]

I think there's some point to made about this not being an intended use for match statements but at least it should give a cryptic error message

[Robin Arnez]

Do you mind filing an issue?

[Alessandra Simmons]

Sure, I filed an issue here: https://github.com/leanprover/lean4/issues/11186

[Alessandra Simmons]

I'm curious though, why isn't this intended? I match on constructors for every other type, so I'm not really sure why this wouldn't also be in-scope

[Aaron Liu]

they're special-cased to use the decidable equality instance instead of pattern matching normally

[Aaron Liu]

it only does it for literals of the types listed

[Aaron Liu]

the matcher maker machinery is set up to be able to do it for any type with decidable equality though