Problem with Apply instance

[jwiegley]

The following code demonstrates the problem:

works :: (Apply Eq1 r, Eq v) => Sum r v -> Sum r v -> Bool
works x y = x == y

-- Could not deduce (Apply Eq1 (Const () : r))
fails :: (Apply Eq1 r, Eq v) => Sum r v -> Sum r v -> Bool
fails x y = weaken @_ @_ @(Const ()) x == weaken y

Of course, if I try to provide the missing instance it complains about overlap. So how do I convince it that if Apply Eq1 r, then clearly Apply Eq1 (Const () : r), since there is both Eq1 for Const and Eq for ()?

[patrickt]

Hm. This very much feels like it should work. I have no idea why it doesn't.

[robrix]

The key detail here is that it's complaining that it lacks the Apply instance, not Eq1 or Eq. Lacking the Apply instance (or rather, a constraint bringing it into scope) is the fault of the sad fact that Apply isn't inductive, so knowing either of Apply Eq1 r or Apply Eq1 (Const : r) is insufficient to deduce the other. That's unfortunately precisely why fastsum exists: by not defining properties inductively, we avoid ghc's problems with constraints under these conditions, which grow (IIRC) quadratically.

You can add a constraint for the instance you want, which in this example could replace the instance for r, but it is admittedly a bit gross to expose implementation details like that. I think what I used to do in cases like this was to operate on the un-weakened things wherever possible—weaken last, in other words—or equivalently to operate on the things to be inserted directly as long as possible before making a union. Of course, if I'm not in need of weakening, then there's really no problem.

Let us know how it goes!