Hi. 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 typechecks:
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. Cheers, Andres