unreachable match case

Stream: lean4

[Arthur Paulino]

Is it possible to replace the unreachable! with some proof that any other possibility except for bool _ is unreachable because the return of Literal.eq is always a Literal.bool?

inductive Literal
  | bool  : Bool   → Literal
  | int   : Int    → Literal
  | float : Float  → Literal
  | str   : String → Literal

def Literal.eq : Literal → Literal → Literal
  | bool  bₗ, bool  bᵣ => bool $ bₗ == bᵣ
  | int   iₗ, int   iᵣ => bool $ iₗ == iᵣ
  | float fₗ, float fᵣ => bool $ fₗ == fᵣ
  | int   iₗ, float fᵣ => bool $ (.ofInt iₗ) == fᵣ
  | float fₗ, int   iᵣ => bool $ fₗ == (.ofInt iᵣ)
  | str   sₗ, str   sᵣ => bool $ sₗ == sᵣ
  | _       , _        => bool false

def Literal.isEq (l r : Literal) : Bool :=
  match h : l.eq r with
  | .bool b => b
  | x       => unreachable!

[Sebastian Ullrich]

There may be various workarounds, but have you considered making Literal (and, presumably, other similar types) "intrinsically typed" by parameterizing/indexing it with the type of the value it carries? Then Literal.eq could have type Literal t -> Literal t -> Literal .bool.

[Sebastian Ullrich]

Whether that is a good idea in the greater context depends on a few other things, e.g. on how complex your type system is.

[Arthur Paulino]

In my case I need all Literals to be of the same type so I can have, for instance, List Literal with heterogeneous inner types