Opened 4 years ago

Closed 4 years ago

#8306 closed bug (fixed)

NegativeLiterals allows negative type-level integers

Reported by: monoidal Owned by: thoughtpolice
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: tests/typecheck/should_fail/T8306.hs
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


With NegativeLiterals extension it is possible to write negative type-level "naturals"

type T = -1

while the current solver assumes everything is nonnegative and claims 0 <= -1.

Change History (4)

comment:1 Changed 4 years ago by thoughtpolice

Owner: set to thoughtpolice

Great catch. I have a fix I'm validating as we speak...

comment:2 Changed 4 years ago by Austin Seipp <austin@…>

In 3ee47002dd483e0daa604d37ec45dc33133ff04b/ghc:

Make sure type literals aren't negative (#8306)

As Krzysztof pointed out in #8306, with NegativeLiterals and DataKinds,
definitions such as:

  type T = -1

were accepted, although type literals must be greater than zero.

Signed-off-by: Austin Seipp <>

comment:3 Changed 4 years ago by Austin Seipp <austin@…>

In 32e9017d87792455e15ce1cb232c8c9b4b20cede/testsuite:

Test for #8306

Signed-off-by: Austin Seipp <>

comment:4 Changed 4 years ago by thoughtpolice

Resolution: fixed
Status: newclosed
Test Case: tests/typecheck/should_fail/T8306.hs
Note: See TracTickets for help on using tickets.