Simon Peyton-Jones | 27 Jul 22:16 2013
Picon

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 ...
(Continue reading)

AntC | 29 Jul 03:33 2013
Picon

Re: Liberalising IncoherentInstances

> Simon Peyton-Jones <simonpj <at> microsoft.com> 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 
(Continue reading)

AntC | 29 Jul 08:35 2013
Picon

Re: Liberalising IncoherentInstances

> AntC <anthony_clayden <at> clear.net.nz> 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!
Aleksey Khudyakov | 29 Jul 10:20 2013
Picon

Re: Liberalising IncoherentInstances

> 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.
Edward Kmett | 29 Jul 16:01 2013
Picon

Re: Liberalising IncoherentInstances

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 <simonpj <at> microsoft.com> 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-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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
John Lato | 29 Jul 17:19 2013
Picon

Re: Liberalising IncoherentInstances

+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 <ekmett <at> gmail.com> wrote:
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 <simonpj <at> microsoft.com> 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-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


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 29 Jul 23:46 2013
Picon

Re: Liberalising IncoherentInstances

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 <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Axel Simon | 30 Jul 08:45 2013
Picon

Re: Liberalising IncoherentInstances

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
AntC | 30 Jul 12:18 2013
Picon

Re: Liberalising IncoherentInstances

> Axel Simon <Axel.Simon <at> in.tum.de> 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
Axel Simon | 30 Jul 13:04 2013
Picon

Re: Liberalising IncoherentInstances


On Jul 30, 2013, at 12:18 , AntC <anthony_clayden <at> clear.net.nz> wrote:

>> Axel Simon <Axel.Simon <at> in.tum.de> 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
Joachim Breitner | 19 Aug 10:07 2013
Picon

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 <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 19 Aug 10:27 2013
Picon

RE: Liberalising IncoherentInstances

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 <at> haskell.org] On Behalf Of Joachim Breitner
| Sent: 19 August 2013 09:07
| To: glasgow-haskell-users <at> 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 <at> joachim-breitner.de • http://www.joachim-breitner.de/

|   Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
|   Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 19 Aug 10:59 2013
Picon

Re: Liberalising IncoherentInstances

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 <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane