#11473 closed bug (fixed)

Levity polymorphism checks are inadequate

Reported by: simonpj Owned by: goldfire
Priority: highest Milestone: 8.0.1
Component: Compiler Version: 7.10.3
Keywords: LevityPolymorphism, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case: dependent/should_fail/T11473, typecheck/should_fail/BadUnboxedTuple
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

Ben found

{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}

import GHC.Exts
import GHC.Types

type family Boxed (a :: k) :: *
type instance Boxed Char# = Char
type instance Boxed Char  = Char

class BoxIt (a :: TYPE lev) where
    boxed :: a -> Boxed a

instance BoxIt Char# where boxed x = C# x
instance BoxIt Char  where boxed = id

hello :: forall (lev :: Levity). forall (a :: TYPE lev). BoxIt a => a -> Boxed a
hello x = boxed x
{-# NOINLINE hello #-}

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

This is plainly wrong because we have a polymorphic function boxed that is being passed both boxed and unboxed arguments.

You do get a Lint error with -dcore-lint.

But the original problem is with the type signature for boxed. We should never have a levity-polymorphic type to the left of an arrow. To the right yes, but to the left no. I suppose we could check that in TcValidity.

See also #11471

Change History (18)

comment:1 Changed 22 months ago by simonpj

Description: modified (diff)

comment:2 Changed 22 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 22 months ago by bgamari

Milestone: 8.0.1
Priority: normalhighest
Type of failure: None/UnknownIncorrect warning at compile-time

comment:4 Changed 22 months ago by bgamari

Description: modified (diff)

comment:5 Changed 22 months ago by goldfire

Owner: set to goldfire

This one is straightforward to check for, modulo the deeper issues in #11471.

comment:6 Changed 22 months ago by Ben Gamari <ben@…>

In 89bdac7/ghc:

Add test for #11473

comment:7 Changed 22 months ago by rwbarton

This slight variation of Ben's program does produce a garbage result. I just added an extra function call to hello (and turned on ScopedTypeVariables).

{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes, ScopedTypeVariables #-}

import GHC.Exts
import GHC.Types

type family Boxed (a :: k) :: *
type instance Boxed Char# = Char
type instance Boxed Char  = Char

class BoxIt (a :: TYPE lev) where
    boxed :: a -> Boxed a

instance BoxIt Char# where boxed x = C# x
instance BoxIt Char  where boxed = id

hello :: forall (lev :: Levity) (a :: TYPE lev). BoxIt a => a -> Boxed a
hello x = boxed (myid x)
  where myid :: a -> a
        myid y = y
        {-# NOINLINE myid #-}
{-# NOINLINE hello #-}

main :: IO ()
main = do
    print $ boxed 'c'#
    print $ boxed 'c'
    print $ hello 'c'
    print $ hello 'c'#    -- this one prints '\8589966336'

(Interesting note, hello :: forall foo. forall bar. t does not bring bar into scope in the definition of hello. I guess that makes sense.)

comment:8 Changed 22 months ago by rwbarton

It seems to me the most logical place to put these levity polymorphism checks is in the typing rules for abstraction and application. After all \(a :: t) -> ... is really different beasts at runtime depending on whether t :: * = TYPE L, or t :: TYPE UW32, or t :: TYPE UW64 etc. We should insist that the rep (the r such that t :: TYPE r) of t be known when type-checking the lambda, and resolve the overloading to \_L, or \_UW32, or \_UW64. In short, treat \ as ad-hoc polymorphic.

Similar comments apply to application. f x is really an overloaded f $_r x, where the typing rule for $_r is

s :: RuntimeRep   a :: TYPE r   b :: TYPE s   f :: a -> b   x :: a
------------------------------------------------------------------
                             f $_r x :: b

And this makes sense because later to actually compile an application, we will absolutely need to know the rep of the type of x.

Then I don't think we need any special rules about the kind of ->, which can become rep-polymorphic in both arguments.

comment:9 Changed 22 months ago by rwbarton

What happens with let-bound variables of polymorphic representation? Surely we can't allow this:

{-# LANGUAGE TypeInType, ScopedTypeVariables #-}

import GHC.Types

app :: forall (l :: Levity) (a :: *) (b :: TYPE l). (a -> b) -> a -> b
app f x = let y :: b
              y = undefined
          in f x

comment:10 Changed 21 months ago by goldfire

Thanks for another example. Will get to this soon (next week?).

comment:11 Changed 20 months ago by Richard Eisenberg <eir@…>

In aade1112/ghc:

Fix #11473.

I've added a check in the zonker for representation polymorphism.
I don't like having this be in the zonker, but I don't know where
else to put it. It can't go in TcValidity, because a clever enough
user could convince the solver to do bogus representation polymorphism
even though there's nothing obviously wrong in what they wrote.
Note that TcValidity doesn't run over *expressions*, which is where
this problem arises.

In any case, the check is simple and it works.

test case: dependent/should_fail/T11473

comment:12 Changed 20 months ago by Richard Eisenberg <eir@…>

In 5d98b8bf/ghc:

Clean up some pretty-printing in errors.

It turns out that there were some pretty egregious mistakes
in the code that suggested -fprint-explicit-kinds, which are
fixed. This commit also reorders a bunch of error messages,
which I think is an improvement.

This also adds the test case for #11471, which is what
triggered the cleanup in TcErrors. Now that #11473 is done,
there is nothing more outstanding for #11471.

test case: dependent/should_fail/T11471

comment:13 Changed 20 months ago by goldfire

Status: newmerge
Test Case: dependent/should_fail/T11473

All set now. Perhaps in the future we can find a better home for this check than in the zonker. But the check is very simple, and we know it will always get applied.

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

In c0f628dc/ghc:

Revert "Add test for #11473"

This reverts commit 89bdac7635e6ed08927d760aa885d3e7ef3edb81 as
this test is duplicated with dependent/should_fail/T11473, added by
aade111248dce0834ed83dc4f18c234967b3202.

comment:15 Changed 20 months ago by bgamari

Resolution: fixed
Status: mergeclosed

Merged to ghc-8.0.

comment:16 Changed 20 months ago by Richard Eisenberg <eir@…>

In 12a76be/ghc:

Check for rep poly on wildcard binders.

I had just missed this case when adding my test.
This is relevant to ticket #11473.

Also adds lots of comments.

comment:17 Changed 20 months ago by goldfire

Status: closedmerge
Test Case: dependent/should_fail/T11473dependent/should_fail/T11473, typecheck/should_fail/BadUnboxedTuple

Found a corner case that wasn't handled in previous commit. Please merge for 8.0.

Thanks!

comment:18 Changed 20 months ago by bgamari

Status: mergeclosed
Note: See TracTickets for help on using tickets.