Figuring out the OFunctor hierarchy

Stream: iris-lean

[Markus de Medeiros]

I'm running into some typeclass problems with functors, and I'm looking for the best way to fix it. As it stands, here are the typeclasses we use to represent functors (parameterized by their object map F of type (α : Type _) → (β : Type _) -> [OFE α] → [OFE β] → Type _):

OFunctor, w/ OFE instance for all F α β
OFunctorContractive, extends `OFunctor`
RFunctor, w/ CMRA instance for all F α β
RFunctorContractive, extends `RFunctor`
URFunctor, w/ UCMRA instance for all F α β
URFunctorContractive, extends `URFunctor`

I think the source of my issues comes from the fact that, right now, O/R/UR functors are all separate typeclasses with instances for each other. I'd like to put them together into one extends chain, but sinceCMRA extends OFE and UCMRA extends CMRA (rather than taking OFE/CMRA as a typeclass constraint), I don't know how to resolve the inheritance diamonds for eg. the OFE instance for F α β given some RFunctor F.

What's the usual way to fix this situation? I think if instead of CMRA extending OFE we used typeclasses IsCMRA or IsUCMRA (similar to IsCOFE) then each one of these structures could extend each other, but because the typeclasses contain data I'm not sure if this is a the right move.

[Markus de Medeiros]

(cc @Mario Carneiro, but I'm sure this is a general problem that has been solved before)

[Mario Carneiro]

With this setup, you don't want them to be extends, the data of an RFunctor already include everything you need to build an OFunctor, so you want an instance instead that constructs one from the other

[Markus de Medeiros]

How can I make sure that lean knows (RFunctor.cmra F α β _ _).toOFE and OFunctor.cofe (OFunctor_of_RFunctor F _) α β _ _ are the same OFE? I've hit a few lemmas already where this has come up

[Mario Carneiro]

Because that is the definition of the cofe field of OFunctor_of_RFunctor

[Mario Carneiro]

or it should be

[Mario Carneiro]

(it seems to be true by definition)

[Markus de Medeiros]

Ah okay I didn't know Lean could compare them by unfolding! It's possible that my issues were due to some definitions being sorry'd out. I'll play around with it some more, thanks