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 ExpType
s 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 |