50 | | 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: |

| 50 | 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. Here's the idea: |

| 51 | |

| 52 | * A `type instance` declaration can define multiple equations, not just one: |

| 59 | * Patterns within a single `type instance` declaration (henceforth "group") may overlap, and are matched top to bottom. |

| 60 | |

| 61 | * A single type family may, as now, have multiple `type instance` declarations: |

| 62 | {{{ |

| 63 | type family F a :: * |

| 64 | |

| 65 | type instance F where |

| 66 | F [Int] = Int |

| 67 | F [a] = Bool |

| 68 | |

| 69 | type instance F where |

| 70 | F (Int,b) = Char |

| 71 | F (a,b) = [Char] |

| 72 | }}} |

| 73 | |

| 74 | * The groups for `F` may not overlap. That is, there must be no type `t` such that `(F t)` matches both groups. |

| 75 | |

| 76 | * The groups do not need to be exhaustive. If there is no equation that matches, the call is stuck. (This is exactly as at present.) |

| 77 | |

| 78 | * It would perhaps be possible to emit warnings for equations that are shadowed: |

| 79 | {{{ |

| 80 | type instance F where |

| 81 | F (a,b) = [Char] |

| 82 | F (Int,b) = Char |

| 83 | }}} |

| 84 | Here the second equation can never match. |

| 85 | |