fastsum
fastsum copied to clipboard
Problem with Apply instance
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 ()
?