[GHC] #11519: Inferring non-tau kinds

[GHC]

#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