Kind refinement in type families with PolyKinds
andres.loeh at gmail.com
Tue Oct 30 23:46:27 CET 2012
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
> 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.
More information about the Glasgow-haskell-users