#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11519 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler