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

[GHC]

#14917: Allow levity polymorphism 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 Ericson2314):

 Taking a step back, I think the first thing we need is a notion of a
 monomorphic term. A closed term is a monomorphic term, but sime open terwm
 are too. A term whose free variables are all irellevant is also a
 monomorphic term. This might seem counterintuitive and maybe I need a new
 name because of that, but it makes sense because we don't actually want to
 specialize on types: we just want to specialize on relevant things like
 runtime representations and constraint dictionaries.

 The second thing to note is that is that substitution preserves
 monomorphic-term-ness, so in some sense template polymorphism shouldn't be
 too hard. What I mean by preservation is that it that the body of an
 abstraction is a monomorphic term other than the free variable being
 replaced, and the substituted term is monomorphic, then the beta-reduced
 term is monnomorphic. The issue with polymorphic recursion is not that we
 can't make progress unlining, but that the partial evaluation may not
 terminate. For template polymorphism, I think annotations are sufficient.
 We want be able to force otherwise-optional specialization "deeply", and
 control where that request is undecidable vs where it is guaranteed to
 succeed or prevented from trying.

 The new quanitifers would be, as said, to require specialization, with the
 "infection" @goldfire points out that entails. Besides runtime reps, this
 is also needed for CLaSH, and intrinsics taking immediate values (as
 @carter told me about). Variables bound with such quantifiers would not
 penalize monnomorphic terms. That means the final definition of a
 monnomorphic term is one whose free variables are all irellevant or
 "monomorphizable".

 Lastly, I welcome the object file problems. As we said to @goldfire and
 @nomeata at an NYC Meetup, it's annoying that module organization, a
 convenience for humans, ends up affecting performance. We desperately want
 to cache compilation on as fine a granularity as possible, too. I hope
 tackling this inlining issue forces that caching one.

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