| 269 | '''RAE's examples''' |

| 270 | |

| 271 | Here are some examples that I've come up with that show some tricky points: |

| 272 | |

| 273 | {{{#!hs |

| 274 | type family E1 a = r | r -> a where |

| 275 | E1 Int = Int |

| 276 | E1 a = a |

| 277 | }}} |

| 278 | |

| 279 | According to the algorithm above, this would be rejected as non-injective. This is because clause (c) of the closed type family check says that if an equation is not subsumed by a previous equation, yet the RHSs unify, the family is flagged as non-injective. Yet, `E1` ''is'' injective. |

| 280 | |

| 281 | Here's another one: |

| 282 | |

| 283 | {{{#!hs |

| 284 | type family E2 (a :: Bool) = r | r -> a where |

| 285 | E2 False = True |

| 286 | E2 True = False |

| 287 | E2 a = False |

| 288 | }}} |

| 289 | |

| 290 | A naive injectivity check here would conclude that `E2` is not injective, because the RHS of the last equation unifies with the RHS of a previous equation, and the LHS of the last equation is not subsumed by any previous equation. But, noting that `a` (as used in the last equation) can neither be `True` nor `False`, `E2 is in fact injective. These are the "exclusions" I talk about above. |

| 291 | |