Note [Decomposing type family applications]
Supose we have
[G/W] (F ty1) ~r (F ty2)
This is handled by the TyFamLHS/TyFamLHS case of canEqCanLHS2.
We never decompose to
[G/W] ty1 ~r' ty2
Instead
* For Givens we do nothing. Injective type families have no corresponding
evidence of their injectivity, so we cannot decompose an
injective-type-family Given.
* For Wanteds, for the Nominal role only, we emit new Wanteds rather like
functional dependencies, for each injective argument position.
E.g type family F a b -- injective in first arg, but not second
[W] (F s1 t1) ~N (F s2 t2)
Emit new Wanteds
[W] s1 ~N s2
But retain the existing, unsolved constraint. References 0
This Note does not link to any other.
Referenced by 3
- GHC.Tc.Solver.Equality call site
- Type inference for type families with injectivity GHC.Tc.Solver.Equality
- Decomposing TyConApp equalities GHC.Tc.Solver.Equality