Deriving DecidableEq fails in the presence of an import

Stream: lean4

[Graham Leach-Krouse]

Noticing some strange behavior around DecidableEq. The following code doesn't work:

import Mathlib.Logic.Denumerable

inductive Form : Type
  | atom : Nat → Form
  | and  : Form → Form → Form
  | impl : Form → Form → Form
  deriving DecidableEq

inductive BTheorem : Form → Type
  | taut {p} : BTheorem (Form.impl p p)
  | andE₁ {p q} : BTheorem (Form.impl (Form.and p q) p)
  | andE₂ {p q} : BTheorem (Form.impl (Form.and p q) q)
  deriving DecidableEq

[Graham Leach-Krouse]

The diagnostic on the last line is:

▶ 13:12-13:23: error:
tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  Form.and p✝ q✝ = q✝ after processing
  _, (@BTheorem.taut _), _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

[Graham Leach-Krouse]

The problem seems to resolve if I remove either the import, the second andE constructor (but not the first!) or the taut constructor.

[Graham Leach-Krouse]

Any ideas?

[Graham Leach-Krouse]

This is on leanprover/lean4:nightly-2023-02-04

[Graham Leach-Krouse]

Sorry, maybe I should be more specific. What I'm wondering is:

1. Is this a bug, or am I doing something incorrectly?
2. If it is a bug, should I open an issue somewhere, and if so, where?