#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