[GHC] #8268: Local annotations ignored in ambiguity check

[GHC]

#8268: Local annotations ignored in ambiguity check
-------------------------------------+-------------------------------------
       Reporter:  maxs               |             Owner:
           Type:  bug                |            Status:  new
       Priority:  highest            |         Milestone:
      Component:  Compiler (Type     |           Version:  7.7
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8268>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler