[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 <ben@…>): In [changeset:"89bdac7635e6ed08927d760aa885d3e7ef3edb81/ghc" 89bdac7/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="89bdac7635e6ed08927d760aa885d3e7ef3edb81" Add test for #11473 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11473#comment:6> 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): 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 <eir@…>): In [changeset:"5d98b8bf249fab9bb0be6c5d4e8ddd4578994abb/ghc" 5d98b8bf/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5d98b8bf249fab9bb0be6c5d4e8ddd4578994abb" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11473#comment:12> 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 <eir@…>): In [changeset:"aade111248dce0834ed83dc4f18c234967b32024/ghc" aade1112/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="aade111248dce0834ed83dc4f18c234967b32024" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11473#comment:11> 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: | -------------------------------------+------------------------------------- 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 <ben@…>): In [changeset:"c0f628dc6f604028acc665e5b37019750a30c852/ghc" c0f628dc/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="c0f628dc6f604028acc665e5b37019750a30c852" Revert "Add test for #11473" This reverts commit 89bdac7635e6ed08927d760aa885d3e7ef3edb81 as this test is duplicated with dependent/should_fail/T11473, added by aade111248dce0834ed83dc4f18c234967b3202. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11473#comment:14> 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: | -------------------------------------+------------------------------------- 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 <eir@…>): In [changeset:"12a76bebe0864cdf1c9088ed16175d7b34369e24/ghc" 12a76be/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="12a76bebe0864cdf1c9088ed16175d7b34369e24" 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. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11473#comment:16> 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: 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