Type inference in GHCi vs. manual signature

Question

when I type

:t map length . sum

into GHCi, it says that the type would be:

map length . sum :: Num [[a]] => [[[a]]] -> [Int]

However, if I create a file type-test.hs containing

x :: Num [[a]] => [[[a]]] -> [Int]
x = map length . sum

both ghc and ghci complain:

type-test.hs:1:1:
    Non type-variable argument in the constraint: Num [[a]]
    (Use -XFlexibleContexts to permit this)
    In the type signature for `x': x :: Num [[a]] => [[[a]]] -> [Int]

Why does ghci allow me to infer the type for this (using :t), when FlexibleContexts are not enabled?

Answer 1

First, let's clarify one thing. What happens if we define the function in GHCi, rather than querying the type?

> let x = map length . sum :: (Num [[a]]) => [[[a]]] -> [Int]
<interactive>:0:9:
    Non type-variable argument in the constraint: Num [[a]]
    (Use -XFlexibleContexts to permit this)
    In an expression type signature: Num [[a]] => [[[a]]] -> [Int]

And so on. In other words, the same thing. What if we let GHCi infer the type of the definition?

> let x = map length . sum
<interactive>:0:22:
    No instance for (Num [[a0]])
      arising from a use of `sum'
    Possible fix: add an instance declaration for (Num [[a0]])
    In the second argument of `(.)', namely `sum'
    In the expression: map length . sum

This is roughly the same error that results from loading a file containing the definition without a type signature.

What's the upshot of all this? Well, think about the fact that it tells you what extension is needed. GHC is capable of recognizing what the type means, even if it rejects the type by default. I'd hardly expect GHC to use a completely different type checker depending on the combination of extensions used, so it seems easy to conclude that the offending type is being rejected for no reason other than the relevant extension being disabled.

The :t command in GHCi isn't part of the compilation process--it's a hotline to the type checking and inference system, letting you ask the type of hypothetical code. There's no obvious reason for it to restrict itself arbitrarily based on extensions, when a more general type could still be informative, for the same reason that the error messages above tell you use -XFlexibleContexts to permit this rather than merely syntax error in type constraint.

---

As a possibly more interesting aside, there are also cases where an inferred type will be accepted happily by the compiler, but the inferred type can't actually be written out explicitly for one of several reasons.

For instance, disabling the monomorphism restriction will allow your example to have its type inferred (matching what :t says), despite that type requiring an extension to write manually.

Another example are definitions in the where clause of a function definition which make use of polymorphic arguments to the parent function. Their own types are not polymorphic, being dictated by the arguments received in the outer scope, yet the type variables in the parent function's signature are not in scope for the where clause¹. There may be other examples as well.

¹ The type variables from the parent's signature can be brought into scope with the ScopedTypeVariables extension and an explicit forall, if that's needed.