simp error: application type mismatch

Stream: lean4

[Vasilii Nesterov]

While working on #28874 I discovored this bug:

import Mathlib.Data.Seq.Defs
import Mathlib.Data.ENat.Basic

def length' (s : Stream'.Seq ℕ) [Decidable s.Terminates] : ENat :=
  if h : s.Terminates then s.length h else none

instance : Decidable (Stream'.Seq.nil : Stream'.Seq ℕ).Terminates :=
  .isTrue (by simp)

-- (kernel) application type mismatch
theorem length'_nil : length' (Stream'.Seq.nil : Stream'.Seq ℕ) = 0 := by
  simp [length']

Is this a known issue? I haven’t investigated it further yet.

[Joachim Breitner]

Another instance of the issues with simp and defeq proofs; this works

theorem length'_nil : length' (Stream'.Seq.nil : Stream'.Seq ℕ) = 0 := by
  simp -implicitDefEqProofs [length']