Effects of monomorphism restriction on type class constraints

Question

This code breaks when a type declaration for baz is added:

baz (x:y:_) = x == y
baz [_] = baz []
baz [] = False

A common explanation (see Why can't I declare the inferred type? for an example) is that it's because of polymorphic recursion.

But that explanation doesn't explain why the effect disappears with another polymorphically recursive example:

foo f (x:y:_) = f x y
foo f [_] = foo f []
foo f [] = False

It also doesn't explain why GHC thinks the recursion is monomorphic without type declaration.

Can the explanation of the example with reads in http://www.haskell.org/onlinereport/decls.html#sect4.5.5 be applied to my baz case?

I.e. adding a signature removes monomorphism restriction, and without the restriction an ambiguity of right-side [] appears, with an 'inherently ambigous' type of forall a . Eq a => [a]?

Amann

Answer 1

The equations for baz are in one binding group, generalisation is done after the entire group has been typed. Without a type signature, that means baz is assumed to have a monotype, so the type of [] in the recursive call is given by that (look at ghc's -ddump-simpl output). With a type signature, the compiler is explicitly told that the function is polymorphic, so it can't assume the type of [] in the recursive call to be the same, hence it's ambiguous.

As John L said, in foo, the type is fixed by the occurrence of f - as long as f has a monotype. You can create the same ambiguity by giving f the same type as (==) (which requires Rank2Types),

{-# LANGUAGE Rank2Types #-}
foo :: Eq b => (forall a. Eq a => a -> a -> Bool) -> [b] -> Bool
foo f (x:y:_) = f x y
foo f[_] = foo f []
foo _ [] = False

That gives

Ambiguous type variable `b0' in the constraint:
  (Eq b0) arising from a use of `foo'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: foo f []
In an equation for `foo': foo f [_] = foo f []

Puryear

The rank 2 version of foo is inspiring too, thank you! I start finally to grasp what shallow types are. – Amann

+1 Nice! Excuse me while I go play with my new understanding of Rank 2 types. ( ideone.com/RajuI ) – Aga

I believe this answer is missing an important point of the question: the monomorphism restriction doesn't have anything to do with the declaration of baz. The only declarations in the declaration group of baz are function bindings and hence the monomorphism restriction doesn't trigger. The fact you mention is due to the Hindley-Milner type system: you first infer assuming monomorphic types and in the end generalize. If you provide a type signature the compiler uses that type for baz in the rhs and thus the ambiguity. But nothing to do with monomorphic restriction. – Arlettearley

Answer 2

Your second example isn't polymorphically recursive. This is because the function f appears on both the LHS and RHS of the recursive definition. Also consider the type of foo, (a -> a -> Bool) -> [a] -> Bool. This fixes the list element type to be identical to the type of f's arguments. As a result, GHC can determine that the empty list on the RHS must have the same type as the input list.

I don't think that the reads example is applicable to the baz case, because GHC is able to compile baz with no type signature and the monomorphism restriction disabled. Therefore I expect that GHC's type algorithm has some other mechanism by which it removes the ambiguity.

Holmann

+1 for 'This fixes the list element type to be identical to the type of f's arguments' – Amann

@DanielFischer +100500 for 'generalisation is done after the entire group has been typed'. Can you put your comment as an answer? – Amann