Fix let inference (attempts to fix #72 and #82).

[VitorCBSB]

Attempts to fix issues #72 and #82 regarding let polymorphism. Inference works correctly for the functions provided in them and they have been added to the test.ml file. Big thanks to @Azure-Vani for the pointer to his / her implementation as well as providing the algorithm described in TAPL.

For this fix, I had to radically change the infer function's interface, and alter the Infer monad to being a simple State + Reader + Except instead of RWS (the Writer part was not being used). This might not be good for readability, but it's the solution I could come up with.

Additionally, this is going to need to be reflected in the text, but I'm not confident enough to submit changes to it.

[sdiehl]

I'll take a look at this.

[lexi-lambda]

I am certainly no expert, so take this comment with a grain of salt, but I took a glance at this, and it looks right to me. I think it might be possible to implement it more nicely, though, by keeping the use of RWS and using listen from MonadWriter instead of manually threading the results around.

[JKTKops]

I know this is several years late, but there is indeed a better solution, which I found while trying to build my own compiler as a learning exercise, using the code here as a starting point.

in particular, the code

infer expr = case expr of
  ...
  Let x e1 e2 -> do
    env <- ask
    t1 <- infer e1
    let sc = generalize env t1
    ...

should be

infer expr = case expr of -- < I would also use LambdaCase here
  ...
  Let x e1 e2 -> do
    env <- ask
    (t0, constraints) <- listen $ infer e1
    subst <- liftEither $ runSolve constraints
    let t1 = apply subst t0
        sc = generalize env t1
    ...

The issue, as I'm sure is well known, is that we generate constraints for the type variable in the scheme bound to x, which are never solved because each use of x causes instantiation of its scheme. This is not a problem if x's type should truly be universal, but this is rarely the case. My simplest breaking example was \y -> let x = y + 1 in x. We generate the type y :: a and the scheme x :: forall b. b. We also generate the constraints a ~ Int and b ~ Int, where the latter will never be used. In the body of the let, we instantiate x to x :: c. Then we solve our constraints and produce the incorrect type forall a. Int -> a.

This can be fixed simply by listening to the constraint generation while inferring the RHS of the binding, solving the constraints, and applying the substitution to to the type of e1 before generalizing it. Now we correctly generate the type y :: a and the scheme x :: forall . Int.

The algorithm referenced in #82 warns of a caveat with generalization, but the existing logic seems to already handle it; the given example:

(\f x -> let g = f in g 0) (\x -> if x then True else False) True

fails the type checker.