Opened 3 years ago

Closed 3 years ago

#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 3 years ago by simonpj

Description: modified (diff)

comment:2 Changed 3 years ago by simonpj

Keywords: TypeInType added

comment:3 Changed 3 years ago by bgamari

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

comment:4 Changed 3 years ago by bgamari

Description: modified (diff)

comment:5 Changed 3 years ago by goldfire

Owner: set to goldfire

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

comment:6 Changed 3 years ago by Ben Gamari <ben@…>

In 89bdac7/ghc:

Add test for #11473

comment:7 Changed 3 years 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 3 years 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 3 years 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 3 years ago by goldfire

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

comment:11 Changed 3 years 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 3 years 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 3 years 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 3 years 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 3 years ago by bgamari

Resolution: fixed
Status: mergeclosed

Merged to ghc-8.0.

comment:16 Changed 3 years 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 3 years 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 3 years ago by bgamari

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