Opened 20 months ago
Closed 18 months 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 )
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 20 months ago by
Description: | modified (diff) |
---|
comment:2 Changed 20 months ago by
Keywords: | TypeInType added |
---|
comment:3 Changed 20 months ago by
Milestone: | → 8.0.1 |
---|---|
Priority: | normal → highest |
Type of failure: | None/Unknown → Incorrect warning at compile-time |
comment:4 Changed 20 months ago by
Description: | modified (diff) |
---|
comment:5 Changed 20 months ago by
Owner: | set to goldfire |
---|
comment:7 Changed 20 months ago by
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 20 months ago by
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 20 months ago by
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:13 Changed 19 months ago by
Status: | new → merge |
---|---|
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:17 Changed 18 months ago by
Status: | closed → merge |
---|---|
Test Case: | dependent/should_fail/T11473 → dependent/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 18 months ago by
Status: | merge → closed |
---|
Merged to ghc-8.0
as c4f7363465518be3c68a2bacec79d09554d4a886.
This one is straightforward to check for, modulo the deeper issues in #11471.