Note [Lift equality constraints when quantifying]
We can't quantify over a constraint (t1 ~# t2) because that isn't a predicate type; see Note [Types for coercions, predicates, and evidence] in GHC.Core.Predicate So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted to Coercible. This tiresome lifting is the reason that pick_me (in pickQuantifiablePreds) returns a Maybe rather than a Bool.
References 1
- Types for coercions, predicates, and evidence GHC.Core.Predicate
Referenced by 4
- GHC.Tc.Solver call site
- pickQuantifiablePreds GHC.Tc.Solver
- Equality evidence in pattern synonyms GHC.Tc.TyCl.PatSyn
- GHC.Tc.Validity call site