Local annotations ignored in ambiguity check

The following program type checks correctly in GHC 7.6.3 but fails in 7.7 (2013 09 04).

{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, GADTs, OverlappingInstances, ScopedTypeVariables, TypeFamilies, TypeOperators #-}

module Test where

newtype Exp t = Exp (Exp t)

type family EltRepr a :: *
type instance EltRepr () = ()

data TupleType a where
  UnitTuple   ::                               TupleType ()

class (Show a)
      => Elt a where
  eltType  :: {-dummy-} a -> TupleType (EltRepr a)

instance Elt () where
  eltType _ = UnitTuple

instance (Lift Exp a, Lift Exp b, Elt (Plain a), Elt (Plain b)) => Lift Exp (a, b) where
  type Plain (a, b) = (Plain a, Plain b)
  lift (x, y) = tup2 (lift x, lift y)

tup2 :: (Elt a, Elt b) => (Exp a, Exp b) -> Exp (a, b)
tup2 (x1, x2) = undefined -- Exp $ Tuple (NilTup `SnocTup` x1 `SnocTup` x2)

class Lift c e where
  type Plain e
  lift :: e -> c (Plain e)

class Lift c e => Unlift c e where
  unlift :: c (Plain e) -> e

fst :: forall f a b. Unlift f (f a, f b) => f (Plain (f a), Plain (f b)) -> f a
fst e = let (x, _:: f b) = unlift e in x

The error

Test.hs:34:8:
    Could not deduce (Plain (f b0) ~ Plain (f b))
    from the context (Unlift f (f a, f b))
      bound by the type signature for
                 Test.fst :: Unlift f (f a, f b) =>
                             f (Plain (f a), Plain (f b)) -> f a
      at Test.hs:34:8-79
    NB: ‛Plain’ is a type function, and may not be injective
    The type variable ‛b0’ is ambiguous
    Expected type: f (Plain (f a), Plain (f b)) -> f a
      Actual type: f (Plain (f a), Plain (f b0)) -> f a
    In the ambiguity check for:
      forall (f :: * -> *) a b.
      Unlift f (f a, f b) =>
      f (Plain (f a), Plain (f b)) -> f a
    In the type signature for ‛Test.fst’:
      Test.fst :: forall f a b. Unlift f (f a, f b) =>
                  f (Plain (f a), Plain (f b)) -> f a

GHC 7.7 reports:

 Actual type: f (Plain (f a), Plain (f b0)) -> f a

which is incorrect due to the type annotation.

Trac metadata

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture