Polymorphic pattern matching results in ambiguous type

Question

(Inspired by cannot match on polymorphic tuples with constraints, and based on a subsequent comment on my own answer.)

Consider the following minimal example:

test :: (Show a, Show b) => (a -> String, b -> String)
test = (show,show)

(resX, resY) = test

This results in the following error:

    • Ambiguous type variable ‘a0’ arising from a use of ‘test’
      prevents the constraint ‘(Show a0)’ from being solved.
      Relevant bindings include
        resX :: a0 -> String (bound at so.hs:25:2)
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance Show Ordering -- Defined in ‘GHC.Show’
        instance Show Integer -- Defined in ‘GHC.Show’
        instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
        ...plus 22 others
        ...plus 17 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: test
      In a pattern binding: (resX, resY) = test
   |
25 | (resX, resY) = test
   |                ^^^^

This makes sense: that pattern match doesn’t constrain a or b in any way, so they’re ambiguous. But how do I get rid of this error? Just about every attempt to solve this by adding type signature(s) gives another error. For instance:

-- attempt 1
test :: (Show a, Show b) => (a -> String, b -> String)
test = (show,show)

resX :: Show a => a -> String
resY :: Show b => b -> String
(resX, resY) = test

-- attempt 2
test :: (Show a, Show b) => (a -> String, b -> String)
test = (show,show)

(resX, resY) = test :: (Show a, Show b) => (a -> String, b -> String)

So: how can I get rid of the ambiguity error? And why do the above attempts fail?

Answer 1

This makes sense: that pattern match doesn’t constrain a or b in any way, so they’re ambiguous. But how do I get rid of this error?

Giving type signatures will not help here. The type for test is (Show a, Show b) => (a -> String, b -> String). Basically what you do is write:

resX :: Show a => a -> String
resX = fst test

The question is however, what should Haskell fill in for b from the signature of test? You might say that this does not matter, and here it indeed does not matter. But if you defined test through a typeclass for example. The a and b type could determine together what the implementation for the first item would be. For example:

{-# LANGUAGE MultiParamTypeClasses #-}

class (Show a, Show b) => SomeTest a b where
    test :: (a -> String, b -> String)

instance SomeTest Bool Bool where
    test = (const "foo", const "bar")

instance SomeTest Bool Int where
    test = (const "qux", const "bar")

here the second type parameter determines the implementation of the first item of test, and hence we can not just omit that.

You can for example use the TypeApplications extension, to provide a type for the other type parameter (here Bool):

{-# LANGUAGE TypeApplications -#}

test :: (Show a, Show b) => (a -> String, b -> String)
test = (show, show)

resX :: Show a => a -> String
resX = fst (test @_ @Bool)

resY :: Show a => a -> String
resY = snd (test @Bool)

Answer 2

It's instructive to think about how your code actually works at runtime. Type classes have dictionary passing semantics. Classy code

class Foo a where
    foo :: a -> Int

instance Foo Int where
    foo = id

useFoo :: Foo a => a -> IO ()
useFoo x = print (foo x)

callFoo = useFoo (123 :: Int)

is compiled into non-classy code.

data Foo_ a = Foo_ { foo :: a -> Int }

foo_Int :: Foo_ Int
foo_Int = Foo_ { foo = id }

useFoo :: Foo_ a -> a -> IO ()
useFoo dict x = print (foo dict x)

callFoo = useFoo foo_Int 123

The "fat arrow" => really means exactly the same thing at runtime as the "scrawny arrow" ->. The only difference is that =>'s argument is passed implicitly by the constraint solver.

So let's think about your Show example from this perspective. A type like test :: (Show a, Show b) => (a -> String, b -> String) really means test :: (Show_ a, Show_ b) -> (a, String, b -> String). You can't factorise that function into a pair of functions (Show_ a -> a -> String, Show_ b -> b -> String). The body of the function might make use of both Show_ dictionaries before returning a result, so you have to supply both before you can get the (a -> String, b -> String) out.

When inferring a type for resx, the type checker will come up with resx :: (Show a, Show b) => a -> String — it needs both instances in scope in order to call test. Clearly this is an ambiguous type. b doesn't appear to the right of the =>, so at resx's call site there will never be enough local type information to call it successfully.

You might object that one should be able to carry out such a factorisation in this case. The two halves of test's body can't use each others' Show instances, because Show's methods only talk about their type parameter as an input and the input is not in scope in the wrong half of the tuple. But that's a sophisticated argument from parametricity about runtime behaviour, and it only holds for this specific case. It's not the sort of dumb syntax-directed reasoning a compiler is good at.