Skip to content

Major refactor of equality constraints in the constraint solver

Simon Peyton Jones requested to merge wip/T22194-flags into master

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: see canEqCanLHSFinish_try_unification.

There are loads of smaller changes:

  • The on-the-fly unifier GHC.Tc.Utils.Unify.unifyType has a cheap-and-cheerful version of checkTyEqRhs, called simpleUnifyCheck. If simpleUnifyCheck 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 involving swap_for_occurs and canEqTyVarFunEq. Much nicer now. See Note [Orienting TyVarLHS/TyFamLHS] Note [Orienting TyFamLHS/TyFamLHS]

  • Added cteSkolemOccurs, cteConcrete, and cteCoercionHole to the problems that can be discovered by checkTyEqRhs.

Yet smaller:

  • Added a synIsConcrete flag to SynonymTyCon (alongside synIsFamFree) to reduce the need for synonym expansion when checking concreteness. Use it in isConcreteType.

  • Renamed isConcrete to isConcreteType

  • 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 in GHC.Tc.Utils.Unify.definitely_poly, which in turn is used quite a lot.

  • Moved rewriterView to GHC.Core.Type, so we can use it from the constraint solver.

Fixes #22194 (closed)

Edited by Simon Peyton Jones

Merge request reports