BEq fails on structures with dependent types.

[hargoniX]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Deriving a BEq instance like so:

structure BVBit where
  {w : Nat}
  idx : Fin w
  deriving BEq

leads to an error:

type mismatch
  b✝
has type
  Fin b✝¹ : Type
but is expected to have type
  Fin a✝¹ : Type

Presumably because the BEq derive handler does not account for dependent types
in this fashion.

Steps to Reproduce

Run the above code

Expected behavior: we get a BEq instance

Actual behavior: we get a (rather undescriptive) error

Versions

"4.7.0-rc2"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.