Inferring non-tau kinds
While up to my usual type-level shenanigans, I found that I want this definition:
data TypeRep (a :: k) -- abstract data TypeRepX :: (forall k. k -> Constraint) -> Type where TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k). c a => TypeRep a -> TypeRepX c
TypeRepX's higher-rank kind. The idea is that I want to optionally constrain
TypeRepX's payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use
TypeRepX ConstTrue, where
class ConstTrue (a :: k) instance ConstTrue a
This actually works just fine, and I've been using the above definition to good effect.
But then I wanted a
instance Show (TypeRep a) -- elsewhere instance Show (TypeRepX c) where show (TypeRepX tr) = show t
Looks sensible. But GHC complains. This is because it tries to infer
c's kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because
c's kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate
c with the correct kind, unification still fails. This is because that
c is a usage of
c, not a binding of
c. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse.
I'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for
c is perfectly safe, because the kind is known from the use of
TypeRepX. This would allow me to drop the kind annotation in the definition of
TypeRepX, which looks redundant to me. But I'm not fully sure about this assumption.
At the least, we could introduce a spot for explicit binding of type variables in instance declarations.
I think, actually, I just figured it out. Use
ExpTypes when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.