Liberalising IncoherentInstances

[Axel Simon]

Dear Simon,

On Jul 27, 2013, at 22:16 , Simon Peyton-Jones <simonpj at microsoft.com> wrote:
[..]

> So the change I propose to make IncoherentInstances to pick arbitrarily among instances that match.  More precisely, when trying to find an instance matching a target constraint (C tys),
> 
> a) Find all instances matching (C tys); these are the candidates
> 
> b) Eliminate any candidate X for which another candidate Y is
>  strictly more specific (ie Y is a substitution instance of X),
>  if either X or Y was complied with -XOverlappingInstances
> 
> c) Check that any non-candidate instances that *unify* with (C tys)
>   were compiled with -XIncoherentInstances
> 
> d) If only one candidate remains, pick it.
>    Otherwise if all remaining candidates were compiled with
>    -XInccoherentInstances, pick an arbitrary candidate
> 
> All of this is precisely as now, except for the "Otherwise" part of (d).  One could imagine different flags for the test in (c) and (d) but I really don't think it's worth it.
> 

a big -1.

In recent years I acquired the view that type inferences should have some sort of semantic completeness property since otherwise the user has to know exactly how the internals of the inference works in order to understand why a program type checks or not. With "semantic completeness" I mean "the best possible type that that can be expressed by the type language". Haskell is not doing so well with all these ad-hoc deduction rules like the ones you've listed above that skirt around the problem that it is not clear what the best type is. 

What you propose here is going a step further: you propose that the internal implementation of the type inference  not only determines if the program compiles, but also determines its semantics since choosing form different instance in general means choosing from different code. In the worst case, the sequence in which you read in the various modules from disc may alter the behavior of the code. An application therefore might only work correctly if compiled on a specific machine with a specific ghc version and a specific inode numbering of your files.

So if you really want an "Otherwise" in rule d), I suggest the following:

"Otherwise, compare the abstract syntax trees of all remaining candidate instances for equality. If they all equal, pick one, else reject the program.

This is a bit weird, but I guess it will suffice for people using this feature.

Regards,
Axel

> 
> Incidentally, I think it'd be an improvement to localise the Overlapping/Incoherent flags to particular instance declarations, via pragmas, something like
> 	instance C [a] where
> 	  {-# ALLOW_OVERLAP #-}
> 	  op x = ....
> 
> Similarly {-# ALLOW_INCOHERENT #-}.   Having -XOverlappingInstances for the whole module is a bit crude., and might be missed when looking at an instance.   How valuable would this be?
> 
> [1] http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap
> [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers
> 
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users