Skip to content

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information