Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#11465 closed bug (fixed)

Eliminate check_lifted check in TcValidity

Reported by: simonpj Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 7.10.3
Keywords: LevityPolymorphism Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1807
Wiki Page:

Description

In TcValidity, when checking for valid types, we had a long-standing test, embodied in a local function called check_lifted, which checked that a number of places had a lifted type of kind * and not an unlifted one of kind #.

But that test is out-dated now; the kind system does the job.

So this ticket is to remove the check_lifted test. See the discussion in #11120, starting at comment:19.

Change History (12)

comment:1 Changed 4 years ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 4 years ago by bgamari

Differential Rev(s): Phab:D1807

comment:3 Changed 4 years ago by bgamari

Things seem to work about as one would expect with Phab:D1807.

However, this error could use a bit of work,

λ> :set -XTypeInType -XDataKinds -XKindSignatures -XMagicHash 
λ> import GHC.Exts
λ> class Eq Char# where (==) = undefined

<interactive>:3:10: error:
    Unexpected type ‘Char#’
    In the class declaration for ‘Eq’
    A class declaration should have form
      class Eq a where ...

comment:4 Changed 4 years ago by simonpj

Actually I have a patch ready to go... will commit tomorrow

comment:5 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In 07afe44/ghc:

Remove the check_lifted check in TcValidity

This patch fixes Trac #11465.  The check_unlifted check really isn't
necessary, as discussed in Trac #11120 comment:19.

Removing it made just one test-suite change,
in indexed-types/should_fail/T9357, by allowing

   type family F (a :: k1) :: k2
   type instance F Int# = Int

to be accepted.  And indeed that seems entirely reasonable.

comment:6 Changed 4 years ago by simonpj

Resolution: fixed
Status: newclosed

comment:7 Changed 4 years ago by simonpj

Re comment:3, the error message looks fine. I think you meant instance Eq Char#.

comment:8 Changed 4 years ago by bgamari

Oh dear, indeed I did.

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

In 2df42216/ghc:

Add tests for #11465 and the kind invariant

comment:10 Changed 4 years ago by thomie

Milestone: 8.2.1

comment:11 Changed 4 years ago by goldfire

The test case for this was as follows

class BoxIt (a :: TYPE 'Unlifted) where
    type Boxed a :: *
    boxed :: a -> Boxed a

instance BoxIt Char# where
    type Boxed Char# = Char
    boxed x = C# x

main :: IO ()
main = print $ boxed 'c'#

After refactoring the levity stuff as per #11471, this test failed (of course). But as I look at it, it's amazing that it ever worked. The width to the argument of boxed is entirely unknowable. Anyway, it's all much better now. :)

comment:12 Changed 4 years ago by simonpj

Keywords: LevityPolymorphism added

Adding a keyword so we can find it when we write a paper about levity polymorphism!

Note: See TracTickets for help on using tickets.