Un-zonked kind variable passes through type checker

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.

Trac metadata

Trac field	Value
Version	7.8.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

changed weight to 3

Richard, can this ticket be closed?

Output with ghc-7.10.3 is:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
TYPE SIGNATURES
TYPE CONSTRUCTORS
  type role Poly{tc} phantom
  data Poly{tc} (a :: k)
COERCION AXIOMS
Dependent modules: []
Dependent packages: [base-4.8.2.0, ghc-prim-0.4.0.0,
                     integer-gmp-1.0.0.0]
Bug.hs:1:1:
    
    ==================== Typechecker ====================

Trac metadata

Trac field	Value
Priority	normal → low

closed

Yes, this would appear to be fixed. Thanks for noticing! Not worth a regression test, as I don't think the old behavior actually caused any problems.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Plow label