Expand private type synonyms

[yav]

This is more of an improvement than a bug.
Consider the following example:

module A where

 f : [T]
 f = 10

 private type T = 8

In this case we are exporting f, but not the type synonym T. This is questionable practice, but I think that in this case, Cryptol should export f with type [8] rather than [A::T]. This type is equivalent, and the idea is that if the type synonym is not exported, then it should not be used when reporting types.

[brianhuffman]

Instead, we could just report this situation as an error: You are not allowed to mention a private type synonym in the signature of an exported function.

[brianhuffman]

There are some other corner cases to consider: What if the type of a function f exported from module A mentions a type synonym that is defined in module B?

[brianhuffman]

There are also two levels of strictness we could enforce:

1. Require that types of exported functions must be expressible using only public types
2. Require that types of exported functions must be able to have all type synonyms recursively expanded, without running into any private type synonyms

[brianhuffman]

A desired property of the type pretty-printer is that if you print a type, you should be able to cut and paste the type and cryptol should be able to parse it back in.

[robdockins]

I think the easiest thing to do here is to modify the pretty printer so that it will only print a type synonym if the name is currently in scope, and simply recurse into the body of the type definition otherwise. A quick look in the code leads me to believe all the necessary information is already available in the proper places.

[brianhuffman]

I have a patch for this, which is just waiting in line behind some other PRs.