[GHC] #14207: Levity polymorphic GADT requires extra type signatures

[GHC]

#14207: Levity polymorphic GADT requires extra type signatures
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  low               |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:  duplicate         |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13365            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * keywords:  LevityPolymorphism => TypeInType
 * status:  new => closed
 * resolution:   => duplicate
 * related:   => #13365


Comment:

 This is expected behavior, and moreover, this has nothing to do with
 levity polymorphism. A simpler example of what's going on is this:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeInType #-}
 module Foo where

 data Foo s (a :: k) where
   FooC :: Foo s Int
 }}}
 {{{
 Foo.hs:6:17: error:
     • Expected kind ‘k’, but ‘Int’ has kind ‘*’
     • In the second argument of ‘Foo’, namely ‘Int’
       In the type ‘Foo s Int’
       In the definition of data constructor ‘FooC’
   |
 6 |   FooC :: Foo s Int
   |                 ^^^
 }}}

 As you noted, this fails to compile, but adding a kind signature to `s`
 makes it compile. What is happening is that the original definition of
 `Foo` lacks a **c**omplete, **u**ser-**s**upplied **k**ind signature (or
 CUSK), because not all type variables are given kinds. See the
 [https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.html?highlight=cusk
 #complete-user-supplied-kind-signatures-and-polymorphic-recursion users'
 guide] for more information on what constitutes a CUSK.

 When `TypeInType` is enabled, GHC performs kind inference for a data type
 differently depending on whether is has a CUSK or not. When it doesn't
 have a CUSK, the kind of `a` becomes more rigid than it would otherwise
 be, preventing `(a :: k)` from unifying with `(Int :: *)`, which explains
 the error message. The error message with your levity polymorphic example
 is similar (although the presence of `TYPE` causes an overzealous
 "Expected a lifted type" error, see #14155).

 What would be nice is if GHC could warn you about the lack of a CUSK in
 such scenarios. That is the goal of #13365, so I'll close this ticket as a
 duplicate of that one.

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