[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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 An enduring infelicity in GHC’s type inference is the treatment of tuples.
 Consider, this from `RaeJobTalk`:
 {{{
 type family F c sch where
   F _ '[] = (() :: Constraint)
   F c (col ': cols) = (c Int, F c cols)
 }}}
 When kind-checking `F`, we initially give it a return kind of kappa, a
 unification variable.  Suppose we kind-check the second equation first.
 Then what kind of tuple is it, a constraint tuple, or an ordinary type
 tuple.  We must unify kappa with `Type` or `Constraint` respectively – and
 they are different kinds.  How can we choose which?
 Currently we have the following unsatisfactory ruse:

 1. Look at the “expected kind”.   If we kind-check the second equation
 first we learn nothing from that
 2. Infer kinds for all of the elements of the type.  Again in this case we
 learn nothing.
 3. If we still know nothing, arbitrarily pick Type

 This is horrible.  If we kind check the first equation first, step 1 will
 discover Constraint, and kind checking succeeds.  But if we put the
 equations in the other order, kind checking fails.  Ugh!

 Another example with exactly the same cause is #16139.

 What to do?  I can only think of three approaches:

 A. Add a pseudo constraint `(TC kappa)` meaning “kappa must eventually
 turn out to be either `Type` or `Constraint`”.   When generalising,
 default to `Type`.

 B. Same, but by having a special sort of TauTv, a TCTv, which can only
 unify with Type or Constraint.  Again, do not generalise over such type
 variables.

 C. Define
 {{{
 type Type = TYPE (LiftedRep T)
 type Constraint = TYPE (LiftedRep C)
 }}}
     So now we can unify `kappa` with `(TYPE (LiftedRep zeta))` where
 `zeta` is a unification variable that we must eventually unify with `T` or
 `C`.

 Of these, (C) seems most principled, but somehow over-elaborate for our
 purposes.   And the others also seem to be rather too much work to solve a
 simple, local problem.

 -------------
 For reference, here are the current kinding rules
 {{{
           t1 : TYPE rep1
           t2 : TYPE rep2
     (FUN) ----------------
           t1 -> t2 : Type

           t1 : Constraint
           t2 : TYPE rep
   (PRED1) ----------------
           t1 => t2 : Type

           t1 : Constraint
           t2 : Constraint
   (PRED2) ---------------------
           t1 => t2 : Constraint

           ty : TYPE rep
           `a` is not free in rep
 (FORALL1) -----------------------
           forall a. ty : TYPE rep

           ty : Constraint
 (FORALL2) -------------------------
           forall a. ty : Constraint
 }}}

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