Opened 3 years ago

Closed 3 years ago

#12911 closed bug (fixed)

Levity polymorphism check eliminates non-levity-polymorphic data constructor

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T12911
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

When I say

data X where
  MkX :: forall (a :: TYPE r). (a -> a) -> X

I get

    • A representation-polymorphic type is not allowed here:
        Type: a
        Kind: TYPE r
    • In the definition of data constructor ‘MkX’
      In the data type declaration for ‘X’

But that's silly, because the type is not levity-polymorphic!

Change History (4)

comment:1 Changed 3 years ago by josef

I think I hit upon this restriction when trying to implement some of the code from the levity polymorphism paper. The section on levity polymorphic type classes explains how the dictionary from levity polymorphic Num is perfectly safe.

data Num (a :: TYPE r)
 = MkNum {(+) :: a → a → a, abs :: a → a}

But sadly GHC rejects the data type declaration above.

comment:2 Changed 3 years ago by simonpj

Yes, that's over-restrictive; when Richard gets around to implementing the paper (which is very much on his radar I think) it'll be fixed!

comment:3 Changed 3 years ago by Ben Gamari <ben@…>

In 8906e7b7/ghc:

Reshuffle levity polymorphism checks.

Previously, GHC checked for bad levity polymorphism to the left of all
arrows in data constructors. This was wrong, as reported in #12911
(where an example is also shown). The solution is to check each
individual argument for bad levity polymorphism.  Thus the check has
been moved from TcValidity to TcTyClsDecls.

A similar situation exists with pattern synonyms, also fixed here.

This patch also nabs #12819 while I was in town.

Test cases: typecheck/should_compile/T12911, patsyn/should_fail/T12819

Test Plan: ./validate

Reviewers: simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2783

GHC Trac Issues: #12819, #12911

comment:4 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T12911

Thanks for merging, Ben!

Note: See TracTickets for help on using tickets.