[source]

compiler/deSugar/TmOracle.hs

Note [Deep equalities]

[note link]

Solving nested equalities is the most difficult part. The general strategy is the following:

• Equalities of the form (True ~ (e1 ~ e2)) are transformed to just (e1 ~ e2) and then treated recursively.
• Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless we know more about the inner equality (e1 ~ e2). That’s exactly what `simplifyEqExpr’ tries to do: It takes e1 and e2 and either returns truePmExpr, falsePmExpr or (e1’ ~ e2’) in case it is uncertain. Note that it is not e but rather e’, since it may perform some simplifications deeper.