Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) newInstance は全称量化された型変数を ある型変数に固定したコピーを作ってからから単一化する