- infer e >>= \(s1, et)->
- applySubst s1 >>|
- changeGamma (extend k (Forall [] et)) >>| //todo: fieldselectors
- pure (s1, VoidType)
+ lookup k >>= \expected ->
+ infer e >>= \(s1, given)->
+ lift (unify expected given) >>= \s2->
+ let s = compose s2 s1 in
+ applySubst s >>|
+ changeGamma (extend k (Forall [] given)) >>| //todo: fieldselectors
+ pure (s, VoidType)