Ambiguous type variable issue in Haskell

Question

I have read many of the other ambiguous type variable questions on the site but was not able to find a solution to the following issue, although I am new to Haskell so may just not have understood the answers to other questions properly. Simplifying to only include the relevant parts of these definitions, I have a type class

class Dist a where
  un :: a

and I have a multiparameter type class

class Dist a => UnBin a b where 
  opu :: b -> b
  opb :: a -> b -> a

where in general a and b are completely unrelated. However, I also have a data type

data LC a b = LC [(a,b)]

and I make it an instance of UnBin using

instance Dist a => UnBin a (LC [(a,b)]) where
  opu = ...
  opb = ...

where in this particular case, the type LC [(a,b)] already depends on a and I want the two as here to be the same.

What I mean by the two as should be the same is that if I define x = LC [(1 :: Int,'a')] for example (assuming I have made Int a part of the Dist typeclass already) then I would want to be able to just write opb un x and have Haskell automatically infer that I want un :: Int since a is already determined by the type of x however unless I explicitly use a type signature for un and write opb (un::Int) x I get the error

Ambiguous type variable ‘a0’ arising from a use of ‘un’
      prevents the constraint ‘(Dist a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instance exist:
        one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)

Presumably this means that Haskell is treating the two as in my instance declaration as unrelated when I want them to really be the same. Is there a way to make Haskell automatically able to infer the correct type of un without having to give a type signature every time I want to use un in this way?

Answer 1

Presumably this means that Haskell is treating the two as in my instance declaration as unrelated when I want them to really be the same.

Actually, GHC does know that the two as in the instance you wrote are the same. However, it doesn't know that it should use that instance. The problem is that there could be another instance out there. For instance, for all GHC knows, you've also written the instance:

instance UnBin Char (LC Int b) where
  opu = ...
  opb = ...

Then, there are two different types that the un in opb un x could be. It really is ambiguous!

But, you might say, I didn't write any other instance. That may be true, but instances are sneaky. If someone imports your code and then creates an orphan instance like the one I wrote above, what should happen? That value opb un x needs to be the same, but with this new instance in scope, it would also need to change. GHC doesn't like this future possibility, so it gives you an error.

You mentioned in your question that "in general a and b are completely unrelated". Hopefully it's the case that a given b implies a given a. If not, or in other words, if you want to be able to write instances like UnBin Char (LC Int b) like I did above, then you're out of luck. You can't have it both ways: you can't have GHC infer the type you want while also keeping the freedom to decide for yourself whatever type you want.

However, if it is true that a and b are related (in that, say, b can imply a), then there are a few ways forward. For instance, as shown by @chi, you can use a type equality in the instance context to trick GHC into matching on the instance you want first and only verifying that the types are the same later. Another option is to use type families or functional dependencies to achieve a similar goal. For instance:

{-# LANGUAGE FunctionalDependencies #-}

class Dist a => UnBin a b | b -> a where

Note that in either case, you're limiting the total number of instances you can write. In the type equality approach, you have generalized your instance head, and with the functional dependency approach, you force b to imply a. Hopefully, that's okay with you.

Answer 2

Fully working example:

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE GADTs                 #-}

class Dist a where
  un :: a

instance Dist Int where
  un = 42

class Dist a => UnBin a b where 
  opu :: b -> b
  opb :: a -> b -> a

data LC a b = LC [(a,b)]

instance (Dist a, a ~ a') => UnBin a (LC a' b) where
  opu = undefined
  opb = undefined

x = LC [(1 :: Int,'a')]

test = opb un x   -- here GHC infers un::Int as wanted

The main technique is this: instead of writing

instance Dist a => UnBin a (LC a b) where

we write

instance (Dist a, a ~ a') => UnBin a (LC a' b) where

so that the instance head UnBin a (LC a' b) matches even when types a and a' are not the same. Then, we require in the instance context a ~ a' forcing them to be the same.

In this way, the instance is picked during inference at a time where we don't yet know how a and a' are related. After this happens, GHC immediately deduces a~a' and exploits it to infer the type Int for un in test = opb un x.