[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated

[AntC]

> adam vogt <vogt.adam <at> gmail.com> writes:
> 
> > On Wed, Nov 27, 2013 at 9:22 PM, AntC wrote:
> 
> Closed type families ... wait a few weeks for ghc-7.8) 
> 

Yes, I'm in eager anticipation!

> > ...
> >  OTOH, I did feed raise that unhappy hack with Richard
> >  at the time, as a counter-example
> >  that I couldn't understand how he'd handle.
> >  So perhaps he didn't.)
> 
> Do you recall where that discussion was? 

http://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-
families/
My message on June 24. (It also mentions discussion on GHC-Users.)

This is exactly an example of a records mechanism with duplicate 'labels'.
Actually being what the HList paper calls Type-Indexed Products.

Note that the code I give there works beautifully with old-fashioned 
overlapping instances; and produces a helpful error message without any 
additional ancillary Fail classes.

It works because my records are tuples, _not_ HLists.
So instance resolution is working with a 'flat' structure where it can see 
all the types. Contrast that HCons effectively hides types in its tail.
I suspect that Richard's implementation also effectively hides potential 
duplicates by putting them in a later 'case' of the type family. 

> ... Though it seems ghc isn't eager enough ...

This is what I find most frustrating with ghc (as contrasted with dear old 
Hugs): instance failures are 'lazy'. You have to backtrack through a lot 
of code/other modules to figure out what's going wrong.

I was hoping that with Richard's work, instance validation could be eager: 
reject the instance definition as overlapping _at_the_point_of_definition_.

I think that a long time ago ghc took a wrong turn and allowed partially 
overlapping instances. It therefore has to wait until it finds a usage to 
see if it is actually ambiguous.

I think that partially overlapping instances should be banned.
Instances should be either disjunctive or wholly overlapping.
(Note that you can always reorganise a partial overlap to fit this rule.)

> ...
> Which translates to
>
> type family G' x y where
>  G' x x = Failure "mistake" ()
>  G' x y = ()

That's exactly the unhappy hack I was wanting to avoid.
If you still have to do that with closed type families,
then I'm disappointed.

I wanted disequality restraints.
(See the Sulzmann and Stuckey paper I mention earlier on Richard's 
discussion page.)

Which would be one single stand-alone instance:

    type instance G'' x y | x /~ y = ()

(I also think this has more perspicuous type inference rules,
and fits better with a mental model of all the instances 'competing' to be 
chosen at the use site; with type improvement progressing until exactly 
one matches. This does not involve instance search, which as SPJ points 
out would be death to coherence.)

Cheers
AntC