| 33 | |

| 34 | === Defining total families === |

| 35 | |

| 36 | To enable textual disambiguation of overlapping instances, we declare the equalities together (by transferring GADT syntax to type synonyms): |

| 37 | {{{ |

| 38 | type TypeEq s t where |

| 39 | TypeEq s s = TTrue |

| 40 | TypeEq s t = TFalse |

| 41 | }}} |

| 42 | `TypeEq` is a standard type family, but by virtue of being total (i.e., exhaustive) it is also closed. Further equalities cannot define it any further. |

| 43 | |

| 44 | Let's use the same idea for the addition/multiplication examples: |

| 45 | {{{ |

| 46 | type x :+ y where |

| 47 | Z :+ y = y |

| 48 | S x :+ y = S (x :+ y) |

| 49 | |

| 50 | type x :* y where |

| 51 | Z :* y = Z |

| 52 | (S x) :* y = x :* y :+ y |

| 53 | }}} |

| 54 | In contrast to `TypeEq`, `(:+)` and `(:*)` is not total without an extra equality. We take another idea from value-level function definitions and implicitly complete each of these definitions by a final catch all equality. So, for `(:+)`, we assume a final |

| 55 | {{{ |

| 56 | x :+ y = VOID |

| 57 | }}} |

| 58 | and for `(:*)` a final |

| 59 | {{{ |

| 60 | x :* y = VOID |

| 61 | }}} |

| 62 | |

| 63 | === Critical examples from the paper === |

| 64 | |

| 65 | |