#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 Revisions:

Description

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 22 months ago by thoughtpolice

  • Owner set to thoughtpolice

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

comment:2 Changed 22 months 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 <[email protected]>

comment:3 Changed 22 months ago by Austin Seipp <austin@…>

In 32e9017d87792455e15ce1cb232c8c9b4b20cede/testsuite:

Test for #8306

Signed-off-by: Austin Seipp <[email protected]>

comment:4 Changed 22 months ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to tests/typecheck/should_fail/T8306.hs
Note: See TracTickets for help on using tickets.