Liberalising IncoherentInstances

Friends I've realised that GHC's -XIncoherentInstances flag is, I think, over-conservative. I propose to liberalise it a bit. This email describes the issue. Please yell if you think this is a bad idea. Simon Suppose we have class C a where { op :: a -> String } instance C [a] where ... instance C [Char] where ... f :: [b] -> String f xs = "Result:" ++ op xs With -XOverlappingInstances, but without -XIncoherentInstances, f won't compile. Reason: if we call 'f' at Char (e.g. f "foo") then you might think we should use instance C [Char]. For example, if we inlined 'f' at the call site, to get ("Result:" ++ op "foo"), we certainly then would use the C [Char] instance, giving perhaps different results. If we accept the program as-is, we'll permanently commit 'f' to using the C [a] instance. The -XIncoherentInstances flag says "Go ahead and use an instance, even if another instance might become relevant if you were to specialise or inline the enclosing function." The GHC user manual gives a more precise spec [1]. Now consider this class D a b where { opD :: a -> b -> String } instance D Int b where ... instance D a Int where ... g (x::Int) = opD x x Here 'g' gives rise to a constraint (D Int Int), and that matches two instance declarations. So this is rejected regardless of flags. We can fix it up by adding instance D Int Int where ... but this is pretty tiresome in cases where it really doesn't matter which instance you choose. (And I have a use-case where it's more than tiresome [2].) The underlying issue is similar to the previous example. Before, there was *potentially* more than one way to generate evidence for (C [b]); here there is *actually* more than one instance. In both cases the dynamic semantics of the language are potentially affected by the choice -- but -XIncoherentInstnaces says "I don't care". 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. 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-extension... [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers

Simon Peyton-Jones
writes: I've realised that GHC's -XIncoherentInstances flag is, I think, over-conservative.
Hi Simon, by coincidence I've just come across a very similar issue with overlapping instances and FunDeps (following-up some discussion with Oleg, MartinS, EdwardK). Starting with: class C a b | a -> b where foo :: a -> b instance C [a] [a] where foo = id t1 = foo "a" -- t1 :: [Char] -> [Char] I then added: instance C [Char] [Char] where foo = id -- more specific! t2 = foo "a" -- t2 :: C [a] [a] => [a] -> [a] -- more polymorphic! My (probably subjective) experience is that somewhere around 2006 when Type Families started appearing, there were some subtle changes around overlaps. TF's seemed to be very pre-occupied with supporting 'coincident' (or confluent) _partial_ overlap. (By partial overlap I mean: some substitutions match both instances, some only one, some only t'other. This seems to be the root of the issue with Joachim's post on ghc-devs.) Partial overlaps are always going to be awkward for IncoherentInstances. With Type Families, you can always check that the result is confluent. But for class instances there's no such algebraic/semantic check possible. It's easy to avoid partial overlaps: just define an instance for the mgu of the overlap; then both of the less-specific instances totally overlap it. With the benefit of hindsight, I would have banned partial overlaps. IMO we could then validate class instance 'eagerly' at point of declaration (as Hugs does), rather than paying the penalty later with hazy/lazy instance selection woes. I strenuously try to avoid needing IncoherentInstances. I've no objection to your proposed "liberalise a bit".
Incidentally, I think it'd be an improvement to localise the
instance declarations, via pragmas, something like instance C [a] where {-# ALLOW_OVERLAP #-} op x = ....
Similarly {-# ALLOW_INCOHERENT #-}. Having -XOverlappingInstances for
and might be missed when looking at an instance. How valuable would
Overlapping/Incoherent flags to particular the whole module is a bit crude., this be?
+1 I strongly support localising these flags. Very seldom do I want Overlapping for every class in a module, and I'd rather the compiler told me if I inadvertently did overlap an instance. Better still, can we do {-# DISALLOW_PARTIAL #-} ?

AntC
writes:
Uh-oh, quoted the wrong example. I mean: Starting with: class C a b | a -> b where foo :: a -> b instance C [a] [a] where foo = id t11 = \x -> foo [x] -- t11 :: t -> [t] I then added: instance C [Char] [Char] where foo = id -- more specific! t12 = \x -> [x] -- t12 :: C [t] [t] => t -> [t] -- more polymorphic!

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 It would be nice to have same option for undecidable instances as well.

I'll probably never use it, but I can't see any real problems with the
proposal. In many ways it is what I always expected IncoherentInstances to
be.
One thing you might consider is that if you have to make an arbitrary
instance selection at the end during compile time, making that emit a
warning by default or at least under -Wall. That way it is clear when you
are leaning on underdetermined semantics.
-Edward
On Sat, Jul 27, 2013 at 4:16 PM, Simon Peyton-Jones
Friends
I've realised that GHC's -XIncoherentInstances flag is, I think, over-conservative. I propose to liberalise it a bit. This email describes the issue. Please yell if you think this is a bad idea.
Simon
Suppose we have
class C a where { op :: a -> String } instance C [a] where ... instance C [Char] where ...
f :: [b] -> String f xs = "Result:" ++ op xs
With -XOverlappingInstances, but without -XIncoherentInstances, f won't compile. Reason: if we call 'f' at Char (e.g. f "foo") then you might think we should use instance C [Char]. For example, if we inlined 'f' at the call site, to get ("Result:" ++ op "foo"), we certainly then would use the C [Char] instance, giving perhaps different results. If we accept the program as-is, we'll permanently commit 'f' to using the C [a] instance.
The -XIncoherentInstances flag says "Go ahead and use an instance, even if another instance might become relevant if you were to specialise or inline the enclosing function." The GHC user manual gives a more precise spec [1].
Now consider this class D a b where { opD :: a -> b -> String } instance D Int b where ... instance D a Int where ...
g (x::Int) = opD x x
Here 'g' gives rise to a constraint (D Int Int), and that matches two instance declarations. So this is rejected regardless of flags. We can fix it up by adding instance D Int Int where ... but this is pretty tiresome in cases where it really doesn't matter which instance you choose. (And I have a use-case where it's more than tiresome [2].)
The underlying issue is similar to the previous example. Before, there was *potentially* more than one way to generate evidence for (C [b]); here there is *actually* more than one instance. In both cases the dynamic semantics of the language are potentially affected by the choice -- but -XIncoherentInstnaces says "I don't care".
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.
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-extension... [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

+1 to the original proposal and Edward's suggestion of emitting a warning.
I've occasionally wanted this behavior from IncoherentInstances as well.
On Mon, Jul 29, 2013 at 3:01 PM, Edward Kmett
I'll probably never use it, but I can't see any real problems with the proposal. In many ways it is what I always expected IncoherentInstances to be.
One thing you might consider is that if you have to make an arbitrary instance selection at the end during compile time, making that emit a warning by default or at least under -Wall. That way it is clear when you are leaning on underdetermined semantics.
-Edward
On Sat, Jul 27, 2013 at 4:16 PM, Simon Peyton-Jones
wrote:
Friends
I've realised that GHC's -XIncoherentInstances flag is, I think, over-conservative. I propose to liberalise it a bit. This email describes the issue. Please yell if you think this is a bad idea.
Simon
Suppose we have
class C a where { op :: a -> String } instance C [a] where ... instance C [Char] where ...
f :: [b] -> String f xs = "Result:" ++ op xs
With -XOverlappingInstances, but without -XIncoherentInstances, f won't compile. Reason: if we call 'f' at Char (e.g. f "foo") then you might think we should use instance C [Char]. For example, if we inlined 'f' at the call site, to get ("Result:" ++ op "foo"), we certainly then would use the C [Char] instance, giving perhaps different results. If we accept the program as-is, we'll permanently commit 'f' to using the C [a] instance.
The -XIncoherentInstances flag says "Go ahead and use an instance, even if another instance might become relevant if you were to specialise or inline the enclosing function." The GHC user manual gives a more precise spec [1].
Now consider this class D a b where { opD :: a -> b -> String } instance D Int b where ... instance D a Int where ...
g (x::Int) = opD x x
Here 'g' gives rise to a constraint (D Int Int), and that matches two instance declarations. So this is rejected regardless of flags. We can fix it up by adding instance D Int Int where ... but this is pretty tiresome in cases where it really doesn't matter which instance you choose. (And I have a use-case where it's more than tiresome [2].)
The underlying issue is similar to the previous example. Before, there was *potentially* more than one way to generate evidence for (C [b]); here there is *actually* more than one instance. In both cases the dynamic semantics of the language are potentially affected by the choice -- but -XIncoherentInstnaces says "I don't care".
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.
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-extension... [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Hi, Am Montag, den 29.07.2013, 16:19 +0100 schrieb John Lato:
+1 to the original proposal and Edward's suggestion of emitting a warning. I've occasionally wanted this behavior from IncoherentInstances as well.
+1 for the proposal, -1 for the warning: It is a feature, not a bug, at least there where I need it (newtype casting), and then having warnings would be confusing. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org

Dear Simon,
On Jul 27, 2013, at 22:16 , Simon Peyton-Jones
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-extension... [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Axel Simon
writes:
...
In recent years I acquired the view that type inferences should have some sort of semantic completeness property ...
If you want 'semantic completeness', don't use IncoherentInstances. (As several have said, it's not a popular extension; more of a 'necessary evil' to use with caution. That's why it's a good suggestion to limit it's 'reach' to particular instances.) The price to pay for avoiding IncoherentInstances might be: - adding extra instances to avoid partial overlap - adding type annotations - 'helper' classes to resolve type-ambivalent instances (see Oleg's work for examples of these) - fancy uses of FunDeps - ultimately, programs that fail to compile
... With "semantic completeness" I mean "the best possible type that that can be expressed by the type language". ...
If there is a (unique) 'best possible type', then you don't need IncoherentInstances, IMO. AntC

On Jul 30, 2013, at 12:18 , AntC
Axel Simon
writes: ...
In recent years I acquired the view that type inferences should have some sort of semantic completeness property ...
If you want 'semantic completeness', don't use IncoherentInstances.
This is saying that any non-sensical language extension should be added to ghc since people don't have to use them. I'm trying to say what I don't like about this particular extension.
(As several have said, it's not a popular extension; more of a 'necessary evil' to use with caution. That's why it's a good suggestion to limit it's 'reach' to particular instances.)
Types and, in particular class instances, creep into many places. It will be quite difficult to limit the "reach". Adding a module to a project that declares a new instance can change the behavior of the whole program. That is bad enough, but we shouldn't willingly extend these unfortunate effects to language extensions.
The price to pay for avoiding IncoherentInstances might be: - adding extra instances to avoid partial overlap - adding type annotations
I'm just wondering if those few use-cases where they are useful can be dealt with by ensuring that the AST of the instance declarations are identical. Then this would address my concern and those of the proponents of the proposal. Cheers, Axel

Good morning, Am Samstag, den 27.07.2013, 20:16 +0000 schrieb Simon Peyton-Jones:
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.
I believe it would be more consistent to change the otherwise part of (d) to “Otherwise, if all but at most one remaining candidates were compiled with -XInccoherentInstances, pick the one that does not have the flag, or any other”. The rationale is that it goes much better with (c): Consider a typical example for (c): class C a b where foo :: (a,b) instance C [a] b instance [incoherent] [Int] b instance [incoherent] C a Int now foo :: ([a],b]) works (only one instance matches, the others unify, but are incoherent. So I can write (foo :: ([a],b])) :: ([Int], Int]). But I cannot write foo :: ([Int], Int]) as now all three instances from above match. The second is ruled out in step (b), but the third is not, so we are in case (d) and by the original logic, things fail here. If we allow one non-incoherent instance (and, for consistency with (b), pick that), it would work. I’ll prepare the patch in that variant, but of course I’ll change it if it turns out I am wrong here. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org

