3 | | See https://github.com/dreixel/New-axioms for a draft of the design ([https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl cached pdf]). |

| 3 | == Background == |

| 4 | One might imagine that it would be a simple matter to have a type-level function |

| 5 | {{{ |

| 6 | type family :: Equal a b :: Bool |

| 7 | }}} |

| 8 | so that `(Equal t1 t2)` was `True` if `t1`=`t2` and `False` otherwise. But it isn't. You can do it for a fixed collection of types thus: |

| 9 | {{{ |

| 10 | type instance Equal a a = True |

| 11 | type instance Equal Int Bool = False |

| 12 | type instance Equal Bool Int = False |

| 13 | }}} |

| 14 | but this obviously gets stupid as you add more types. Nor can you write |

| 15 | {{{ |

| 16 | type instance Equal a a = True |

| 17 | type instance Equal a b = False |

| 18 | }}} |

| 19 | because System FC (rightly) prohibits overlapping family instances. |

| 20 | |

| 21 | == What to do about it == |

| 22 | |

| 23 | So the deficiency is in System FC, and it seems fundamental. We've been working on an extension to System FC, with a corresponding source-language extension, that does allow overlapping type families, with care. You would write something like this: |

| 24 | {{{ |

| 25 | type instance where |

| 26 | Equal a a = True |

| 27 | Equal a b = False |

| 28 | }}} |

| 29 | |

| 30 | This wiki page is a stub: |

| 31 | * See [https://github.com/dreixel/New-axioms this Github repo] for a Latex draft of the design |

| 32 | * Here is a [https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl cached pdf] of the current state |

| 33 | * We'll use GHC branch `ghc-axioms` for development work. |

| 34 | |

| 35 | Status (Jan 12): the groundwork is done, in HEAD; mainly making `CoAxiom` a more fundamental data type. Not yet started on the details. |