New type error in GHC 7.1 with TypeFamilies, Rank2Types
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 |