Instance diamond with proofs and pi types

Stream: general

[Robin Arnez]

I've got myself in a bit of weird situation with the following instance diamond:

class MyClass (α : Sort u) where
  Rel : Nat → α → Prop

axiom MyRel (a b c : Nat) : Prop
axiom myRel_zero : MyRel 0 x 0

instance proofInst {p : Prop} : MyClass p where
  Rel n _ := n = 0

instance piInst {α : Sort u} {β : α → Sort v} [MyClass α] [∀ a, MyClass (β a)] :
    MyClass ((a : α) → β a) where
  Rel n f := ∀ m a, MyClass.Rel m a → ∃ k, MyRel n m k ∧ MyClass.Rel k (f a)

example (p : Prop) (h : p) : MyClass.Rel 0 h := rfl
example {α : Sort u} [MyClass α] (p : α → Prop) (h : ∀ a, p a) : MyClass.Rel 0 h :=
  fun _ _ _ => ⟨0, myRel_zero, rfl⟩

-- diamond alert!
example {α : Sort u} [MyClass α] (p : α → Prop) :
    (proofInst : MyClass (∀ a, p a)) = piInst := rfl -- fails

Now I wonder whether I can resolve this diamond (failure of normalization comes to mind but maybe there is a better way?). Specifically, I'm looking for some way to define both instances such that MyClass.Rel 0 h holds for all proofs and the instances are definitionally equivalent and piInst is propositionally equivalent to how I have it here for v >= 1. However, it is totally fine for me to have the definitions of proofInst and piInst changed in a significant way for v = 0 as long as MyClass.Rel 0 h holds.

[Edward van de Meent]

firstly, this seems like a strange construction so let me #xy...
Secondly, have you considered changing piInst to {β : α → Type v}?

[Robin Arnez]

No, I want to have piInst to be as general as possible, so it can apply to situations whether you have Sort v

[Robin Arnez]

If you're curious, this is for computability stuff and MyClass.Rel n x is basically a generalized form of n = Encodable.encode x

[Edward van de Meent]

aha...
in that case, i think that having proofInst around is bad from lean's POV. in particular, talking about encoding things in Sort u in a universal way (as proofInst does) is always going to clash with an instance for pi types.
Instead, i think it will be better to either:

• not have this kind of instance at all for Prop values, because any time you use propext you can get non-defeq diamonds showing up
• if you must, only have instances for "primitive" Props e.g. True, False, Exists, etc...

[Robin Arnez]

Yeah that's also a solution I thought about; I definitely want to have an instance for Props (at least some that we know are safe I guess) for example to get MyClass ((n : Nat) → n < 7 → Nat) and it would certainly be nice to automatically have this for all Props but it seems like this is always going to cause problems... oh well I guess I'll see how well it works to register for specific Props.