## 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))`

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 |