| 16 | |

| 17 | Expanding this out, you can do it for a fixed collection of types thus: |

| 18 | {{{ |

| 19 | type instance Equal Int Int = True |

| 20 | type instance Equal Bool Bool = True |

| 21 | type instance Equal Int Bool = False |

| 22 | type instance Equal Bool Int = False |

| 23 | }}} |

| 24 | but this obviously gets stupid as you add more types. |

| 25 | |

| 26 | Furthermore, this is not what you want. Even if we restrict the equality function to booleans |

| 27 | {{{ |

| 28 | type family Equal (a :: Bool) (b :: Bool) :: Bool |

| 29 | }}} |

| 30 | we can't define instances of Equal so that a constraint like this one |

| 31 | {{{ |

| 32 | Equal a a ~ True |

| 33 | }}} |

| 34 | is satisfiable---the type instances only reduce if a is known to True or False. GHC doesn't reason by cases. (Nor should it, |Any| also inhabits |Bool|. No kinds really are closed.) |

| 35 | |

| 36 | The only way to work with this sort of reasoning is to use Overlapping Instances, as suggested in the [http://homepages.cwi.nl/~ralf/HList/ HList paper.] |