GADT Constraint breaks type inference

The following code compiles:

{-# LANGUAGE TypeFamilies,
             MultiParamTypeClasses, GADTs #-}

module Foo () where

class (Num src, Num tgt) => Bar src tgt where
  bar :: (tgt, src)

type family Type a

data CT :: (* -> * -> *) where
  CT :: --(Type rp ~ Type rq) =>
        rp -> rq -> CT rp rq

foo :: (Bar rp rq) => CT rp rq -> CT rp rq
foo = let (b', a') = bar
      in \(CT a b) -> CT (a * a') (b * b')

But when I add the [totally irrelevant] constraint to the GADT, foo no longer compiles:

Foo.hs:16:22:
    Could not deduce (Bar t1 t0) arising from a use of ‘bar’
    from the context (Bar rp rq)
      bound by the type signature for
                 foo :: Bar rp rq => CT rp rq -> CT rp rq
      at testsuite/Foo.hs:15:8-42
    The type variables ‘t0’, ‘t1’ are ambiguous
    Relevant bindings include
      b' :: t0 (bound at Foo.hs:16:12)
      a' :: t1 (bound at Foo.hs:16:16)
    In the expression: bar
    In a pattern binding: (b', a') = bar
    In the expression:
      let (b', a') = bar in \ (CT a b) -> CT (a * a') (b * b')

Foo.hs:17:31:
    Couldn't match expected type ‘rp’ with actual type ‘t1’
      ‘t1’ is untouchable
        inside the constraints (Type rp ~ Type rq)
        bound by a pattern with constructor
                   CT :: forall rp rq. Type rp ~ Type rq => rp -> rq -> CT rp rq,
                 in a lambda abstraction
        at Foo.hs:17:12-17
      ‘rp’ is a rigid type variable bound by
           the type signature for foo :: Bar rp rq => CT rp rq -> CT rp rq
           at testsuite/Foo.hs:15:8
    Relevant bindings include
      a :: rp (bound at Foo.hs:17:15)
      a' :: t1 (bound at Foo.hs:16:16)
      foo :: CT rp rq -> CT rp rq (bound at Foo.hs:16:1)
    In the second argument of ‘(*)’, namely ‘a'’
    In the first argument of ‘CT’, namely ‘(a * a')’

Foo.hs:17:40:
    Couldn't match expected type ‘rq’ with actual type ‘t0’
      ‘t0’ is untouchable
        inside the constraints (Type rp ~ Type rq)
        bound by a pattern with constructor
                   CT :: forall rp rq. Type rp ~ Type rq => rp -> rq -> CT rp rq,
                 in a lambda abstraction
        at Foo.hs:17:12-17
      ‘rq’ is a rigid type variable bound by
           the type signature for foo :: Bar rp rq => CT rp rq -> CT rp rq
           at Foo.hs:15:8
    Relevant bindings include
      b :: rq (bound at Foo.hs:17:17)
      b' :: t0 (bound at Foo.hs:16:12)
      foo :: CT rp rq -> CT rp rq (bound at Foo.hs:16:1)
    In the second argument of ‘(*)’, namely ‘b'’
    In the second argument of ‘CT’, namely ‘(b * b')’

The errors can be fixed using -XScopedTypeVariables and changing foo to:

foo :: forall rp rq . (Bar rp rq) => CT rp rq -> CT rp rq
foo = let (b' :: rq, a' :: rp) = bar
      in \(CT a b) -> CT (a * a') (b * b')

Why should I need an explicit type on bar, when the type can be inferred from its use in foo (as it was before the GADT constraint was added)? Is that expected behavior for GADTs?

Trac metadata

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