Does Scala guarantee coherence in the presence of implicits?

Question

The article Type classes: confluence, coherence and global uniqueness makes the following points -

[Coherence] states that every different valid typing derivation of a program leads to a resulting program that has the same dynamic semantics.

[..]

So, what is it that people often refer to when they compare Scala type classes to Haskell type classes? I am going to refer to this as global uniqueness of instances, defining to say: in a fully compiled program, for any type, there is at most one instance resolution for a given type class. Languages with local type class instances such as Scala generally do not have this property, but in Haskell, we find this property is a very convenient one when building abstractions like sets.

If you look at this paper on Modular implicits, it states -

[..] Scala’s coherence can rely on the weaker property of non-ambiguity instead of canonicity. This means that you can define multiple implicit objects of type Showable[Int] in your program without causing an error. Instead, Scala issues an error if the resolution of an implicit parameter is ambiguous. For example, if two implicit objects of type Showable[Int] are in scope when show is applied to an Int then the compiler will report an ambiguity error.

Both of these give the impression that Scala does ensure coherence but does not ensure global uniqueness of instances.

However, if you look at Martin Odersky's comments (1, 2), it seems that the term coherence is being used as shorthand for "uniqueness of instances", which would explain the terms "local coherence" and "global coherence".

Is this just an unfortunate case of the same term being used to mean two different things? They're certainly distinct -- OCaml's modular implicits ensure coherence (as per the first definition) but not global uniqueness of instances.
Does Scala guarantee coherence (as per the first definition) in the presence of implicits?

Alec Alec · Accepted Answer · 2019-03-02T17:58:28

I think they mean the same thing in this case. Coherence is only put into question when you have more than one way of deriving the instance/implicit value; "every different valid typing derivation" is only interesting when there is more than once typing derivation. Both Scala and Haskell disallow at compile time instances which might lead to ambiguous derivations.

Scala

Odersky's comment says it for Scala: there is only ever one local way of resolving instances. In other words, there is only one valid local typing derivation. Trivially enough, it is coherent with itself. It isn't clear to me that it even makes sense to to talk about global coherence in Scala but, if it does, Scala definitely doesn't have it:

object Object1 {
  implicit val i: Int  = 9
  println(implicitly[Int])    // valid typing derivation of `Int` => printing 9
}
object Object2 {
  implicit val i: Int  = 10
  println(implicitly[Int])    // valid typing derivation of `Int` => printing 10
}

Haskell

Since Haskell instances are global, there is no point in distinguishing local/global coherence.

Haskell disallows at compile time having two instances where either instance head overlaps with the other. This turns finding type derivations into an unambiguous non-backtracking search problem. The non-ambiguity is again what gets us coherence.

Interestingly enough, GHC allows you to loosen this requirement with -XIncoherentInstances allowing you to write locally non-confluent instances, potentially breaking global coherence too.

Does Scala guarantee coherence in the presence of implicits?

1 Answers

Scala

Haskell