Major refactor of equality constraints in the constraint solver
This MR substantially refactors the way in which the constraint solver deals with equality constraints. The big thing is:
- Intead of a pipeline in which we /first/ canonicalise and /then/ interact (the latter including performing unification) the two steps are more closely integreated into one. That avoids the current rather indirect communication between the two steps.
The proximate cause for this refactoring is fixing #22194 (closed), which involve solving [W] alpha[2] ~ Maybe (F beta[4]) by doing this: alpha[2] := Maybe delta[2] [W] delta[2] ~ F beta[4] That is, we don't promote beta[4]! This is very like introducing a cycle breaker, and was very awkward to do before, but now it is all nice. See GHC.Tc.Utils.Unify Note [Promotion and level-checking] and Note [Family applications in canonical constraints].
The big change is this:
-
Several canonicalisation checks (occurs-check, cycle-breaking, checking for concreteness) are combined into one new function: GHC.Tc.Utils.Unify.checkTyEqRhs
This function is controlled by
TyEqFlags
, which says what to do for foralls, type families etc. -
canEqCanLHSFinish
now sees if unification is possible, and if so, actually does it: seecanEqCanLHSFinish_try_unification
.
There are loads of smaller changes:
-
The on-the-fly unifier
GHC.Tc.Utils.Unify.unifyType
has a cheap-and-cheerful version ofcheckTyEqRhs
, calledsimpleUnifyCheck
. IfsimpleUnifyCheck
succeeds, it can unify, otherwise it defers by emitting a constraint. This is simpler than before. -
I simplified the swapping code in
GHC.Tc.Solver.Equality.canEqCanLHS
. Especially the nasty stuff involvingswap_for_occurs
andcanEqTyVarFunEq
. Much nicer now. See Note [Orienting TyVarLHS/TyFamLHS] Note [Orienting TyFamLHS/TyFamLHS] -
Added
cteSkolemOccurs
,cteConcrete
, andcteCoercionHole
to the problems that can be discovered bycheckTyEqRhs
.
Yet smaller:
-
Added a
synIsConcrete
flag toSynonymTyCon
(alongsidesynIsFamFree
) to reduce the need for synonym expansion when checking concreteness. Use it inisConcreteType
. -
Renamed
isConcrete
toisConcreteType
-
Defined
GHC.Core.TyCo.FVs.isInjectiveInType
as a more efficient way to find if a particular type variable is used injectively than finding all the injective variables. It is called inGHC.Tc.Utils.Unify.definitely_poly
, which in turn is used quite a lot. -
Moved
rewriterView
toGHC.Core.Type
, so we can use it from the constraint solver.
Fixes #22194 (closed)