Some test cases failed in polymorphic type checker

[SeungUkLee]

Some test cases failed in polymorphic type checker

[SeungUkLee]

M Spec에 Static Semantics 의 $\text{[Op]}$, $\text{[Write]}$ rule 을 보면 $\tau$ 가 각각 $i, b, s, l$ 과 $i, b, s$ 인 것을 볼 수 있다.

즉, m_algorithm 에 pattern matching 에서 다음과 같이 TVar로 타입변수를 만들면 안됨.

let rec m_algorithm : TyEnv.t -> M.exp -> typ -> Subst.t =
 fun tyenv exp expected ->
  match exp with
  | ...
  | M.WRITE e -> 
    let a = TVar (new_var ()) in ...
  | M.BOP (op, e1, e2) ->
    let bop op r = ...
    match op with
    | ...
    | M.EQ -> bop (TVar (new_var ())) TBool)
  | ...

이는 다음과 같이 TWritableVar, TComparableVar 을 추가하면 간단하게 해결이 가능하다: b63d2bc 참고

type typ =
  | ...
  | TVar of var
  | TWritableVar of var
  | TComparableVar of var

...

let rec m_algorithm : TyEnv.t -> M.exp -> typ -> Subst.t =
 fun tyenv exp expected ->
  match exp with
  | ...
  | M.WRITE e -> 
    let a = TWritableVar (new_var ()) in ...
  | M.BOP (op, e1, e2) ->
    let bop op r = ...
    match op with
    | ...
    | M.EQ -> bop (TComparableVar (new_var ())) TBool)
  | ...

하지만,

• #2 또 다른 문제가 발생