Better type inference for Constraint vs Type

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

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture