[GHC] #16148: Better type inference for Constraint vs Type

[GHC]

#16148: Better type inference for Constraint vs Type
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11621, #11715,   |  Differential Rev(s):
  #13742, #16139                     |
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 >  You say "don't worry about levity polymorphism", but the example you
 give is explicitly ruled out by our lev-poly story

 Ah, that's not true: see [https://www.microsoft.com/en-
 us/research/publication/levity-polymorphism/ Section 7.3 of the levity-
 polymorphism paper], where we discuss functions like
 {{{
 absX :: forall (r :: RuntimeRep) (a :: TYPE r). NumX a => a -> a
 }}}
 where `NumX :: forall (r :: RuntimeRep). TYPE r -> Constraint` is levity-
 polymorphic.  Here we allow `absX` to have an arrow `a -> a` with a
 levity-polymorphic argument; it's just ''term binders'' that can't have
 levity-polymorphic types.

 Another point is that messing with TYPE etc affects the entire compiler.
 A major merit of plan (A) is that it affects the type inference engine
 only and is then gone.

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