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 _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
