GitLab

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' ?

Trac metadata

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