Don't drop derived quantified constraints
In looking at the way quantified constraints are handled, I noticed that we drop derived quantified constraints (in TcCanonical.solveForAll). I don't see a reason why this is a good idea. And indeed, it causes trouble:
{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses,
KindSignatures, FlexibleInstances, TypeFamilies #-}
module Bug where
import Data.Kind
class (forall (a :: Type -> Type). a b ~ a c) => C b c
instance C a a
class (b ~ c) => D b c
instance D a a
foo :: C a b => a -> b
foo = undefined
bar = foo
food :: D a b => a -> b
food = undefined
bard = food
C and D should really behave identically. Yet bar is rejected while bard is accepted.
Note that the monomorphism restriction forces us to solve, not quantify over, the C and D constraints. This is intentional in this test case.
Normally, the superclasses of a wanted are emitted as derived constraints. In the case of bard, we start with [W] D alpha beta, which doesn't make progress. So we get [D] alpha ~ beta, which unifies the two, and then [W] D alpha alpha is easily dispatched. But in bar the [D] forall a. a alpha ~ a beta is dropped, leading to rejection.
The kind signature in the test case is needed because of #17562 (closed).