Transferring from https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html Second instalment. On Sat, 13 Oct 2018 at 4:04 AM, wrote:

... Ambiguity should be a property of an expression, defined as follows: if a constraint set C on the constrained type C∪D⇒t of an expression has unreachable variables, then satisfiability is tested for C (a definition of reachable and unreachable type variables is at the end of this message), and:

- if there is a single unifying substitution of C with the set of instances in the current context (module), then C can be removed (overloading is resolved) and C∪D⇒t 'improved' to D⇒t;

- otherwise there is a type error: ambiguity if there are two or more unifying substitutions of C with the set of instances in the current context (module), and unsatisfiability otherwise.

2. Allow instances to be imported (all instances are assumed to be exported):

import M (instance A τ₁ ⋯ τₙ , … )

specifies that the instance of τ₁ ⋯ τₙ for class A is imported from M, in the module where the import clause occurs.

In case of no explicit importation, all instances remain imported, as currently in Haskell (in order that well-typed programs remain well-typed).

Consider some typical Read instances from the Haskell Prelude

instance Read a => Read [a] where ... instance Read a => Read (Maybe a) where ...

Suppose I have `show . read` where the 'piggy in the middle' type is unreachable (by your definition below); but I want it to be taken as `(Maybe [Int])`. Then I arrange my imports of instances to make visible only ... what? `(Maybe a)` ? Then how do I read the `[a]`? The only instance in scope is `(Maybe a)`. `(Maybe [Int])` ? Then how do I decompose the structure to call the overloads for `read` of the list and of the `Int`? Instance `(Maybe a)` is not in scope, neither is `[a]` nor `Int`. And what if in the same module/same scope I want `show . read` where 'piggy in the middle' is `[Maybe Int]` or `(Maybe [Bool])` ? Then instead of `Read`, I could create a whole swag of specialised classes/methods: ReadMaybeListInt, ReadListMaybeInt, ReadMaybeListBool, ... ? But those could just be regular functions with an explicit signature. Putting an explicit type annotation on each expression seems a whole lot more convenient than mucking around with specialised classes or scope of instances. Before you answer, consider this very common pattern. It's so common there's a base library operator for it: type-level `==` https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base-4.12.0.0/...; but the technique dates back to 2004/the HList paper at least:

class TypeEq a a' (b :: Bool) | a a' -> b instance TypeEq a a True instance (b ~ False) => TypeEq a a' b

Then an example usage

instance (TypeEq e e' b, TypeIf b This That) => instance Elem e (Cons e' tail) where ...

Rubric: `Elem` is searching for type `e` in some type-level heterogeneous list; if found (i.e. `TypeEq` returns `True`), the `TypeIf` despatches to `This`, else to `That`. It's crucial for `TypeEq` that both instances are in scope in all places. Ah, but I see the `TypeEq` example does not contain any "unreachable" tyvars by your definition below. In which case your specification is silent as to how type improvement is to behave. (But you claim your approach is instead of FunDeps; then what is to happen with both instances being able to unify with the type of some expression?) Then do you want to change the spec? This was the experience with the github rounds: the spec kept changing; the examples we'd worked through in earlier rounds then didn't work with the new spec. Therefore the claims were impossible to verify with any certainty.

(Definition: [Reachable and unreachable type variables in constraints] Consider a constrainted type C∪D⇒τ. A variable a ∈ tv(C) is reachable from V = tv(τ) if a ∈ V or if a ∈ tv(π) for some π ∈ C such that there exists b ∈ tv(π) such that b is reachable from V; otherwise it is unreachable. For example, in (F a b, X a) ⇒ b, type variable 'a' is reachable from { b }, because 'a' occurs in constraint F a b, and b is reachable. Similarly, if C = (F a b, G b c, X c), then c is reachable from {a}.)

AntC