Opened 2 years ago
Last modified 14 months ago
#14185 new bug
Non-local bug reporting around levity polymorphism
Reported by: | goldfire | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.3 |
Keywords: | LevityPolymorphism, TypeErrorMessages | Cc: | magesh.b |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
From comment:12:ticket:13105.
In HEAD (or, at least, my version, on the wip/rae
branch), this code
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.
Change History (5)
comment:1 Changed 2 years ago by
Cc: | magesh.b added |
---|
comment:3 Changed 14 months ago by
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
.
expect_broken test added in Phab:4981.
This captures the program not compiling, but there's also the issue of non-local bug reporting.