Difficulty with Lex match_pattern

Stream: general

[Robert Maxton]

Consider the following:

import Mathlib.Data.Sum.Order

variable {α β} [LinearOrder α] [LinearOrder β]

def Foo : α ⊕ₗ β → Type
| .inlₗ _ => Unit
| .inrₗ _ => Bool

def Bar : (x : α ⊕ₗ β) → Foo x
| .inlₗ _ => by
  unfold Foo
| .inrₗ _ => true

[Robert Maxton]

Looking at the infoview at unfold Foo, we see that the goal is

 match Sum.inlₗ a with
| Sum.inl val => Unit
| Sum.inr val => Bool

Specifically, the specialized match patterns Sum.inlₗ, Sum.inrₗ have vanished. When providing simple values like in this example, this isn't an issue, but in other cases -- in particular, instance synthesis -- it becomes much more of an issue, as instances visibility isn't enough to collapse the above to Unit, for example, and lemmas about Lex that assume toLex won't fire.

[Robert Maxton]

Is there a good workaround to this, or is this an argument to replace Lex with a single-field structure instead?

[Eric Paul]

I’ve had similar issues with match with Lex. I think the rough takeaway is that it is an issue and one workaround is to do cases' x with x; obtain x | x := x.

Here are some relevant conversations:
#new members > match with toLex
#mathlib4 > Obtain misses `toLex`
#mathlib4 > Modify how rcases matches