Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#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

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.

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.

Note: See TracTickets for help on using tickets.