instance DecidableEq ByteArray

Stream: lean4

[Ilona Prikule]

There seems to be no DecidableEq instance for ByteArray, so I wanted to declare one. Both the deriving:

deriving instance DecidableEq for ByteArray

#eval ByteArray.empty = ByteArray.empty

and trying to prove it by hand:

instance : DecidableEq ByteArray
  | ⟨a⟩, ⟨b⟩ => match decEq a b with
    | isTrue h₁  => isTrue $ congrArg ByteArray.mk h₁
    | isFalse h₂ => isFalse (fun p => by cases p; cases (h₂ rfl))

#eval ByteArray.empty = ByteArray.empty

cause Lean server to crash and lean to fail with an error: error: external command /home/ix/.elan/toolchains/leanprover--lean4---nightly-2022-07-11/bin/lean exited with status 139

Is this expected?

[Ilona Prikule]

Actually, the following instance works:

instance : DecidableEq ByteArray
  | a, b => match decEq a.data b.data with
    | isTrue h₁  => isTrue $ congrArg ByteArray.mk h₁
    | isFalse h₂ => isFalse $ fun h => by cases h; exact (h₂ rfl)

:thinking:

[Chris Bailey]

This seems like a buggy interaction with an extern declaration, you might consider filing an issue.

[Mac]

The bug here seems to be that the pattern match ⟨a⟩, ⟨b⟩ is not using the proper extern like a.data.