Allow referring to type synonym in functor instantiation

[RyanGlScott]

Surprisingly, one cannot write something like this using Cryptol's module system:

 module TypeAlias where
  interface submodule Interface where
    type Alias = Bool
    value: Alias

  submodule Functor where
    import interface submodule Interface

  submodule Instance = submodule Functor where
    value = False: Alias

Loading module TypeAlias
[error] at TypeAlias.cry:10:20--10:25
    Type not in scope: Alias

On the other hand, if you leave off the explicit type signature for value in Instance:

  submodule Instance = submodule Functor where
    value = False

Then Cryptol accepts it. This works around the issue, but it is not a very satisfying workaround. Some use cases for functor instantiations involve complex type definitions, where redefining the type alias is complicated and redundant.

It would be nice if Cryptol provided some way to write value = False: Alias.

[yav]

At the moment

module M = F where
  defs

is syntactic sugar for:

module Anon where
  defs

module M = F{Anon}

To do what's described in the ticket we'd either have to stop treating the where modules as syntactic sugar, or have some way to associate the interface with M.

I think the second option would be largely preferable. Perhaps a good way to do this would be to add something that we've been missing so far, namely a way to specify that a module satisfies one or more interfaces. Without worrying about notation too much, this might look something like this:

module Anon where
  implements interface Interface
  defs

When validating such a module, we'd check that defs satisfies the requirements of Interface.

In addition, we could add the type definitions from Inteface to Anon. Note, however, that the type definitions in Intefrace would, in general, depend on the some of the type definitions in defs (as the type definitions in an interface can mention the parameters, and here the module is supposed to be specifying the parameters), so we have to be careful to report cycles.

Perhaps the easiest is to say that the interface definitions are added as new defintiions to the enclosing module. This would be akin ML's include mechanism (which is different from Cryptol's).

One potential difficulty is that if one has multiple interface declarations the type definitions from them might clash.
For example:

interface A where
  type A: *
  type T = [8]A

interface B where
  type A: *
  type T = [16]A

module X where
  implements interface A
  implements interface B
 type A = Bit

The easiest option would be to simply report this as an error.