Implementing instance methods with ambiguous type variables not contained in the class head

Question

Say I have two classes like this:

{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes, FlexibleContexts #-}
class Foo a b

class Bar a where
  foo :: Foo a b => a

Notably, the b of foo can neither be inferred from the use of foo nor from the instance head. Now let's try to implement an instance for this:

data A = A

-- This implementation doesn't actually need the Foo A b constraint, but for the sake of the question it's required here.
a :: Foo A b => A
a = A

So far so good. a is supposed to become the foo in our instance. It even has the right type, right? So let's go ahead and implement the instance:

instance Bar A where
  foo = a

Unfortunately this instance doesn't compile and gives this error instead:

instance-ambiguous.hs:15:9: error: …
    • Could not deduce (Foo A b0) arising from a use of ‘a’
      from the context: Foo A b
        bound by the type signature for:
                   foo :: forall b. Foo A b => A
        at /home/sven/instance-ambiguous.hs:15:3-5
      The type variable ‘b0’ is ambiguous
    • In the expression: a
      In an equation for ‘foo’: foo = a
      In the instance declaration for ‘Bar A’
   |
Compilation failed.

At first this error message seems quite nonsensical, because it looks like GHC could just unify b and b0 and infer a perfectly fine type. Then I remembered that b and b0 aren't visible from the type of foo or a and GHC can't unify them, because it has nothing that guarantees that b and b0 are really always exactly the same and this is not such an unexpected error when working with ambiguous types.

Normally when I encounter such errors, I'm able to solve them using TypeApplications and ScopedTypeVariables like this:

{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes, FlexibleContexts, TypeApplications, ScopedTypeVariables #-}

class Foo a b

class Bar b

foo :: forall b a. (Bar b, Foo a b) => a
foo = undefined

bar :: forall b a. (Bar b, Foo a b) => a
bar = foo @b

Here I can explicitly supply the @b, because the type signature of bar brought it in scope. So I tried to do the same with my instance (using InstanceSigs):

instance Bar A where
  foo :: forall b. Foo A b => A
  foo = a @b

This doesn't compile either and gives this error:

instance-ambiguous.hs:16:10-31: error: …
    • Could not deduce (Foo A b0)
      from the context: Foo A b
        bound by the type signature for:
                   foo :: forall b. Foo A b => A
        at /home/sven/instance-ambiguous.hs:16:10-31
      The type variable ‘b0’ is ambiguous
    • When checking that instance signature for ‘foo’
        is more general than its signature in the class
        Instance sig: forall b. Foo A b => A
           Class sig: forall b. Foo A b => A
      In the instance declaration for ‘Bar A’
   |
Compilation failed.

I'm not sure, but I think this means that GHC thinks that my Foo A b => A in the instance refers to some other b than the one in the class declaration.

Using a pattern declaration on foo to get the original b in scope also doesn't work, because Pattern bindings are forbidden in instance declarations.

Now the question: What are my options to work around this problem?

I know that I can just use Proxy(s/y/ie/)s everywhere and hear none of those ambiguity problems, but I usually find TypeApplications more elegant than Proxys and would like to use them here, especially because the affected classes are part of my public API.

I could also include the b as a class variable of Bar, but I think that would change the meaning of Bar to something that I don't want, because then instances can choose which bs to implement instances for, but I want every Bar a => a to work for every b for which an Foo a b exists.

Answer 1

There doesn't seem to be a way to resolve the ambiguity for instances, so a Proxy or Tagged seems inevitable to define the class, but you can wrap it to use the class with TypeApplications.

class Bar a where
  foo_ :: Foo a b => proxy b -> a

foo :: forall b a. (Bar a, Foo a b) => a
foo = foo_ (Proxy @b)