33 | | The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families. Moreover, in Forms (2) & (3), the left- and right-hand side need to be different, and the left-hand side may not occur in the right-hand side. |
34 | | |
35 | | '''SLPJ''': I think that you intend a "normal equality" to embody the Orientation Invariant and the Flattening Invariant from new-single.tex. But they don't line up exactly. For example, what about `F [x] ~ G x`? That satisfies both invariants. |
36 | | |
37 | | NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. |
38 | | |
39 | | Coercions `co` are either wanteds (represented by a flexible type variable) or givens ''aka'' locals (represented by a type term of kind CO). In GHC, they are represented by `TcRnTypes.EqInstCo`. Moreover, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules. '''SLPJ''' but I hope the difference between wanted and given is explicit (different constructor) not implicit (look at the form of the coercion). |
| 34 | where |
| 35 | |
| 36 | * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, and |
| 37 | * we call the Forms (2) & (3) '''variable equalities''', and require that the left- and right-hand side need to be different, and that the left-hand side does not occur in the right-hand side. |
| 38 | |
| 39 | === Observations === |
| 40 | |
| 41 | The following is interesting to note: |
| 42 | |
| 43 | * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. |
| 44 | * Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same. |
| 45 | * Normal equalities are '''never''' recursive. They can be mutually recursive. A mutually recursive group will exclusively contain variable equalities. |
| 46 | |
| 47 | === Coercions === |
| 48 | |
| 49 | Coercions `co` are either wanteds (represented by a flexible type variable) or givens ''aka'' locals (represented by a type term of kind CO). In GHC, they are represented by `TcRnTypes.EqInstCo`, which is defined as |
| 50 | {{{ |
| 51 | type EqInstCo = Either |
| 52 | TcTyVar -- case for wanteds (variable to be filled with a witness) |
| 53 | Coercion -- case for locals |
| 54 | }}} |
| 55 | Moreover, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules. |