[GHC] #14917: Allow levity polymorhism in binding position

[GHC]

#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      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 andrewthad):

 I agree that it isn’t always possible to inline. Higher order functions,
 like map, don’t allow it. Maybe the most accurate way to describe what I
 want is for there to be a way to make fully saturated calls to functions
 with levity polymorphic binders. It seems like it should be possible to
 perform a check for unsaturated calls. Recursive levity polymorphic
 functions would not be allowed, but there’s still a lot of useful stuff
 that could be done.

 Your point about the proof that the paper offers is good. My suggested
 addition would mess up that proof, which would be bad. What if (and this
 is total speculation since I don’t understand type theory) you had two
 universes that functions could live in. One universe is this one that we
 currently have. There are no levity polymorphic binders, and in this
 universe, you have the guarantee that you always know the runtime
 representation of values that need to be manipulated. In the second
 universe, levity polymorphism would be unrestricted. Technically, this
 universe would be a superset of the first one. But it may be helpful to
 think of them as separate universes since in GHC, codegen could only
 happen for functions in the first universe. Functions from 1 could be
 freely used in 2. Functions from 2 could be freely used in 2 as well. But,
 functions from 2 could not be freely used in 1. They would need to be
 specialized to satisfy the restrictions around levity polymorphism. In
 practice, this specialization would take the form of inlining.

 So, I guess that would mean that the function arrow would have a weird
 kind, since it could create types belonging to universe 1 or 2. And I have
 no idea how function application would typecheck.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler