Preserve Type Synonyms in Shallow Embedding

[gteege]

Up to now the type synonyms defined in Cogent have been unfolded at the end of the typecheck stage. When generating the shallow embedding, monomorphic type synonyms have been re-introduced by matching the replacements. Pull requests #390 and #395 extended this to polymorphic types. However, this may yield surprising results, since several type synonyms may match a type expression, and an arbitrary one is selected.

Therefore, this pull request replaces the re-introduction of type synonyms by preserving the original type synonyms for the shallow embedding generation. The advantages are:

• The shallow embedding resembles more the original Cogent code.
• The shallow embedding code is smaller (unfolding the type synonyms may lead to exponentially larger code)

The implementation works as follows: The type synonyms are not unfolded at the end of the typecheck stage, instead, they are on-demand unfolded in the desugaring stage, whenever necessary. At the beginning of the normalisation stage they are permanently unfolded, so the remaining stages are not affected. The shallow embedding generated in the desugaring stage uses the preserved type synonyms, the shallow embedding generated in later stages has type synonyms unfolded. As a drawback, developers have to keep in mind to on-demand unfold type synonyms in the desugaring stage.

Some remarks about details:

• The type synonym definitions have been added to the monad state of the internal typechecking to do on-demand unfolding there.
• Monadic actions have been defined for on-demand unfolding types and expressions in desugaring, internal typecheck, and shallow embedding generation.
• On-demand unfolding can be shallow (when matching the type with a specific variant) or deep (when testing for subtyping or type equality).
• The constant definitions have been treated like the other definitions, passing them through the stages instead of re-creating them in every stage in genShallow.
• The type synonym definitions are passed through all stages to be available in glue generation for the internal typecheck states.

All compiler regression tests have been passed. For BilbyFS the shallow embedding is successfully created and the generated C code is identical.

[gteege]

I am aware of the failed checks and will fix them, so please be patient...

[gteege]

Ok, now it works (the failed checks now are due to a misconfiguration in examples/buffer and are not related to this pull-request, all other tests were successful). Two further remarks:

• The permanent unfolding has been postponed to the beginning of the simplification stage, so that the preserved type synonyms are also used in the normalised shallow embedding.
• In the Core-AST a new variant TSyn has been introduced for Type to store the necessary information for type synonyms. This has been preferred over modifying the TCon variant and its processing. After permanent unfolding all TSyn are gone and the Type processing can stay as it is.

[gteege]

I just added a small improvement. Now in the shallow embedding record and variant types with name nnn are matched back to using the type synonym nnn (which is printed as nnn\<^sub>T). This makes inferred type annotations more readable because it is closer to the original Cogent code.

[zilinc]

Merged, with some minor fixes. Thanks for the PR.