Algorithm W and monomorphic type coercion

Question

I'm trying to write my own type inference algorithm for a toy language, but I'm running into a wall - I think algorithm W can only be used for excessively general types.

Here are the expressions:

Expr ::= EAbs String Expr
       | EApp Expr Expr
       | EVar String
       | ELit
       | EConc Expr Expr

The typing rules are straightforward - we proceed to use type variables for abstraction and application. Here are all possible types:

Type ::= TVar String
       | TFun Type Type
       | TMono

As you might have guessed, ELit : TMono, and more specifically, EConc :: TMono → TMono → TMono.

My issue comes from doing the actual type inference. When recursing down an expression structure, the general technique when seeing an EAbs is to generate a fresh type variable representing the newly bound variable, replace any occurrences of typing in our context with the (String : TVar fresh) judgment, then continue down the expression.

Now, when I hit EConc, I was thinking about taking the same approach - replace the free expression variables of the sub expressions with TMon in the context, then type-infer the sub expressions, and take the most-general unifier of the two results as the main substitution to return. However, when I try this with an expression like EAbs "x" $ EConc ELit (EVar "x"), I get the incorrect TFun (TVar "fresh") TMon.

Answer 1

You need to use mgu to coerce sub-expressions. If you directly manipulate the context to affect sub expressions, you don't know how that affects earlier types. Use mgu to get the substitution that unifies sub expressions to TMon, then compose that substitution in the result.