Opened 3 months ago

Closed 3 months ago

Last modified 3 months ago

#14207 closed bug (duplicate)

Levity polymorphic GADT requires extra type signatures

Reported by: andrewthad Owned by:
Priority: low Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeInType, CUSKs Cc:
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:

Description

This does not compile:

data Foo s (a :: TYPE k) where
  FooC :: Foo s Int#

However, this does:

data Foo (s :: Type) (a :: TYPE k) where
  FooC :: Foo s Int#

This also works:

data Foo (s :: j) (a :: TYPE k) where
  FooC :: Foo s Int#

These are all of the language pragmas I have enabled:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

This is pretty easy to work around, but I think it's an incorrect behavior.

Change History (2)

comment:1 Changed 3 months ago by RyanGlScott

Keywords: TypeInType added; LevityPolymorphism removed
Resolution: duplicate
Status: newclosed

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

{-# 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 complete, user-supplied kind signature (or CUSK), because not all type variables are given kinds. See the 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.

comment:2 Changed 3 months ago by goldfire

Keywords: CUSKs added
Note: See TracTickets for help on using tickets.