Why does GHC infer a monomorphic type here, even with MonomorphismRestriction disabled?

Question

This was prompted by Resolving the type of `f = f (<*>) pure`, which discusses a more complicated example, but this one works too.

The following definition compiles without problem:

w :: Integral a => a
w = fromInteger w

...Of course it doesn't work runtime-wise, but that's beside the question. The point is that the definition of w itself uses a specialised version of w :: Integer. Clearly that is a suitable instantiation, and therefore typechecks.

However, if we remove the signature, then GHC infers not the above type, but only the concrete one:

w' = fromInteger w'

GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer

Well, when I saw this, I was fairly sure this was the monomorphism restriction at work. It's well known that also e.g.

i = 3

GHCi> :t i
i :: Integer

although i :: Num p => p would be perfectly possible. And indeed, i :: Num p => p is inferred if -XNoMonomorphismRestriction is active, i.e. if the monomorphism restriction is disabled.

However, in case of w' only the type Integer is inferred even when the monomorphism restriction is disabled.

To count out that this has something to do with defaulting:

fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'

GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float

Why is the polymorphic type not inferred?

Selfconceit

Doesn't the monomorphism restriction apply only to simple bindings anyways (and w' = fromInteger w', being recursive, is not simple)? – Arcadia

@Arcadia possible, but still – why does something like the monomorphism restriction seem to kick in here? – Selfconceit

I'm probably being dense and missing something here, but fromInteger has type (Num a) => Integer -> a, and since w' is used as the input to fromInteger, doesn't that mean Integer is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.) – Kronfeld

@RobinZigmond Integer is certainly the only possible monomorphic type for w', but as w demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints. – Selfconceit

Answer 1

Polymorphic recursion (where a function calls itself at a different type than the one at which it was called) always requires a type signature. The full explanation is in Section 4.4.1 of the Haskell 2010 Report:

If a variable f is defined without providing a corresponding type signature declaration, then each use of f outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type. However, to ensure that type inference is still possible, the defining occurrence, and all uses of f within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).

The same section later presents an example of polymorphic recursion supported by a type signature.

My understanding is that unaided type inference is generally undecidable in the presence of polymorphic recursion, so Haskell doesn't even try.

In this case, the type checker starts with

w :: a

where a is a meta-variable. Since fromInteger is called with w as an argument within its own declaration (and therefore within its declaration group), the type checker unifies a with Integer. There are no variables left to generalize.

A slight modification of your program gives a different result for the same reason:

v = fromIntegral v

By your original reasoning, Haskell would infer v :: forall a. Num a => a, defaulting the v on the RHS to type Integer:

v :: forall a. Num a => a
v = fromIntegral (v :: Integer)

But instead, it starts with v :: a. Since v is passed to fromIntegral, it imposes Integral a. Finally, it generalizes a. In the end, the program turns out to be

v :: forall a. Integral a => a
v = fromIntegral (v :: a)

Listel

My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up to k depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times. – Irrationality

@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code. – Listel

Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO. – Irrationality

@Bakuriu, just for my own curiosity: how much of Data.Sequence could be inferred with bounded polymorphic recursion depth? I'm not quite sure what you mean when you say "depth" in this context. – Listel

The reason there is no inference for polymorphic recursion is exactly because it’s undecidable. This is a decision from long before ghc gained a lot of other undecidable features. You can trust me on this one, I was on the Haskell committee at that point. :) – Tawnatawney

@Listel As far as I know given any well-typed polymorphic recursive program there exist a finite depth k such that the type inference works. The issue is that there is no finite k that works for every program. However, at the time, I did not consider other Haskell extensions so it could well be that if you add type families, functional dependencies and such this is not true anymore. – Irrationality

@Bakuriu, ah, I didn't realize it was semi-decidable. Interesting. – Listel