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).