Documentation

This is a very interesting function. Like typecheckIface, we want to type check an interface file into a ModDetails. However, the use-case for these ModDetails is different: we want to compare all of the ModDetails to ensure they define compatible declarations, and then merge them together. So in particular, we have to take a different strategy for knot-tying: we first speculatively merge the declarations to get the "base" truth for what we believe the types will be (this is "type computation.") Then we read everything in relative to this truth and check for compatibility.

During the merge process, we may need to nondeterministically pick a particular declaration to use, if multiple signatures define the declaration (mergeIfaceDecl). If, for all choices, there are no type synonym cycles in the resulting merged graph, then we can show that our choice cannot matter. Consider the set of entities which the declarations depend on: by assumption of acyclicity, we can assume that these have already been shown to be equal to each other (otherwise merging will fail). Then it must be the case that all candidate declarations here are type-equal (the choice doesn't matter) or there is an inequality (in which case merging will fail.)

Unfortunately, the choice can matter if there is a cycle. Consider the following merge:

signature H where { type A = C; type B = A; data C } signature H where { type A = (); data B; type C = B }

If we pick type A = C as our representative, there will be a cycle and merging will fail. But if we pick type A = () as our representative, no cycle occurs, and we instead conclude that all of the types are unit. So it seems that we either (a) need a stronger acyclicity check which considers *all* possible choices from a merge, or (b) we must find a selection of declarations which is acyclic, and show that this is always the "best" choice we could have made (ezyang conjectures this is the case but does not have a proof). For now this is not implemented.

It's worth noting that at the moment, a data constructor and a type synonym are never compatible. Consider:

signature H where { type Int=C; type B = Int; data C = Int} signature H where { export Prelude.Int; data B; type C = B; }

This will be rejected, because the reexported Int in the second signature (a proper data type) is never considered equal to a type synonym. Perhaps this should be relaxed, where a type synonym in a signature is considered implemented by a data type declaration which matches the reference of the type synonym.

Typecheck a signature ModIface_ under the assumption that we have instantiated it under some implementation (recorded in mi_semantic_module) and want to check if the implementation fills the signature.

This needs to operate slightly differently than typecheckIface because (1) we have a NameShape, from the exports of the implementing module, which we will use to give our top-level declarations the correct Names even when the implementor provided them with a reexport, and (2) we have to deal with DFun silliness (see Note [rnIfaceNeverExported])