Remove duplication of type definitions across .fst and .fsti in the compiler

[aseemr]

Building more on #2512, this PR tweaks the interleaving strategy of .fsti and .fst for the compiler code (i.e. --MLish), so that the type definitions need not be duplicated across .fsti and .fst.

Problem

In the current compiler code, take FStar.Syntax.Syntax for instance, type definitions such as term are duplicated in .fsti and .fst. This is a pain, every change has to be done in two places. Whereas in F*, if the clients needs to work with it, the type definition is written only in .fsti. My guess is that earlier our hands were tied by F# compatibility. But now that it is no longer a constraint, we can do better.

Changing the interleaving strategy

The main changes are in 392429d commit. They relate to how we interleave when --MLish flag is on.

• Earlier, we were keeping only val decls from the .fsti, ignoring everything else.
• When we encounter a let in .fst, we searched for its val in the interface declarations, if found, we prefixed let with the corresponding val, else no op.

In this PR:

• We keep Tycon and val from .fsti.
• When we encounter a let in .fst, we first get the prefix type definitions from the interface declarations, then find val, and typecheck the prefix type definitions, val, and let.

Enabling us to get rid of the duplication of types from .fst.

Additionally, this PR also disallows writing type t in interfaces, instead the programmer must write a val, as is custom in F*.

Future work

We still don't enforce the proper ordering of let definitions as per the val declarations in the interface in the compiler code. Ideally, the interleaving code would not treat --MLish in any special way.

But that's some grunt work, leaving for future.

[nikswamy]

Thanks @aseemr !

Indeed it would be better to not have any special handling for --MLish, but this is great progress to better, more easily maintainable compiler code. In the long run, we should get rid of the interleaving of interfaces altogether: cf #1770

Since the compiler is the only place that uses --MLish, and if this change works for bootstrapping the compiler, I think we should go ahead and merge it.