How can Haskell integer literals be comparable without being in the Eq class?

Question

In Haskell (at least with GHC v8.8.4), being in the Num class does NOT imply being in the Eq class:

$ ghci
 GHCi, version 8.8.4: https://www.haskell.org/ghc/  :? for help
 λ> 
 λ> let { myEqualP :: Num a => a -> a -> Bool ; myEqualP x y = x==y ; }

<interactive>:6:60: error:
    • Could not deduce (Eq a) arising from a use of ‘==’
      from the context: Num a
        bound by the type signature for:
                   myEqualP :: forall a. Num a => a -> a -> Bool
        at <interactive>:6:7-41
      Possible fix:
        add (Eq a) to the context of
          the type signature for:
            myEqualP :: forall a. Num a => a -> a -> Bool
    • In the expression: x == y
      In an equation for ‘myEqualP’: myEqualP x y = x == y
 λ> 

It seems this is because for example Num instances can be defined for some functional types.

Furthermore, if we prevent ghci from overguessing the type of integer literals, they have just the Num type constraint:

 λ> 
 λ> :set -XNoMonomorphismRestriction
 λ> 
 λ> x=42
 λ> :type x
 x :: Num p => p
 λ> 

Hence, terms like x or 42 above have no reason to be comparable.

But still, they happen to be:

 λ> 
 λ> y=43
 λ> x == y
 False
 λ> 

Can somebody explain this apparent paradox?

Answer 1

Integer literals can't be compared without using Eq. But that's not what is happening, either.

In GHCi, under NoMonomorphismRestriction (which is default in GHCi nowadays; not sure about in GHC 8.8.4) x = 42 results in a variable x of type forall p :: Num p => p.¹

Then you do y = 43, which similarly results in the variable y having type forall q. Num q => q.²

Then you enter x == y, and GHCi has to evaluate in order to print True or False. That evaluation cannot be done without picking a concrete type for both p and q (which has to be the same). Each type has its own code for the definition of ==, so there's no way to run the code for == without deciding which type's code to use.³

However each of x and y can be used as any type in Num (because they have a definition that works for all of them)⁴. So we can just use (x :: Int) == y and the compiler will determine that it should use the Int definition for ==, or x == (y :: Double) to use the Double definition. We can even do this repeatedly with different types! None of these uses change the type of x or y; we're just using them each time at one of the (many) types they support.

Without the concept of defaulting, a bare x == y would just produce an Ambiguous type variable error from the compiler. The language designers thought that would be extremely common and extremely annoying with numeric literals in particular (because the literals are polymorphic, but as soon as you do any operation on them you need a concrete type). So they introduced rules that some ambiguous type variables should be defaulted to a concrete type if that allows compilation to continue.⁵

So what is actually happening when you do x == y is that the compiler is just picking Integer to use for x and y in that particular expression, because you haven't given it enough information to pin down any particular type (and because the defaulting rules apply in this situation). Integer has an Eq instance so it can use that, even though the most general types of x and y don't include the Eq constraint. Without picking something it couldn't possibly even attempt to call == (and of course the "something" it picks has to be in Eq or it still won't work).

If you turn on -Wtype-defaults (which is included in -Wall), the compiler will print a warning whenever it applies defaulting⁶, which makes the process more visible.

---

¹ The forall p part is implicit in standard Haskell, because all type variables are automatically introduced with forall at the beginning of the type expression in which they appear. You have to turn on extensions to even write the forall manually; either ExplicitForAll just for the ability to write forall, or any one of the many extensions that actually add functionality that makes forall useful to write explicitly.

---

² GHCi will probably pick p again for the type variable, rather than q. I'm just using a different one to emphasise that they're different variables.

---

³ Technically it's not each type that necessarily has a different ==, but each Eq instance. Some of those instances are polymorphic, so they apply to multiple types, but that only really comes up with types that have some structure (like Maybe a, etc). Basic types like Int, Integer, Double, Char, Bool, each have their own instance, and each of those instances has its own code for ==.

---

⁴ In the underlying system, a type like forall p. Num p => p is in fact much like a function; one that takes a Num instance for a concrete type as a parameter. To get a concrete value you have to first "apply the function" to a type's Num instance, and only then do you get an actual value that could be printed, compared with other things, etc. In standard Haskell these instance parameters are always invisibly passed around by the compiler; some extensions allow you to manipulate this process a little more directly.

This is the root of what's confusing about why x == y works when x and y are polymorphic variables. If you had to explicitly pass around the type/instance arguments it would be obvious what's going on here, because you would have to manually apply both x and y to something and compare the results.

---

⁵ The gist of the default rules is that if the constraints on an ambiguous type variable are:

1. all built-in classes
2. at least one of them is a numeric class (Num, Floating, etc)

then GHC will try Integer to see if that type checks and allows all other constraints to be resolved. If that doesn't work it will try Double, and if that doesn't work then it reports an error.

You can set the types it will try with a default declaration (the "default default" being default (Integer, Double)), but you can't customise the conditions under which it will try to default things, so changing the default types is of limited use in my experience.

GHCi however comes with extended default rules that are a bit more useful in an interpreter (because it has to do type inference line-by-line instead of on the whole module at once). You can turn those on in compiled code with ExtendedDefaultRules extension (or turn them off in GHCi with NoExtendedDefaultRules), but again, neither of those options is particularly useful in my experience. It's annoying that the interpreter and the compiler behave differently, but the fundamental difference between module-at-a-time compilation and line-at-a-time interpretation mean that switching either's default rules to work consistently with the other is even more annoying. (This is also why NoMonomorphismRestriction is in effect by default in the interpreter now; the monomorphism restriction does a decent job at achieving its goals in compiled code but is almost always wrong in interpreter sessions).

---

⁶ You can also use a typed hole in combination with the asTypeOf helper to get GHC to tell you what type it's inferring for a sub-expression like this:

λ :t x
x :: Num p => p

λ :t y
y :: Num p => p

λ (x `asTypeOf` _) == y

<interactive>:19:15: error:
    • Found hole: _ :: Integer
    • In the second argument of ‘asTypeOf’, namely ‘_’
      In the first argument of ‘(==)’, namely ‘(x `asTypeOf` _)’
      In the expression: (x `asTypeOf` _) == y
    • Relevant bindings include
        it :: Bool (bound at <interactive>:19:1)
      Valid hole fits include
        x :: forall p. Num p => p
          with x
          (defined at <interactive>:1:1)
        it :: forall p. Num p => p
          with it
          (defined at <interactive>:10:1)
        y :: forall p. Num p => p
          with y
          (defined at <interactive>:12:1)

You can see it tells us nice and simply Found hole: _ :: Integer, before proceeding with all the extra information it likes to give us about errors.

A typed hole (in its simplest form) just means writing _ in place of an expression. The compiler errors out on such an expression, but it tries to give you information about what you could use to "fill in the blank" in order to get it to compile; most helpfully, it tells you the type of something that would be valid in that position.

foo `asTypeOf` bar is an old pattern for adding a bit of type information. It returns foo but it restricts (this particular usage of) it to be the same type as bar (the actual value of bar is totally unused). So if you already have a variable d with type Double, x `asTypeOf` d will be the value of x as a Double.

Here I'm using asTypeOf "backwards"; instead of using the thing on the right to constrain the type of the thing on the left, I'm putting a hole on the right (which could have any type), but asTypeOf conveniently makes sure it's the same type as x without otherwise changing how x is used in the overall expression (so the same type inference still applies, including defaulting, which isn't always the case if you lift a small part of a larger expression out to ask GHCi for its type with :t; in particular :t x won't tell us Integer, but Num p => p).