Dan Doel writes:
It seems to me the problem is that there's no way to define classes by consecutive cases to match the family definitions.
Thanks Dan, yes we've an impedance mis-match. Closed logic for type families; Open (or Distributed) logic for class instances. I see two possible fixes: 1. Closed logic for class instances
I don't know what a good syntax for that would be, since 'where' syntax is taken for those.
Indeed. We could follow SQL and use 'HAVING' ;-) 2. Open/Distributed logic for type families (and class instances). Take the example type family:
type family F a where F (Foo Int c) = Int F (Foo b Char) = Char
For instance selection to move confidently from the first to the second equation, it must satisfy itself that Foo's first arg could not possibly be Int. ie (b /~ Int) Let's expose the compiler's internal workings into the surface lang. And annotate that on the second equation as F (Foo b Char) | (b /~ Int) = Char This mirrors the syntax for pattern guards. Now no usage site could ever match both equations. (And we can prove that as we validate each instance.) So we could 'float' the type instances away to appear with the class instances -- even as Associated types. (And we'd need type disequality guards on the class instances.) AntC