#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.... #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