cases tactic error when pattern matching despite no missing cases

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following code produces an error. The code should be accepted because there are no missing cases.

inductive T : Bool → Type
| mk1 : (a : Bool) → T a 
| mk2 (f : Bool → Bool) (i : Bool) : T (f i)

def f : (a : Bool) → T a → Nat 
| false, T.mk1 false => 0
| _, _ => 0

Expected behavior:
The definition is accepted without an error

Actual behavior:
The following error message

tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  false = f✝ i✝
at case T.mk2 after processing
  false, _
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

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

4.0.0-nightly-2022-09-04
OS : Ubuntu 22.04.1 LTS

Additional Information

Possibly related to #1562. There seems to be too much case splitting going on.
Any additional information, configuration or data that might be necessary to reproduce the issue.

Start by running the self-contained inductive T and definition f example, then inspect the cases tactic and dependent pattern matcher implicated in the error. Compare the behavior with related issue #1562; done means the definition is accepted without the dependent-elimination error when no cases are missing.