Closed Type Families: type checking dumbness? [was: separate instance groups]

[AntC]

> 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