[GHC] #8907: Un-zonked kind variable passes through type checker

[GHC]

#8907: Un-zonked kind variable passes through type checker
-------------------------------------------+-------------------------------
       Reporter:  goldfire                 |             Owner:
           Type:  bug                      |            Status:  new
       Priority:  normal                   |         Milestone:
      Component:  Compiler (Type checker)  |           Version:  7.8.1-rc2
       Keywords:                           |  Operating System:
   Architecture:  Unknown/Multiple         |  Unknown/Multiple
     Difficulty:  Unknown                  |   Type of failure:
     Blocked By:                           |  None/Unknown
Related Tickets:                           |         Test Case:
                                           |          Blocking:
-------------------------------------------+-------------------------------
 I have this module:

 {{{
 {-# LANGUAGE PolyKinds #-}

 module Bug where

 data Poly a
 }}}

 Now, I say this:
 {{{
 > ghc Bug.hs -fforce-recomp -dppr-debug -fprint-explicit-foralls -ddump-tc
 }}}

 The following is produced:

 {{{
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 TYPE SIGNATURES
 TYPE CONSTRUCTORS
   main:Bug.Poly{tc rn2} :: k{tv ao6} [sk]
                            -> ghc-prim:GHC.Prim.*{(w) tc 34d}
   data Poly{tc} (k::ghc-prim:GHC.Prim.BOX{(w) tc 347}) (a::k)
     No C type associated
     Roles: [nominal, phantom]
     RecFlag NonRecursive, Not promotable
     =
     FamilyInstance: none
 COERCION AXIOMS
 Dependent modules: []
 Dependent packages: [base, ghc-prim, integer-gmp]

 ==================== Typechecker ====================
 }}}

 My concern is the `[sk]` that appears after the kind variable `k_ao6`. It
 would appear that a ''skolem'' type variable passes out of the type-
 checker and is used as the binder for polymorphic kind of `Poly`. Should
 this get zonked somewhere?

 My guess is that there is no way to get this apparent misbehavior to
 trigger some real failure, given that the variable will be substituted
 away before much else happens. Yet, when I saw a skolem appear in a
 similar position after modifying the type-checker, I was sure I had done
 something wrong somewhere.

 So, is this intended or accidental behavior? If accidental, should we be
 scared? If we needn't be scared, I'm happy to close this as wontfix, but a
 Note would probably be helpful somewhere. Apologies if that Note is
 already written and I missed it!

 The same behavior is present in 7.8.1 RC 2 and in HEAD.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8907>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler