Better type inference for Constraint vs Type
An enduring infelicity in GHC’s type inference is the treatment of tuples. Consider, this from
type family F c sch where F _ ' = (() :: Constraint) F c (col ': cols) = (c Int, F c cols)
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
Constraint respectively – and they are different kinds. How can we choose which?
Currently we have the following unsatisfactory ruse:
- Look at the “expected kind”. If we kind-check the second equation first we learn nothing from that
- Infer kinds for all of the elements of the type. Again in this case we learn nothing.
- 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
Constraint”. When generalising, default to
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.
type Type = TYPE (LiftedRep T) type Constraint = TYPE (LiftedRep C)
So now we can unify
(TYPE (LiftedRep zeta))where
zetais a unification variable that we must eventually unify with
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