Impoting interfaces from functors

[yav]

Currently we can't import an interfaces from a functor, because the instantiation of the functor would have to happen inside the module, and the parameters of the functor cannot depend on things defined inside it. For example:

module FI where
   parameter:
      type n : #

  interface I where
     f : [n]

module A where
  import FI{M}    
  import I         -- Doesn't work

-- Desugared A
module A where
  module Anon = FI{M}
  import Anon        
  import I

We could allow such imports as long as the instantiation does not depend on anything in the module (i.e., it could be moved outside the module).

There is a second case that it would be good to support, and where the instantiation cannot be moved outside the module, namely when we are passing through other parameters:

interface module J where
  type n : #

module B where
   import interface J
   import FI { interface J }
   import I

This requires us to change the implementation of pass through parameters, which is probably a good idea any way. Currently, this would be desugared like this:

module B where
  import interface J
  submodule AnonArg where
    type n = n
  submodule Anon = FI { AnonArg }
  import Anon

Note that in this case we cannot move Anon outside the module because it depends on the parameters that came in through J. To support this, we should avoid creating the local "copy" module (AnonArg in the example), and treat this type of instantiation as its own construct.

To summarize, it should be possible to use interfaces from functor instantiations as long as the instantiations only depend on externally defined modules and other parameters (and the parameter dependencies don't form loops of course).

[WeeknightMVP]

Not sure if this is related, but I'm trying to define functors that "extend" a common interface in different ways and a functor that generates an instantiation of one extended interface in terms of the other; Cryptol reports that the same field in their respective imports of the same extended interface cannot match:

module SymmetricCipher where

submodule Util where
  swap : {a, b, c} (a -> b -> c) -> b -> a -> c
  swap f x y = f y x

/** a common interface used to generate another interface and an instantiation */
interface submodule I_Common where
  type Key: *
  type Message: *

/** functor to "extend" the common interface */
submodule F__I_Symmetric__I_Common where
  import interface submodule I_Common

  interface submodule I_Symmetric where
    encipher: Key -> Message -> Message
    decipher: Key -> Message -> Message

/** another functor to "extend" the common interface with different fields */
submodule F__I_Iterated__I_Common where
  import interface submodule I_Common

  interface submodule I_Iterated where
    type rounds : #
    type RoundKey : *

    expand_key : Key -> [rounds]RoundKey

    encipher_round : RoundKey -> Message -> Message
    decipher_round : RoundKey -> Message -> Message

/** functor (of the common interface) to generate a functor (of the second extended interface) to instantiate the first */
submodule F__P_Symmetric__I_Iterated where
  import interface submodule I_Common
  import submodule F__I_Iterated__I_Common { interface I_Common } (I_Iterated)

  submodule P_Symmetric where
    import interface submodule I_Iterated

    import submodule Util (swap)

    // Explicit type parameters are needed to avoid more "not sufficiently polymorphic" errors.
    encipher k pt = foldl`{rounds} (swap`{RoundKey, Message} encipher_round) pt (expand_key k)
    decipher k ct = foldl`{rounds} (swap`{RoundKey, Message} decipher_round) ct (expand_key k)

Cryptol> :r
Loading module Cryptol
Loading module SymmetricCipher

[error] at .../SymmetricCipher.cry:46:82--46:92:
  Inferred type is not sufficiently polymorphic.
    Quantified variable: SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey
    cannot match type: SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::RoundKey
    Context: _ -> [_] ERROR
    When checking function call
  where
  SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::RoundKey is module parameter SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::RoundKey at .../SymmetricCipher.cry:26:10--26:18
  SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey is module parameter SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey at .../SymmetricCipher.cry:39:32--39:42

Demoting the functors that import the common interface into a common functor submodule that imports this interface (and adding type constraint (fin rounds) ) convinces Cryptol to load the nested module:

module SymmetricCipher where

submodule Util where
  swap : {a, b, c} (a -> b -> c) -> b -> a -> c
  swap f x y = f y x

/** a common interface used to generate another interface and an instantiation */
interface submodule I_Common where
  type Key: *
  type Message: *

/** functor to derive all submodules from the same common interface import */
submodule F__I_Common where
  import interface submodule I_Common

  /** "extension" of the common interface */
  interface submodule I_Symmetric where
    encipher: Key -> Message -> Message
    decipher: Key -> Message -> Message

  /** "extension" of the common interface with different fields */
  interface submodule I_Iterated where
    type rounds : #
    type constraint fin rounds

    type RoundKey : *

    expand_key : Key -> [rounds]RoundKey

    encipher_round : RoundKey -> Message -> Message
    decipher_round : RoundKey -> Message -> Message

  /** functor (of the second extended interface) to instantiate the first extended interface */
  submodule F_P_Symmetric__I_Iterated where
    import interface submodule I_Iterated
    import submodule Util (swap)

    // Explicit type parameters are needed to avoid more "not sufficiently polymorphic" errors.
    encipher k pt = foldl`{rounds} (swap`{RoundKey, Message} encipher_round) pt (expand_key k)
    decipher k ct = foldl`{rounds} (swap`{RoundKey, Message} decipher_round) ct (expand_key k)

Cryptol> :r
Loading module Cryptol
Loading module SymmetricCipher

Returning to the original example and adding type constraint (fin rounds) to interface submodule I_Iterated reveals another error in which this type constraint does not propagate to its instantiation (alongside the original error):

[error] at .../SymmetricCipher.cry:1:1--46:95:
  Failed to validate user-specified signature.
    when checking the module's parameters,
    we need to show that
      for any type SymmetricCipher::F_P_Symmetric__I_Iterated::I_Common::Key,
      SymmetricCipher::F_P_Symmetric__I_Iterated::I_Common::Message,
      SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey,
      SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::rounds
      assuming
        • fin SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::rounds
      the following constraints hold:
        • fin SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::rounds
            arising from
            use of expression foldl
            at .../SymmetricCipher.cry:45:21--45:26
  where
  SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::rounds is module parameter SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::rounds at .../SymmetricCipher.cry:25:10--25:16
[error] at .../SymmetricCipher.cry:46:82--46:92:
  Inferred type is not sufficiently polymorphic.
    Quantified variable: SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey
    cannot match type: SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::RoundKey
    Context: _ -> [_] ERROR
    When checking function call
  where
  SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::RoundKey is module parameter SymmetricCipher::F__I_Iterated__I_Common::I_Iterated::RoundKey at .../SymmetricCipher.cry:27:10--27:18
  SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey is module parameter SymmetricCipher::F_P_Symmetric__I_Iterated::P_Symmetric::I_Iterated::RoundKey at .../SymmetricCipher.cry:40:32--40:42

Adding interface constraint (fin rounds) to submodule F_P_Symmetric__I_Iterated removes this new error, retaining the original.