Major refactor in the handling of equality constraints
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, 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 Compile times decrease by an average of 0.1%; but there is a 7.4% drop in compiler allocation on T15703. Metric Decrease: T15703
parent
e1fb56b2
Branches wip/ttg-booleanformula
No related tags found
Pipeline #64979 failed
Showing
- compiler/GHC/Core/Opt/Simplify/Iteration.hs 3 additions, 3 deletionscompiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/TyCo/FVs.hs 46 additions, 19 deletionscompiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs 7 additions, 2 deletionscompiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCon.hs 32 additions, 27 deletionscompiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs 44 additions, 14 deletionscompiler/GHC/Core/Type.hs
- compiler/GHC/Core/Type.hs-boot 2 additions, 1 deletioncompiler/GHC/Core/Type.hs-boot
- compiler/GHC/Data/Bag.hs 12 additions, 1 deletioncompiler/GHC/Data/Bag.hs
- compiler/GHC/Data/Maybe.hs 2 additions, 1 deletioncompiler/GHC/Data/Maybe.hs
- compiler/GHC/Tc/Errors.hs 40 additions, 45 deletionscompiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs 5 additions, 5 deletionscompiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Solver.hs 3 additions, 0 deletionscompiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Equality.hs 462 additions, 402 deletionscompiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs 19 additions, 16 deletionscompiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs 233 additions, 197 deletionscompiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs 109 additions, 71 deletionscompiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Concrete.hs 4 additions, 6 deletionscompiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/TcMType.hs 27 additions, 4 deletionscompiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs 13 additions, 3 deletionscompiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs 719 additions, 223 deletionscompiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/ado/T16135.stderr 14 additions, 0 deletionstestsuite/tests/ado/T16135.stderr
Loading
Please register or sign in to comment