#4935: New type error in GHC 7.1 with TypeFamilies, Rank2Types
--------------------------------+-------------------------------------------
Reporter: patrick_premont | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.1 | Keywords:
Testcase: | Blockedby:
Os: Windows | Blocking:
Architecture: x86 | Failure: None/Unknown
--------------------------------+-------------------------------------------
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' ?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4935>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
