[GHC] #14185: Non-local bug reporting around levity polymorphism

#14185: Non-local bug reporting around levity polymorphism -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: | Operating System: Unknown/Multiple LevityPolymorphism, | TypeErrorMessages | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- From comment:12:ticket:13105. In HEAD (or, at least, my version, on the `wip/rae` branch), this code {{{#!hs class Unbox (t :: *) (r :: TYPE k) | t -> r, r -> t where unbox :: t -> r box :: r -> t instance Unbox Int Int# where unbox (I# i) = i box i = I# i instance Unbox Char Char# where unbox (C# c) = c box c = C# c instance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where unbox (a,b) = (# unbox a, unbox b #) box (# a, b #) = (box a, box b) testInt :: Int testInt = box (unbox 1) testTup :: (Int, Char) testTup = box (unbox (1, 'a')) }}} fails with {{{ Bug.hs:27:11: error: • Couldn't match a lifted type with an unlifted type When matching types a' :: * Int# :: TYPE 'IntRep • In the expression: box (unbox 1) In an equation for ‘testInt’: testInt = box (unbox 1) | 27 | testInt = box (unbox 1) | ^^^^^^^^^^^^^ Bug.hs:27:16: error: • Couldn't match a lifted type with an unlifted type When matching types a' :: * Int# :: TYPE 'IntRep • In the first argument of ‘box’, namely ‘(unbox 1)’ In the expression: box (unbox 1) In an equation for ‘testInt’: testInt = box (unbox 1) | 27 | testInt = box (unbox 1) | ^^^^^^^ Bug.hs:42:11: error: • Couldn't match a lifted type with an unlifted type When matching types a' :: * Int# :: TYPE 'IntRep • In the expression: box (unbox (1, 'a')) In an equation for ‘testTup’: testTup = box (unbox (1, 'a')) | 42 | testTup = box (unbox (1, 'a')) | ^^^^^^^^^^^^^^^^^^^^ }}} I think it should succeed. Worse, when I comment out the `testTup` definition, the file succeeds... but note that two of the errors above are in `testInt`, which compiles fine on its own. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14185 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14185: Non-local bug reporting around levity polymorphism -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | LevityPolymorphism, | TypeErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by magesh.b): * cc: magesh.b (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14185#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14185: Non-local bug reporting around levity polymorphism -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | LevityPolymorphism, | TypeErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): expect_broken test added in Phab:14185. This captures the program not compiling, but there's also the issue of non-local bug reporting. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14185#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14185: Non-local bug reporting around levity polymorphism -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | LevityPolymorphism, | TypeErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I looked at this in an odd moment. This instance {{{ instance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where unbox (a,b) = (# unbox a, unbox b #) box (# a, b #) = (box a, box b) }}} is quantified over four type variables, ''all of which get kind `Type`''. But in `testTup` we will need to solve {{{ [W] Unbox (Int, Char) (# Int#, Char# ) }}} That is well-kinded but it doesn't match the instance (which has only lifted type variables). What ''actually'' happens is that we try to solve {{{ [W] Unbox (Int,Char) alpha }}} and the fundep says `alpha := (# beta, gamma #)`, but since the fundep comes from the tuple instance, it insists that `beta::*` and `gamma::*`. If you try to make the instance levity-polymorphic: {{{ instance forall a b ar br (a' :: TYPE r1) (b' :: TYPE br). (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where }}} it rightly fails with {{{ T14185a.hs:23:10: error: A levity-polymorphic type is not allowed here: Type: a' Kind: TYPE r1 In the type of binder ‘a’ | 23 | box (# a, b #) = (box a, box b) | ^ }}} This does not explain why we get bogus errors in `testInt` but I claim there is no bug in rejecting `testTup`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14185#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14185: Non-local bug reporting around levity polymorphism
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.3
Resolution: | Keywords:
| LevityPolymorphism,
| TypeErrorMessages
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#14185: Non-local bug reporting around levity polymorphism
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.3
Resolution: | Keywords:
| LevityPolymorphism,
| TypeErrorMessages
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
participants (1)
-
GHC