[GHC] #11473: Levity polymorphism checks are inadequate
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Keywords: | Operating System: Unknown/Multiple LevityPolymorphism | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism 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 changed by simonpj: @@ -40,0 +40,2 @@ + + See also #11471 New description: 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 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: LevityPolymorphism => LevityPolymorphism, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * priority: normal => highest * failure: None/Unknown => Incorrect warning at compile-time * milestone: => 8.0.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: @@ -2,1 +2,1 @@ - {{{ + {{{#!hs New description: Ben found {{{#!hs {-# 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 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire Comment: This one is straightforward to check for, modulo the deeper issues in #11471. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: new
Priority: highest | Milestone: 8.0.1
Component: Compiler | Version: 7.10.3
Resolution: | Keywords:
| LevityPolymorphism, TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Thanks for another example. Will get to this soon (next week?). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: new
Priority: highest | Milestone: 8.0.1
Component: Compiler | Version: 7.10.3
Resolution: | Keywords:
| LevityPolymorphism, TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11473: Levity polymorphism checks are inadequate
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: new
Priority: highest | Milestone: 8.0.1
Component: Compiler | Version: 7.10.3
Resolution: | Keywords:
| LevityPolymorphism, TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | dependent/should_fail/T11473 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => dependent/should_fail/T11473 Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: merge
Priority: highest | Milestone: 8.0.1
Component: Compiler | Version: 7.10.3
Resolution: | Keywords:
| LevityPolymorphism, TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: Incorrect | Test Case:
warning at compile-time | dependent/should_fail/T11473
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | dependent/should_fail/T11473 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.0`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: closed
Priority: highest | Milestone: 8.0.1
Component: Compiler | Version: 7.10.3
Resolution: fixed | Keywords:
| LevityPolymorphism, TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: Incorrect | Test Case:
warning at compile-time | dependent/should_fail/T11473
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | dependent/should_fail/T11473, | typecheck/should_fail/BadUnboxedTuple Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: closed => merge * testcase: dependent/should_fail/T11473 => dependent/should_fail/T11473, typecheck/should_fail/BadUnboxedTuple Comment: Found a corner case that wasn't handled in previous commit. Please merge for 8.0. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | dependent/should_fail/T11473, | typecheck/should_fail/BadUnboxedTuple Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed Comment: Merged to `ghc-8.0` as c4f7363465518be3c68a2bacec79d09554d4a886. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC