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
