Use predicates in the constraint solver
Sometimes it would be useful if type inference could emit a requirement that does not have a corresponding constraint in Haskell.
For example, when typechecking the body of a forall, we should require that its kind is either
TYPE r or
Constraint. This could be done with a predicate
TypeLike a. The evidence for a TypeLike is a coercion whose right-hand side is either
TYPE r or
Implementation plan: make it so that constraints (
Cts and friends) are no longer classified by types, but are classified directly by PredTrees. (Rename that type, too.) Then, make TypeLike a constructor in PredTree. This means we don't have to wire in a type that will be used only internally. Create a coercion hole when the TypeLike constraint arises.
TypeLike is used only in the typechecker and is absent in Core. However, most predicates can have a corresponding Core Lint check.
This ticket will be useful in:
- #15979 #19573 #8388 TypeLike: body of a forall, either TYPE r or Constraint
- Likewise tuple inference: either Type or Constraint
- #17201 FixedRuntimeRep, also should fix #13105 #17518 #17536 #18170
- #17368 Homogeneous equality
- #18756 Linear types submultiplicity
- #19915 Perhaps tagToEnum/withDict
WIP branch: !2857