:kind should do kind generalisation

Suppose you load this into GHCi:

{-# LANGUAGE PolyKinds #-}
module Test where

data Proxy (t::k) = Proxy

Now you use :kind to see the kind of Proxy:

ghci> :k Proxy
Proxy :: * -> *

It is true that Proxy has that kind but it has a more polymorphic kind, and that's the one we'd like to see.

The trouble is this. Proxy really does have a polymorphic kind. However, :kind takes a type (not a type constructor) as its argument, so you can say

	:kind (Maybe Int)

for example. So as usual we instantiate Proxy with fresh kind variables -- BUT :kind does not do kind generalisation, so we get a monomorphic instance. (And we default unbound kind variables to *.

Conclusion: :kind should do kind-generalisation.

See also #7586 (closed)

Trac metadata

Trac field	Value
Version	7.6.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture