Cc @robbertkrebbers -- this was needed to make lambda-rust weak work again with Coq master.

What's the point we define as_fractional_fractional as an instance anyway?

For example, for gen_heap we define the Fractional instance as an instance, so it appears as_fractional_fractional gives overlap.

In lambda-rust we have a case where in the context we got AsFractional P Φ 1, and then need a Fractional Φ during the proof.

Question then: is that a bug or a feature?

Do you know where that occurs (file and linenumber?)

Question then: is that a bug or a feature?

No idea.^^ Cc @jjourdan

Do you know where that occurs (file and linenumber?)

It was here.

I don't remember much of the rational of this design. The only thing I remember is that I was not much satisfied by it, so feel free to change it if you find something better.

In particular, I do agree that it feels bad to have two instances for each fractional object (the one derived from as_fractional_fractional, and the one directly defined). We could try to drop as_fractional_fractional as an instance. But then, I think there is actually no point at keeping it at all: AsFractional would then only contain the as_fractional field, and semantically not tied to the fractionality.