CODEWITHSUNDEEP
haskelltype-inferenceambiguous-types
Wheat Wizard
Wheat Wizard

Reputation: 4219

What is causing this type ambiguity?

I have two relatively simple classes, MSet:

{-# Langage MultiParamTypeClasses #-}

-- A generalization of G set to Magmas
class MSet a b where
  (+>>) :: a -> b -> a

instance MSet Integer Integer where
  (+>>) = (+)

-- (+>>) constrained to a Magma
(<<+>>) ::
  ( MSet a a
  )
    => a -> a -> a
(<<+>>) = (+>>)

When I boot into ghci and try and test these I have an issue:

*Main> 1 <<+>> 2
3
*Main> 1 +>> 2

<interactive>:31:1: error:
    • Could not deduce (MSet a b0)
      from the context: (MSet a b, Num a, Num b)
        bound by the inferred type for ‘it’:
                   forall a b. (MSet a b, Num a, Num b) => a
        at <interactive>:31:1-7
      The type variable ‘b0’ is ambiguous
    • In the ambiguity check for the inferred type for ‘it’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the inferred type
        it :: forall a b. (MSet a b, Num a, Num b) => a

While (+>>) works when it is constrained to a Magma but is ambiguous when it is not.

Now I can do:

*Main> :set -XFlexibleContexts
*Main> 1 +>> (2 :: Integer)
3

But I don't understand what is going on here or why this annotation helps. I don't really get how the type checker disambiguates (<<+>>). If I add another instance, say Int, it continues to function even though it seems to be it should be ambiguous whether 1 is an Int or an Integer.

Why does one of these error and why do the other two not?

Upvotes: 4

Views: 207

Answers (1)

Isaac van Bakel
Isaac van Bakel

Reputation: 1852

Essentially - you are asking GHC to solve "what is the type of 1 and 2 in the expression 1 +>> 2, and your typeclasses mean that the answer is ambiguous.

In depth

<<+>>

What is the type of 1 <<+>> 2? Why, (Num a, MSet a a) => a of course, because GHC has to be able to turn the literals into values (Num) and then +>> them (MSet), and the type signature of <<+>> says that both literals will have the same type.

What happens when you ask GHCi to print the value of 1 <<+>> 2? It tries to default a to Integer, which succeeds because Num Integer and MSet Integer Integer. It then evaluates the type-defaulted expression.

This is the reason the Int instance doesn't introduce ambiguity - GHCi isn't trying to infer the specific instance to use, it instead infers the type and then defaults the variables, leaving only the instance check.

+>>

What is the type of 1 +>> 2? Well... (Num a, Num b, MSet a b) => a, it seems like. Clearly you need MSet, but there's no longer an assurance that a and b unify. More unfortunately, b does not appear in the type of the term - which is the source of the type ambiguity. The type system doesn't know which choice of b to use.

What happens when you ask GHCi to print the value of 1 +>> 2? It first infers the type of the term, and gets the above type - and now it hits a type inference error before it can try to default a to Integer.

Why do the fixes work?

Adding type information will prevent the error

> 1 +>> (2 :: Integer) -- fine

because these changes eliminate the ambiguity of b. GHC doesn't need to infer b, so it doesn't get raise an inference error.

Weirdly, and I don't fully understand the reason for it, adding the annotation for a also seems to prevent the error

> (1 :: Integer) +>> 2 -- fine
> (1 +>> 2) :: Integer -- fine

though I suspect that's another GHCi-specific trick that's defaulting b to Integer in (1 +>>) :: (Num b, MSet Integer b) => b -> Integer. Don't quote me on that, though.

With fundeps

It is possible to eliminate the type ambiguity using FunctionalDependencies

class MSet a b | a -> b where
  ...

though that doesn't seem like it fits your use case. This solves the inference problem because in (Num a, Num b, MSet a b) => a, knowing a will be enough to deduce b from the fundep in MSet. Later, when GHCi defaults a to Integer, it can just look up the type of b.

Upvotes: 1

Related Questions