I share an observation/"workaround" below.

On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh <[email protected]> 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.

_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to