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