#5277 closed bug (invalid)
Clash between RankNTypes and TypeFamilies
Reported by: | stefan | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.0.3 |
Keywords: | rank-n types, type families, type signatures | Cc: | simonpj@…, dimitris@…, stefan@… |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Difficulty: | |
Test Case: | Blocked By: | ||
Blocking: | Related Tickets: |
Description
[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
Change History (6)
comment:1 Changed 3 years ago by stefan
- Cc stefan@… added
comment:2 Changed 3 years ago by simonpj
- Resolution set to invalid
- Status changed from new to closed
comment:3 Changed 3 years ago by stefan
Thanks for the quick response. It could well be that my brain's just not big enough for this, but I still don't quite get the part where type checking only fails *after* one adds the type signature. My apologies for the inconvenience, but I would really like to understand the issue there.
comment:4 Changed 3 years ago by simonpj
Did you read the FAQ I pointed you at? It (attempts to) explain precisely why the type error occurs only when you add a type signature. Did that not help?
If you want the type signature, you need to help the type checker to resolve the ambiguity, thus:
{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeFamilies #-} module T5277 where 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 :: forall a b. T a -> F a b f = unW . (unT :: T a -> W a b)
Simon
comment:5 Changed 3 years ago by stefan
I have to admit that from reading the FAQ, I probably wouldn't have figured out leaving out the type signature would help here.
I guess the part that I am missing is: why does the compiler pick the "right" equality constraint if the signature is absent.
comment:6 Changed 3 years ago by simonpj
I've elaborated the FAQ a bit; hope that helps.
Yes, this is a gotcha with type families. See: http://haskell.org/haskellwiki/GHC/Indexed_types#Frequently_asked_questions.
I don't know how to improve matters.