equation compiler failed to prove equation lemma

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

equation compiler failed to prove equation lemma (workaround: disable lemma generation using `set_option eqn_compiler.lemmas false`) in the following code snippet. Found by @rwbarton.

Steps to Reproduce

variables (C D : Type) (c : C) (d : D)
inductive time : Type
| start {} : time
| after : (D → time) → time

-- set_option eqn_compiler.lemmas false
def foo : time D → Σ (γ : Type), γ → C
| time.start := ⟨C, id⟩
| (time.after ts) := ⟨(∀ (i : D), (foo $ ts i).1) × D, λ p, (foo $ ts p.2).2 $ p.1 p.2⟩

Versions

Lean (version 3.4.2, commit cbd2b6686ddb, Release)

Additional Information

• Here is a very similar case that work:

variables (C D : Type) (c : C) (d : D)
inductive time : Type
| start {} : time
| after : (D → time) → time

-- set_option eqn_compiler.lemmas false
def foo : time D → Σ (γ : Type), γ → C
| time.start := ⟨C, id⟩
| (time.after ts) := ⟨(∀ (i : D), (foo $ ts i).1) × D, λ p, (foo $ ts d).2 $ p.1 d⟩

• If you run #print foo.equations._eqn_1 there are two problems: the LHS is not applied to enough arguments (it should be applied to time.start) and the RHS seems to be a metavariable.
• @rwbarton and I find the code in function mk_lemmas in file src\library\equations_compiler\structural_rec.cpp suspicious.

Reproduce the self-contained Lean snippet with equation-compiler lemma generation enabled, then inspect src\library\equations_compiler\structural_rec.cpp, especially mk_lemmas. Run #print foo.equations._eqn_1 and compare the generated left-hand side and right-hand side with the working variant. Done means the equation lemma is generated correctly without requiring the workaround.