Note [Reverse order of fundep equations]
Consider this scenario (from dependent/should_fail/T13135_simple):
type Sig :: Type -> Type
data Sig a = SigFun a (Sig a)
type SmartFun :: forall (t :: Type). Sig t -> Type
type family SmartFun sig = r | r -> sig where
SmartFun @Type (SigFun @Type a sig) = a -> SmartFun @Type sig
[W] SmartFun @kappa sigma ~ (Int -> Bool)
The injectivity of SmartFun allows us to produce two new equalities:
[W] w1 :: Type ~ kappa
[W] w2 :: SigFun @Type Int beta ~ sigma
for some fresh (beta :: SigType). The second Wanted here is actually
heterogeneous: the LHS has type Sig Type while the RHS has type Sig kappa.
Of course, if we solve the first wanted first, the second becomes homogeneous.
When looking for injectivity-inspired equalities, we work left-to-right,
producing the two equalities in the order written above. However, these
equalities are then passed into wrapUnifierTcS, which will fail, adding these
to the work list. However, crucially, the work list operates like a *stack*.
So, because we add w1 and then w2, we process w2 first. This is silly: solving
w1 would unlock w2. So we make sure to add equalities to the work
list in left-to-right order, which requires a few key calls to 'reverse'.
This treatment is also used for class-based functional dependencies, although
we do not have a program yet known to exhibit a loop there. It just seems
like the right thing to do.
When this was originally conceived, it was necessary to avoid a loop in T13135.
That loop is now avoided by continuing with the kind equality (not the type
equality) in canEqCanLHSHetero (see Note [Equalities with heterogeneous kinds]).
However, the idea of working left-to-right still seems worthwhile, and so the calls
to 'reverse' remain. References 1
- Equalities with heterogeneous kinds GHC.Tc.Solver.Equality
Referenced by 2
- GHC.Tc.Solver.Equality call site
- GHC.Tc.Solver.Monad call site