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 magesh.b

Cc: magesh.b added

comment:2 Changed 14 months ago by monoidal

expect_broken test added in Phab:4981.

This captures the program not compiling, but there's also the issue of non-local bug reporting.

Last edited 14 months ago by monoidal (previous) (diff)

comment:3 Changed 14 months ago 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.

comment:4 Changed 14 months ago by Simon Peyton Jones <simonpj@…>

In 6c19112/ghc:

Build more implications

The "non-local error" problem in Trac #14185 was due to the
interaction of constraints from different function definitions.

This patch makes a start towards fixing it.  It adds
TcUnify.alwaysBuildImplication to unconditionally build an
implication in some cases, to keep the constraints from different
functions separate.

See the new Note [When to build an implication] in TcUnify.

But a lot of error messages change, so for now I have set
   alwaysBuildImplication = False

Result: no operational change at all.  I'll get back to it!

comment:5 Changed 14 months ago by Ben Gamari <ben@…>

In 3581212/ghc:

Add an expect_broken test for #14185

Test Plan: validate

Reviewers: goldfire, bgamari, alpmestan

Reviewed By: alpmestan

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14185

Differential Revision: https://phabricator.haskell.org/D4981
Note: See TracTickets for help on using tickets.