New type error in GHC 7.1 with TypeFamilies, Rank2Types

[patrick_premont]

The following produces a type error with ghc-7.1.20110126. No error is reported by ghc-7.0.1.

condBug.lhs:48:29:
    Could not deduce (a ~ CondV c a (f a))
    from the context (TBool c, Functor f)
      bound by the type signature for
                 condMap :: (TBool c, Functor f) =>
                            (a -> b) -> Cond c f a -> Cond c f b
      at condBug.lhs:48:3-40
    or from (c ~ TFalse)
      bound by a type expected by the context:
                 c ~ TFalse => CondV c a (f a) -> b
      at condBug.lhs:48:24-40
      `a' is a rigid type variable bound by
          the type signature for
            condMap :: (TBool c, Functor f) =>
                       (a -> b) -> Cond c f a -> Cond c f b
          at condBug.lhs:48:3
    Expected type: CondV c a (f a) -> b
      Actual type: a -> b
    In the first argument of `cond', namely `g'
    In the expression: cond g (fmap g) n

> {-# LANGUAGE TypeFamilies, Rank2Types, ScopedTypeVariables #-}

> import Control.Applicative

> data TFalse
> data TTrue

> data Tagged b a = Tagged {at :: a}
> type At b = forall a. Tagged b a -> a

> class TBool b where onTBool :: (b ~ TFalse => c) -> (b ~ TTrue => c) -> Tagged b c
> instance TBool TFalse where onTBool f _ = Tagged $ f
> instance TBool TTrue where onTBool _ t = Tagged $ t

> type family CondV c f t
> type instance CondV TFalse f t = f
> type instance CondV TTrue f t = t

> newtype Cond c f a = Cond {getCond :: CondV c a (f a)}
> cond :: forall c f a g. (TBool c, Functor g) => (c ~ TFalse => g a) -> (c ~ TTrue => g (f a)) -> g (Cond c f a)
> cond f t = (at :: At c) $ onTBool (fmap Cond f) (fmap Cond t)
> condMap :: (TBool c, Functor f) => (a -> b) -> Cond c f a -> Cond c f b
> condMap g (Cond n) = cond g (fmap g) n
  
> main = undefined

The type error seems inappropriate. Given the defintion of 'CondV', and the 'c ~ TFalse' available form the context, shouldn't the compiler see that 'CondV c a (f a) ~ a' ?

[simonpj]

Yes this is a definite bug; thank you! Should not be hard to fix.

[simonpj]

Excellent! Fixed by

Fri Feb 11 17:40:58 GMT 2011  simonpj@microsoft.com
  * New plan: push unsolved wanteds inwards
  
  This fixes Trac #4935.  See Note [Preparing inert set for implications].
  Lots of comments, but not a lot of code is changed!

    M ./compiler/typecheck/TcCanonical.lhs -17 +19
    M ./compiler/typecheck/TcSimplify.lhs -37 +77

Lots of work by Dimitrios. Thank you!

Simon

[igloo]

Merged