Yes that makes sense to me. Please do document the reasoning of this thread (and the example you give) in a "Note [Incoherent instances]" somewhere though! S | -----Original Message----- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Joachim Breitner | Sent: 19 August 2013 09:07 | To: glasgow-haskell-users@haskell.org | Subject: Re: Liberalising IncoherentInstances | | Good morning, | | Am Samstag, den 27.07.2013, 20:16 +0000 schrieb Simon Peyton-Jones: | > 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. | | I believe it would be more consistent to change the otherwise part of | (d) to “Otherwise, if all but at most one remaining candidates were | compiled with -XInccoherentInstances, pick the one that does not have | the flag, or any other”. The rationale is that it goes much better with | (c): | | Consider a typical example for (c): | | class C a b where foo :: (a,b) | instance C [a] b | instance [incoherent] [Int] b | instance [incoherent] C a Int | | now | foo :: ([a],b]) | works (only one instance matches, the others unify, but are incoherent. | So I can write | (foo :: ([a],b])) :: ([Int], Int]). | But I cannot write | foo :: ([Int], Int]) | as now all three instances from above match. The second is ruled out in | step (b), but the third is not, so we are in case (d) and by the | original logic, things fail here. | | If we allow one non-incoherent instance (and, for consistency with (b), | pick that), it would work. | | I’ll prepare the patch in that variant, but of course I’ll change it if | it turns out I am wrong here. | | Greetings, | Joachim | | | | | -- | Joachim “nomeata” Breitner | mail@joachim-breitner.de • http://www.joachim-breitner.de/ | Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C | Debian Developer: nomeata@debian.org

Hi, Am Montag, den 19.08.2013, 08:27 +0000 schrieb Simon Peyton-Jones:
Yes that makes sense to me. Please do document the reasoning of this thread (and the example you give) in a "Note [Incoherent instances]" somewhere though!
done, patches ready for review and merge at https://github.com/nomeata/ghc/compare/liberalisingIncoherent and https://github.com/nomeata/ghc-testsuite/compare/liberalisingIncoherent (should I post patches only in trac, or only here on the list, or both?) Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org
participants (7)
-
Aleksey Khudyakov
-
AntC
-
Axel Simon
-
Edward Kmett
-
Joachim Breitner
-
John Lato
-
Simon Peyton-Jones