Repeated variables in type family instances - UndecidableInstances

AntC anthony_clayden at clear.net.nz
Mon Jun 24 04:58:48 CEST 2013


> 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





More information about the Glasgow-haskell-users mailing list