[GHC] #12973: No levity-polymorphic arguments

#12973: No levity-polymorphic arguments -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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: -------------------------------------+------------------------------------- As discussed in our [http://cs.brynmawr.edu/~rae/papers/2017/levity/levity.pdf draft paper] on levity polymorphism, you cannot have a levity-polymorphic argument. Here is an example: {{{#!hs {-# LANGUAGE RebindableSyntax, TypeInType, ExplicitForAll #-} module Bug where import qualified Prelude as P import GHC.Exts class Num (a :: TYPE r) where (+) :: a -> a -> a fromInteger :: P.Integer -> a foo :: forall (a :: TYPE r). Num a => a foo = 3 + 4 }}} HEAD panics in `kindPrimRep`, but the code should be rejected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12973 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12973: No levity-polymorphic arguments -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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: | -------------------------------------+------------------------------------- Comment (by goldfire): This is subtler than we realized in the paper. Consider {{{#!hs data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a bar :: forall (r :: RuntimeRep) (a :: TYPE r). a :~~: Int -> a bar HRefl = 3 + 4 }}} Well? What do we think? Is that good or bad? It depends on how GHC inserts the coercions. :( In HEAD, this panics as written. But if I make the RHS to be `3 + 4 :: Int`, then it compiles. The question is whether GHC chooses to desugar the RHS to {{{ (+) @a (fromInteger @a 3) (fromInteger @a 4) }}} or to {{{ (+) @Int (fromInteger @Int 3) (fromInteger @Int 4) |> co }}} where `co` can cast from `Int` to `a`. The former is much more obvious in this case, but there's nothing actually wrong about the latter. And I'm sure some scenarios won't be as easy to guess what might happen under the hood. I think this question is more fundamental than just predictable type inference. For example, is this Core well typed: {{{f (x |> co)}}} What if the left-hand type of `co` is levity polymorphic? What if the right-hand type is? And what happens in the code generator when it sees such a construct? Presumably, it just ignores casts. This tells us that we care about `co`'s left-hand type. But now what if we substitute `x :-> y |> co'`. If `y` looks levity-polymorphic while `x` does not, this substitution has brought us from a well typed program to an ill typed one. Disaster! I thus go to sleep troubled. Hopefully wisdom strikes in the night, either in my sleep or on this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12973#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12973: No levity-polymorphic arguments -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Something struck in the night. Time will tell if it was wisdom. The idea is this: the representation choice of an argument is properly a property of the ''function'', not the ''argument''. So, in Core at least, when examining `f (x |> co)`, we care about the argument type of `f`, not that of `x` or `co`. (Of course, if it's well typed, the right-hand type of `co` matches the argument type of `f`.) So the Core levity polymorphism check does ''not'' look under coercions. However, this means that the code generator must also not look under coercions when compiling arguments (that is, when converting to ANF). Does this already happen? Perhaps, as I look at !CorePrep. But then is this respected further on down the compilation chain? (That is, how are coerced arguments handled in STG and beyond?) I do see that we simply drop casts in !CoreToStg; no surprise there. And I suppose that, at this point, we're already in ANF form, so any arguments are bound to ids that have the right type.... so maybe it's all OK. I'd love confirmation. Even if this all works out at the Core level, we still have a type inference challenge. Maybe the solution is simply to punt, arguing that the user is playing with fire and so sometimes will get burnt. By "punt" here, I mean that GHC just has a little unpredictability in this area. (Indeed, this is already the case, as discussed in the paper around trouble generalizing levity variables.) Maybe this is the real wisdom here: keep calm, carry on, and hope it all works. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12973#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12973: No levity-polymorphic arguments -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12973#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12973: No levity-polymorphic arguments
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone: 8.2.1
Component: Compiler | Version: 8.1
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: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#12973: No levity-polymorphic arguments -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12973 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => typecheck/should_fail/T12973 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12973#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC