[Parameterized Modules] newtype instance has inconsistent type

[WeeknightMVP]

My attempt to apply the instantiated block cipher from Issue #812 to a cipher mode fails:

CBC_.cry

module CBC_ where

import `BlockCipher_ (BlockCipher)

parameter
    type _Key: *
    type _Block: *
    type constraint (Cmp _Block, Logic _Block)

    _blockCipher: BlockCipher _Key _Block


type Key = _Key
type Block = _Block

blockCipher = _blockCipher


type Op n = Key -> Block -> [n]Block -> [n]Block


encrypt: {n} Op n
encrypt k iv ps = cs
  where
    cs = [ blockCipher.encrypt k (p ^ c')
         | p <- ps
         | c' <- [iv] # cs ]

decrypt: {n} Op n
decrypt k iv cs = 
    [ (blockCipher.decrypt k c) ^ c'
    | c <- cs
    | c' <- [iv] # cs ]

_CBC_XOR32.cry

module _CBC_XOR32 = CBC_ where

import XOR32Cipher (blockCipher)

type _Key = [32]
type _Block = [32]

_blockCipher = blockCipher

Cryptol> :m CBC_
Loading module BlockCipher_
Loading module CBC_Cryptol> :m _CBC_XOR32
...
Loading module _CBC_XOR32

[error] at ...\_CBC_XOR32.cry:8:1--8:13:
  Type mismatch:
    Expected type: `BlockCipher_::BlockCipher _CBC_XOR32::_Key
                                              _CBC_XOR32::_Block
    Inferred type: _XOR32Cipher::BlockCipher

Would an analogous blockCipher instantiated from BlockCipher_, as in the Issue #812 crash, have worked? If not, is there a way to encapsulate instances of parameterized modules in this fashion?

[WeeknightMVP]

Closing as newtype is obsolete, per #815.

[yav]

I think I see what's happening here. The issue is that when you define a newypte in a functor, you get a different newypte for each functor instantiation---this has to happen as the same type can't have different definitions. In fact, when you use a backtick import, the newyptes don't even have the same type parameters (one has 0, one has 2).

Perhaps something like this would work?

submodule BlockCipherWithTypes where                                                
                                                                                    
  parameter                                                                         
    type Key:   *                                                                   
    type Block: *                                                                   
    type constraint Cmp Block                                                       
                                                                                    
  type Op = Key -> Block -> Block                                                   
  newtype BlockCipher = { encrypt: Op, decrypt: Op }                                
                                                                                    
  submodule Ops where                                                               
    parameter                                                                       
      encrypt: Op                                                                   
      decrypt: Op                                                                   
                                                                                    
    blockCipher = BlockCipher { encrypt = encrypt, decrypt = decrypt }              
                                                                                    
submodule Cipher_128_16 = submodule BlockCipherWithTypes where                      
  type Key   = [128]                                                                
  type Block = [16]                                                                 
                                                                                    
import submodule Cipher_128_16 as Cipher_128_16                                     
                                                                                    
submodule NoCipher = submodule Cipher_128_16::Ops where                             
  encrypt key val = val                                                             
  decrypt key val = val                                                             
                                                                                    
                                                                                    
import submodule NoCipher as NoCipher                                               
                                                                                    
example = NoCipher::blockCipher.encrypt 1 2