We want our typechecker to throw errors when checking any pair of term and type that shouldn't typecheck.
A way of achieving some level of confidence in this direction is by getting a decently long list of term/type pairs such that no two pairs of types are defeq and then trying to check some permutations and expecting them to fail. Example:
Suppose we have the following pairs of terms and types:
(te1, ty1), (te2, ty2), (te3, ty3)
Then the following shouldn't typecheck for any pair:
(te1, ty2), (te2, ty3), (te3, ty1)
We want our typechecker to throw errors when checking any pair of term and type that shouldn't typecheck.
A way of achieving some level of confidence in this direction is by getting a decently long list of term/type pairs such that no two pairs of types are defeq and then trying to check some permutations and expecting them to fail. Example:
Suppose we have the following pairs of terms and types:
Then the following shouldn't typecheck for any pair: