From intuition we know that the type annotation for `foo4` is "to general",

I am making a toy compiler for a polymorphic lambda calculus working of Stephen Diehls excellent Write You a Haskell [1]. I would like to add explicit type annotations to the language, eg. type signatures for functions, but yesterday stumbled over a nut I still haven't been able to crack. The problem is with the semantics of programmer specified type annotations, type variables contained in those signatures and how they interact with the type checker. First off, the WYAH type inference algorithm is a text-book implementation of Hindley-Milner algorithm. It is designed to take a program without any explicit type information, and if type checking succeeds, it outputs the types of every part of the AST. This works fine, the issue surfaced when I added explicit type annotations to the AST. Lets say I have the function: foo1 :: a -> a foo1 x = x The inferred type of `foo1` is `foo1 :: t -> t`, when unified with the annotated type, `a -> a`, the substitution [t = a] is found. Everything works out, as it should. Now consider: foo2 :: Int -> Int foo2 x = x The inferred type of `foo2` is `foo2 :: t -> t` when unified with the annotated type, `Int -> Int`, a substitution [t = Int] is found. Everything works out, as it should. Lastly consider: foo3 :: a -> Int foo3 x = x The inferred type of `foo3` is, again, `foo3 :: t -> t`, when unified with the annotated type, `a -> Int`, we find that `t` must have the same type as `a`, and `t` must be of type `Int`, thus `t = a = Int`. Everything works out!? This is of course not intended behavior, the type annotation on foo3 is horribly wrong, and is blatantly lying about the actual type of the function. When I found this my first instinct was to check how the Haskell compiler would check this function. I found that Haskell complains: Couldn't match expected type `a' with actual type `Int' `a' is a rigid type variable bound by the type signature for foo3 :: a -> Int at foo3.hs:1:9 As far as I understand, Haskell has the notion of a rigid type variable, which my compiler is missing, I am also guessing that these rigid type variables have different rules with respect to unification? Where can I read more about these strange things? I have been trying to form the rules for unification from my intuition about Haskell type checking, but still haven't grasped the whole story, eg. how does one decide if the rigid type variable can be "specialized" or not. In `foo2` it is ok to specialize `a` into `Int`, but in `foo3`, this is not ok. I am struggling to see the underlying rules for this, and would gladly appreciate any pointers to enlightenment! Bonus question! Given the function: foo4 :: a -> a foo4 x = -(x :: Int) The inferred type of `foo4` is `foo4 :: Int -> Int`. When unified with the annotated type, `a -> a`, the substitution [a = Int] is found, everything checks out! that is, `generalness(Int -> Int) < generalness(a -> a)`, but how does one actually express that in code? That is, what is the algorithm that lies behind the function `generalness`? [1] http://dev.stephendiehl.com/fun/