Kind refinement in type families with PolyKinds

Nicolas Frisby nicolas.frisby at gmail.com
Tue Oct 30 19:19:06 CET 2012


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.



More information about the Glasgow-haskell-users mailing list