Kind refinement in type families with PolyKinds

[Andres Löh]

Hi.

This one looks strange to me:

>> -- Stripping a type from all its arguments
>> type family Strip (t :: *) :: k

I'd be tempted to read this as saying that

> Strip :: forall k. * -> k

So the result of Strip would actually have to be kind-polymorphic. I'm
surprised that

>> type instance Strip (Maybe a) = Maybe

then doesn't trigger an error.

> If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I
> would expect `* -> *`.

This seems to indicate that the correct reading for Strip might be

> Strip :: exists k. * -> k

which is counter-intuitive to me, because it's different from anything
else in Haskell. Then the result of Strip would indeed by an unknown
kind "k", and it would feel wrong to be able to reveal what concrete
kind it is later.

I think kind refinement on type families only makes sense if it is
introduced by arguments of the kind family.

> 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

This is somewhat different. Here, the kind of DStrip is clearly

DStrip :: forall k . k -> *

So here, actual refinement of k would make sense to me, although I
could understand if it isn't currently implemented.

Cheers,
  Andres