Clash between RankNTypes and TypeFamilies
[Note: a more specific summary line is in order for this ticket.]
Consider the following program:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
type family F a b :: *
data W a b = W {unW :: F a b}
data T a = T {unT :: forall b. W a b}
-- f :: T a -> F a b
f = unW . unT
It type checks fine and querying the inferred type for f interactively yields the expected type. However, adding a type signature for f,
f :: T a -> F a b
f = unW . unT
results in a typing error:
Couldn't match type `F a b0' with `F a b'
NB: `F' is a type function, and may not be injective
Expected type: W a b0 -> F a b
Actual type: W a b0 -> F a b0
In the first argument of `(.)', namely `unW'
In the expression: unW . unT
Trac metadata
Trac field | Value |
---|---|
Version | 7.0.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | dimitris@microsoft.com, simonpj@microsoft.com |
Operating system | |
Architecture |