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 Constraint.

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 (closed) #18170
• #17368 Homogeneous equality
• #18756 Linear types submultiplicity
• #19915 Perhaps tagToEnum#/withDict
• #20532 (closed) Perhaps dataToTag#
• #14722 (comment 148235) Use a constraint in illegal VTA
• Possibly eqPhantPrimTyCon. It's currently documented as: "This is only used to make higher-order equalities. Nothing should ever actually have this type!"
• (not tested) Perhaps we could have a FixedKind type in parallel to FixedRuntimeRep, and then it would be used when -XNoPolyKinds is on. Likewise FixedMultiplicity.
• Possibly warnAboutIdentities: this is used to warn about identity conversions in the desugarer. We could have a predicate ConvertFrom X Y that could always be solved, but would raise a warning when X and Y are known to be the same. That would move the warning from the desugarer to the typechecker. In addition, in the list of relevant functions listed in conversionNames there's a comment "We can't easily add fromIntegerName, fromRationalName, because they are generated by literals" - by doing this check earlier, we'd know if we're checking a literal or an application.
  • Other type-directed warnings are possible. For example, comparing references (eqStableName, testEquality etc.) on types that are known to be apart (not just not known to be equal) could be a warning. This is dual to ConvertFrom X Y: it detects apartness rather than equality.
  • Or a warning when a polymorphic function is going to become a monomorphic one, e.g. #24316 (closed)
  • Or disabling unused bind warnings for singleton types #26006
• Restrictions on datatype kinds in Note [Datatype return kinds]: "The /principle/ here is that in the TyCon for a data type or data instance, we must be able to lay out all the type-variable binders, one by one, until we reach (TYPE xx). There is no place for a cast here.". This is similar to TypeLike or IsRefl#, but on the other hand, it's a syntactic check which does not involve the constraint solver. Therefore, it's not as convincing as other examples.

We could support default declarations to control defaulting, though this makes most sense with representation polymorphism.

Predicates could be made available in signature and hs-boot files (as in #20358), but this caused issues in representation polymorphism !6705 (comment 383380).

If the evidence of a predicate is explicit in Core, it could work with -fdefer-type-errors; otherwise, it'll have to be nondeferrable (nonDeferrableOrigin).

There's a possibility of integrating with TH CodeC constraints, see https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep#typed-template-haskell

WIP branch: !2857