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

Note 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 Show instance:

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.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture