[GHC] #12973: No levity-polymorphic arguments

[GHC]

#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