[Haskell-cafe] Rigid type variables and their role in type checking

[Morten Olsen Lysgaard]

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!
>From intuition we know that the type annotation for `foo4` is "to general",
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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160824/de3a7daf/attachment.html>