关于将 solution: Solution 作为额外参数加入到 check 与 infer 中

[xieyuheng]

以 infer2 为例：

function infer2(implicit A: Type, implicit B: Type, x: A, y: B): Type {
  return Pair(A, B)
}

compute infer2(sole, "abc")

• infer infer2 发现了两个 ImplicitPi -- implicit A: Type, implicit B: Type
• 就直接插入两个 ImplicitAp 得到 infer2(implicit A)(implicit B) 作为 inferred.core
• 然后返回的 inferred.type 其实是 (x: A, y: B) -> Type，用这个 Pi 来 check 两个参数 (sole, "abc")
• 在 check 的过程中，如果可以 infer 参数，得到 inferred.argType，就 solve(solution, inferred.argType, givenArgType)
• 最后 evaluate 也要带有 solution 参数，在遇到 A 和 B 的时候，如果在 env 里找不到，就去 solution 里找

[xieyuheng]

关于 solution 的垃圾回收，可以在每次 stmt.execute 结束之后，清空当前的 mod.solution

[xieyuheng]

如果 evaluate 需要 solution，用 ctx 生成 env 的时候，是否也需要带上 solution？

[xieyuheng]

evaluate Pi：

    case "Pi": {
      return Values.Pi(
        evaluate(solution, env, core.argType),
        Closure(env, core.name, core.retType),
      )
    }

这里的 evaluate 用了 solution 参数，但是构造 Closure 的时候没有给 solution。

感觉这样 Closure 也要带 solution 了（并且要复制一下，因为 solution 有副作用）。

否则定义不了 applyClosure：

export function applyClosure(closure: Closure, arg: Value): Value {
  return evaluate(EnvCons(closure.name, arg, closure.env), closure.body)
}

[xieyuheng]

不对。

好像 Closure 也必须包含带有副作用的 solution，Closure 构造之后得到的解没法在 Closure 里用到。

[xieyuheng]

这样看来就不能在 stmt 之间 清空 solution 了。

因为，如果 let g = f(x) 返回了 Closure 它所包含的 solution 不能被清除。