Repeated variables in type family instances - UndecidableInstances

[Richard Eisenberg]

In an attempt to dredge out the mud from these waters, I have updated the
wiki page at
http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
to have the correct details about the current implementation (which has been
merged with HEAD).

A few salient points:
* Open (normal, old-fashioned) type families are essentially unchanged. In
particular, coincident overlap and non-linear patterns *are* allowed.
* The overlap check between open type family instances now does a
unification without an "occurs check" to mark (x, x) and ([y], y) as
overlapping, as necessary for type soundness.
* Coincident overlap within closed families works just fine, the way you
might expect. In particular, in both the theory and the implementation, any
set of type instances you could write in an open family can be combined in a
closed family, and they will behave in exactly the same way. This is a
marked improvement over the last implementation.

As for AntC's finer-grained UndecidableInstances: I think that would be
great, too. In general, I'm of the opinion that the brutal termination
checker could use some improvements. But, there's little incentive to do so,
with the ease of just saying UndecidableInstances. Even then, though, some
reasonable type-level computations really don't terminate in all cases
(division) and these still have a role to play.

Richard

PS: Sorry to those of you who have used "type instance where" and now find
that your code doesn't compile. We (Simon, Dimitrios, and I) put a good deal
of thought into the original design. But, we really liked the new one more.
Given that the feature never made it into a released GHC, we thought it was
OK to make this breaking change before it became impossible. Note that you
can simulate the openness of "type instance where" by using an open family
with closed family helpers.

> -----Original Message-----
> From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
> users-bounces at haskell.org] On Behalf Of AntC
> Sent: 24 June 2013 03:59
> To: glasgow-haskell-users at haskell.org
> Subject: Re: Repeated variables in type family instances -
> UndecidableInstances
> 
> > Richard Eisenberg <eir <at> cis.upenn.edu> writes:
> >
> > ... The plan of action is to use the check labeled (B)
> > on the wiki page. This check does *not* ban all nonlinear type families.
> 
> Thanks Richard, great! Then the focus of attention moves to infinite
types.
> 
> I don't think anybody intentionally wants infinite types,
> so UndecidableInstances ought to be switched off,
> to catch unintended instances.
> 
> But often there's a need for one or two instances to break the coverage
> conditions. (For example one of Oleg's standard techniques is to introduce
> a 'helper class' that has the same parameters as the based-on class, plus
> some extra parameter that drives instance selection, and is computed from
> the types of the arguments. It's not easy to see at this stage how that
> technique will translate into 'closed type families'.)
> 
> The trouble with the UndecidableInstances flag is that it's a very blunt
> instrument module-wide. A 'nice to have' would be to make it
finer-grained:
> - set Undecidableness on a per-instance or per-family basis.
> - or even: validate that the RHS of this instance uses a decidable family
>            but allow the RHS to break cover compared to LHS
> 
> (OK, I know that for a 'decidable' family there could be instances
> declared in other modules that get compiled with a different flag setting.
> But with 'closed type families', that can't happen, right?)
> 
> AntC
> 
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users