I think the issue is this. We have
Strip :: forall k. * -> k
When you say
type instance Strip (Maybe a) = Maybe
GHC infers the kind arguments (as with all hidden argument) to get
type instance Strip (*->*) (Maybe a) = Maybe
It would be fine to have another type instance like this
type instance Strip (Maybe a) = Int
which would turn into
type instance Strip * (Maybe a) = Maybe
In all cases, an occurrence of (Strip <kind> <type>) will match one of the
"type instances" only if, well, it matches, including the kind.
Does that answer the question.
I would love someone to write some user guidance notes about this kind of
thing, perhaps as a new sub-page of
http://www.haskell.org/haskellwiki/GHC/Type_system
Simon
From: [email protected]
[mailto:[email protected]] On Behalf Of José Pedro
Magalhães
Sent: 30 October 2012 10:29
To: GHC users
Subject: Kind refinement in type families with PolyKinds
Hi all,
I'm wondering why the following does not work:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
-- Type equality
data a :=: b where Refl :: a :=: a
-- Applying a type to a list of arguments
type family Apply (t :: k) (ts :: [*]) :: *
type instance Apply t '[] = t
type instance Apply (f :: * -> *) (t ': ts) = f t
-- Stripping a type from all its arguments
type family Strip (t :: *) :: k
type instance Strip (Maybe a) = Maybe
-- Reapplying a stripped type is the identity
x :: Apply (Strip (Maybe a)) (a ': '[]) :=: Maybe a
x = Refl
If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I would
expect `* -> *`.
That explains why the `Apply` type family is not reduced further.
I understand that this might be related to GADTs not being allowed to refine
kinds;
the following datatype fails to compile with the error "`D1' cannot be GADT-like
in its *kind* arguments":
data DStrip :: k -> * where
D1 :: DStrip Maybe
But then, shouldn't the type instance for `Strip` above trigger the same error?
Thanks,
Pedro
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
