Kind refinement in type families with PolyKinds

[Nicolas Frisby]

I share an observation/"workaround" below.

On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh <andres.loeh at gmail.com> wrote:
> 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. If you add a kind annotation, as below,

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

then it type checks. I'm not sure if that scales to your general
objective, though.

Again, this is based on experience, not inspecting GHC or its theory.