Opened 2 years ago
Closed 22 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 2 years ago by
Description: | modified (diff) |
---|
comment:2 Changed 2 years ago by
Keywords: | TypeInType added |
---|
comment:3 Changed 2 years ago by
Milestone: | → 8.0.1 |
---|---|
Priority: | normal → highest |
Type of failure: | None/Unknown → Incorrect warning at compile-time |
comment:4 Changed 2 years ago by
Description: | modified (diff) |
---|
comment:5 Changed 2 years ago by
Owner: | set to goldfire |
---|
comment:7 Changed 2 years 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 2 years 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 2 years 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 23 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 22 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 22 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.