Revert #1790

[samcowger]

@eddywestbrook and I had some further discussions on #1790, and realized that it allowed non-type-correct terms to be constructed. One such example is, unfortunately, the very SAWCore term I cited in that PR:

\(u1229 : Num) ->
  \(u1230 : isort 0) ->
    \(x : seq (tcMul (TCNum 3) u1229) u1230) -> 
      ecSplit u1229 (TCNum 3) u1230 x

ecSplit's type is (m n : Num) -> (a : isort 0) -> seq (tcMul m n) a -> seq m (seq n a). Applying it manually to its type arguments yields a function of type seq (tcMul u1229 (TCNum 3)) u1230 -> seq u1229 (seq (TCNum 3) u1230), which is incompatible with application to x, whose type transposes the multiplicands u1229 and TCNum 3.

Indeed, check_term applied to this term will reveal its failure to typecheck. I think this may suggest the need for more systematic, in-tool applications of check_term or its underpinnings, which I'll work on in a forthcoming PR or surface in a separate issue.

While I figure out how best to solve the original issue behind #1790, I'm reverting its changes, as they're far more unsound than the previous status quo.

[eddywestbrook]

Well, I am sad to see an entire integration test disappear, but I guess it has to be. :(

Thanks for taking care of this, Sam!

[eddywestbrook]

The heapster-tests failure seems to be the result of a type code in the LLVM generated by rustc on ubuntu that llvm-pretty-bc-parser can't handle. Because the test passes on OSX, and because this PR has nothing to do with that test, it is probably reasonable to ignore it.