Bugfix: normalize SAW core types when necessary to type elimination forms

[eddywestbrook]

This fix addresses issue #1420, where the type-checker does not normalize the types of globals when it tries to type-check applications or pair or record projections. For example, the definitions

FunType : (a b:sort 0) -> sort 0;
FunType a b = a -> b;

myId : FunType Nat Nat;
myId x = x;

applyId : Nat -> Nat;
applyId x = myId x;

will fail to type-check, because the type of myId is not normalized to a function type when myId is applied to x.

The fix is to update calls to recognizers asSort, asPi, asPairType, and asRecordType in the type-checker so that the types passed to these recognizers are normalized when the recognizers fail.

[brianhuffman]

Looks good