SAW core type-checker does not normalize the types of constants

[eddywestbrook]

The following well-typed SAWCore code will cause a type error:

`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;`

The issue is that the type-checker needs to normalize the type of myId when the application happens in order to see that FunType Nat Nat normalizes to the arrow type Nat -> Nat. A similar problem happens with constants whose types normalize to (but are not) record or pair types.

One suggestion for how to fix this is to replace calls to the recognizer functions asPi, asPairType, and asRecordType in the SCTypeCheck module with calls to new functions asPiWHNF, asPairTypeWHNF, and asRecordTypeWHNF that call the normalizer in the case that the associated recognizer function fails to match.

[eddywestbrook]

Fixed by #1426