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