deriving BEq fails for structures with Prop fields

[girving]

deriving BEq currently fails if a structure has Prop fields, a simple example being

structure S where
  p : True
  deriving BEq

which produces the error message

typeclass instance problem is stuck, it is often due to metavariables
  BEq (?m.302 x✝¹ x✝ a✝ b✝)

From discussion in Zulip and here, this is due to BEq being defined only over Type, not Sort. However, the desire is to keep it this way, and instead fix deriving BEq directly to ignore Prop fields (which is fine by proof irrelevance).

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[kmill]

There's nothing preventing there from S having a BEq instance in principle, even a LawfulBEq. It would be a different story if it were structure S : Prop where ...

The DecidableEq derive handler works here, and from that you get a BEq:

structure S where
  p : True
  deriving DecidableEq

#synth BEq S -- succeeds

This seems to just be a bug in the BEq derive handler that it can't handle a Prop field in the structure. I think this RFC needs a better case for making BEq be parameterized over Sort _ rather than Type _ than just to avoid fixing the BEq deriving handler. (Thanks for filing this issue, though, since it's worth tracking the fact that the BEq derive handler has a bug!)

[girving]

I’m happy to change this to be a bug report on deriving BEq if that’s the preference.

[girving]

I changed the title, but don’t have permission to change the label.

[arademaker]

I got a similar errror in

structure Result where
 derivation : String
 mrs : MRS
deriving Repr

the error is

typeclass instance problem is stuck, it is often due to metavariables
  Repr (?m.3386 x✝ prec✝)

where MRS is defined as

structure MRS where
  top : Var
  index : Var
  preds : List EP
  hcons : List Constraint
  icons : List Constraint

instance : ToFormat MRS where
 format
 | {top := t, index := i, preds := ps, icons := [], hcons := hs} =>
   f!"[ LTOP: {t}
        INDEX: {i}
        RELS: < {Format.joinSep (ps.map fun a => format a) " "} >
        HCONS: < {Format.joinSep (hs.map fun a => format a) " "} > ]"
 | {top := t, index := i, preds := ps, icons := is, hcons := hs} =>
   f!"[ LTOP: {t}
        INDEX: {i}
        RELS: < {Format.joinSep (ps.map fun a => format a) " "} >
        HCONS: < {Format.joinSep (hs.map fun a => format a) " "} >
        ICONS: < {Format.joinSep (is.map fun a => format a) " "} > ]"

instance : Repr MRS where
 reprPrec m _ := f!"{m}"

[kim-em]

@girving, could you update the issue description? I think no need to keep the old version, it's just noise now. If you prefer to just open a new issue that might even be easier.

[arademaker]

From my side. Not sure how I solved, but the error disappeared after moving to Lean last release. Maybe my step by step procedure to update Lean and std were not ideally and some of the lake clean and lake build solve the issue.

[girving]

@semorrison I updated the issue description.

[girving]

Woohoo, thank you!