Unification of type variables in constraints

The following code works:

{-# LANGUAGE RankNTypes, ConstraintKinds, KindSignatures, GADTs #-}

import Data.Monoid
import GHC.Prim (Constraint)

data Dict :: Constraint -> * where
  Dict :: a => Dict a

f :: (c (), c String) => (forall a. Dict (c a) -> a) -> ((), String)
f g = (g Dict, g Dict)

test :: ((), String)
test = f g
  where
    g :: Dict (Monoid a) -> a
    g Dict = mempty

But this doesn't:

f :: (c (), c String) => (forall a. c a => a) -> ((), String)
f g = (g, g)

test :: ((), String)
test = f g
  where
    g :: Monoid a => a
    g = mempty

With the errors:

Could not deduce (c0 String, c0 ()) arising from a use of `f'

Could not deduce (Monoid a) arising from a use of `g'

So it seems that type variables in constraints are not unified. At first I thought this might not be easy to fix, but since there's a workaround I guess it should be possible.

Trac metadata

Trac field	Value
Version	7.6.1-rc1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture