[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:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Richard responds: This has come up before, of course. I've always had an
 affinity for choice (A). It's easy to describe, even to users, and I think
 it will lead to nice error messages (which can special-case printing
 unsolved TC constraints). I don't think it would take all that much code.

 (C) doesn't actually work, tempting though it may be. Consider (
 {{{
 f :: forall (r :: RuntimeRep) (a :: TYPE r). a -> ()
 }}}
 Don't worry about levity-polymorphism restrictions in binding positions,
 as that's not the issue here. The question is: does f take 1 visible
 argument or 0? The answer depends on the choice of r (under plan C),
 because r might be LiftedRep C. So have no way of reliably instantiating
 f's type at an occurrence and are thus dead in the water.

 Plan D:
 {{{
 data TC = T | C
 TYPE :: RuntimeRep -> TC -> Type
 }}}
 That is, make the T/C distinction totally orthogonal to representation,
 and simply disallow any quantification over a type whose kind has a
 variable in the TC position. This has the nice side effect of allowing
 unlifted constraints (e.g., an unboxed implicit parameter or a strict
 dictionary). But it has the significant drawback of polluting the type of
 `(->)`, which would now be
 {{{
 (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (tc1 :: TC) (tc2 ::
 TC).
         TYPE r1 tc1 -> TYPE r2 tc2 -> TYPE LiftedRep tc2
 }}}
 Indeed, we have considered this route before, [https://github.com/ghc-
 proposals/ghc-
 proposals/blob/0506dd68fefa26f56dd8e377d4c9d34bf241252f/proposals/0000
 -constraint-vs-type.rst here].

 The main drawback I see from that abandoned approach in the proposal is
 that it banned newtype-classes. I don't think we have a satisfactory way
 (yet) of eliminating newtype-classes while keeping, e.g., reflection
 working. (This matters: singletons uses the reflection trick to change
 exponentially-slow processes to linear ones.)

 Summing up, I see two ways forward:

 - Simon's (A)

 - (D) above, including banning newtype-classes and coming up with a new
 way for the reflection trick to work.

 Simon's (B) would work, but it seems strictly inferior to (A), simply
 because a new TyVar flavor is a more obscure approach to getting the
 behavior we would see in (A), whereas (A) uses an abstraction (a class-
 like constraint) that everyone knows and loves.

 Between these two approaches, (A) is at least an order of magnitude
 easier. So I vote for that. :) I do believe, though, that we'll have to do
 (D) eventually, though.

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