adam vogt
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