#10: some improvements on #10: now the typechecking is accurate enough
to ensure that there is no verify error.