
I share an observation/"workaround" below.
On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh
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.