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:
- 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 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))
wherezeta
is a unification variable that we must eventually unify withT
orC
.
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 |