Kind refinement in type families with PolyKinds

[Andres Löh]

Hi.

I had said earlier that:

>> 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.
>
> In my experience, such kind arguments are treated like family indices,
> not parameters.

Oh, I see. Thanks. This actually makes sense, but not have guessed it.
So then the behaviour of GHC seems correct. For example, this
typechecks:

> type family Strip (t :: *) :: k
> type instance Strip (Maybe a) = Either
> type instance Strip (Maybe a) = Maybe
> type instance Strip (Maybe a) = Int
>
> test :: (Strip (Maybe Int) Bool Char, Strip (Maybe Int) (), Strip (Maybe Char))
> test = (Left True, Just (), 5)

The problem with

>> x :: Apply (Strip (Maybe a) :: * -> *) (a ': '[]) :=: Maybe a
>> x = Refl

is indeed that without the type annotation, there's no way for GHC to
infer the (implicit) kind parameter, because you're passing it to
something which is also kind polymorphic.

Cheers,
  Andres