[Parameterized Modules] newtype crash

[WeeknightMVP]

Consider a parameterized block cipher specification and nested instantiation:

BlockCipher_.cry

module BlockCipher_ where

parameter
    type _Key: *
    type _Block: *
    type constraint Cmp _Block

    _encrypt: Op
    _decrypt: Op

type Op = _Key -> _Block -> _Block

newtype BlockCipher = { encrypt: Op, decrypt: Op }
// blockCipher = BlockCipher { encrypt = _encrypt, decrypt = _decrypt }  // <-- induces crash

_XORCipher_.cry

module _XORCipher_ = BlockCipher_ where

parameter
    type _KeyBlock: *
    type constraint (Cmp _KeyBlock, Logic _KeyBlock)

type _Key = _KeyBlock
type _Block = _KeyBlock

_encrypt = (^)`{_KeyBlock}
_decrypt = (^)`{_KeyBlock}

_XOR32Cipher.cry

module _XOR32Cipher = _XORCipher_ where

type _KeyBlock = [32]

Alas, uncommenting the indicated line in BlockCipher_ causes a crash when loading _XOR32Cipher:

_XORCipher_(parameterized)> :m BlockCipher_
Loading module BlockCipher_
BlockCipher_(parameterized)> :m _XORCipher_ 
Loading module _XORCipher_
_XORCipher_(parameterized)> :m _XOR32Cipher 
Loading module _XOR32Cipher
cryptol.exe: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  1e1f7af812b122e0dcd4f4d36a2a84a4864427a4
  Branch:    HEAD (uncommited files present)
  Location:  [Eval] evalExpr
  Message:   var `BlockCipher_::BlockCipher` is not defined
...
_XOR32Cipher::BlockCipher -> <function>
...
 _XOR32Cipher::BlockCipher -> <function>
CallStack (from HasCallStack):
  panic, called at src\Cryptol\Utils\Panic.hs:21:9 in cryptol-2.8.1-CsLNPSw0BJM1P20gctBZPn:Cryptol.Utils.Panic
  panic, called at src\Cryptol\Eval.hs:158:9 in cryptol-2.8.1-CsLNPSw0BJM1P20gctBZPn:Cryptol.Eval
%< ---------------------------------------------------

Modifying _XOR32Cipher to instantiate BlockCipher_ directly (with the same line uncommented) causes a similar crash.

Given this issue, achieving the desired effect (to export an encapsulated block cipher instance, e.g. as a parameter for cipher modes) requires exporting aliases for BlockCipher_ parameters...

BlockCipher_.cry

type Key = _Key
type Block = _Block

encrypt = _encrypt
decrypt = _decrypt

...and wrapping _XOR32Cipher:

module XOR32Cipher where

import _XOR32Cipher

blockCipher = BlockCipher { encrypt=encrypt, decrypt=decrypt }

[WeeknightMVP]

Closing as newtype is obsolete, per #815.

[WeeknightMVP]

In the current functors-merge branch, BlockCipher_ loads successfully, whereas _XORCipher_ reports another error:

Parse error at .../_XORCipher_.cry:4:10--4:19
  Instantiation of a parameterized module may not itself be parameterized

This can be remediated by separating the functor and instantiation components of _XORCipher_. Updating the example...

interface module I_BlockCipher where
  type Key: *

  type Block: *
  type constraint Cmp Block

  type Op = Key -> Block -> Block

  encrypt: Op
  decrypt: Op

module F_BlockCipher where
  import interface I_BlockCipher as I

  newtype BlockCipher = { encrypt: I::Op, decrypt: I::Op }
  blockCipher = BlockCipher { encrypt = I::encrypt, decrypt = I::decrypt }

interface module I_XORCipher where
  type KeyBlock: *

  type Key = KeyBlock
  type Block = KeyBlock

  type constraint (Cmp KeyBlock, Logic KeyBlock)

module F_XORCipher where
  import interface I_XORCipher as I

  submodule P_BlockCipher where
    type Key = I::KeyBlock
    type Block = I::KeyBlock

    encrypt = (^)`{I::KeyBlock}
    decrypt = (^)`{I::KeyBlock}

  submodule BlockCipher = F_BlockCipher { submodule P_BlockCipher }

...these modules load without crashing. However, when I try a concrete example...

module P_XOR32Cipher where
  type KeyBlock = [32]

module XOR32Cipher where
  import F_XORCipher { P_XOR32Cipher } (P_BlockCipher, BlockCipher)
  import submodule P_BlockCipher (Key, Block)
  import submodule BlockCipher (blockCipher)

  (key, block) = random 0 : (Key, Block)

  test : Bool
  test = blockCipher.decrypt key (blockCipher.encrypt key block) == block

...the REPL reports type matching errors:

Cryptol> :m XOR32Cipher
Loading module Cryptol
Loading interface module I_XORCipher
Loading interface module I_BlockCipher
Loading module F_BlockCipher
Loading module F_XORCipher
Loading module P_XOR32Cipher
Loading module XOR32Cipher
[error] at .../XOR32Cipher.cry:9:10--9:29:
  Inferred type is not sufficiently polymorphic.
    Quantified variable: F_BlockCipher::I::Key
    cannot match type: [32]
    Context: ERROR -> _
    When checking type of field 'decrypt'
  where
  F_BlockCipher::I::Key is module parameter F_BlockCipher::I::Key at .../I_BlockCipher.cry:2:8--2:11
[error] at .../XOR32Cipher.cry:9:10--9:29:
  Inferred type is not sufficiently polymorphic.
    Quantified variable: F_BlockCipher::I::Block
    cannot match type: [32]
    Context: _ -> _ -> ERROR
    When checking type of field 'decrypt'
  where
  F_BlockCipher::I::Block is module parameter F_BlockCipher::I::Block at .../I_BlockCipher.cry:4:8--4:13
[error] at .../XOR32Cipher.cry:9:35--9:54:
  The type ?a is not sufficiently polymorphic.
    It cannot depend on quantified variables: F_BlockCipher::I::Block
    Context: _ -> _ -> ERROR
    When checking type of field 'encrypt'
  where
  ?a is type of function argument at .../XOR32Cipher.cry:9:10--9:74
  F_BlockCipher::I::Block is module parameter F_BlockCipher::I::Block at .../I_BlockCipher.cry:4:8--4:13

I've seen other examples where newtype still crashes, though.

[yav]

Here is a minimized version of the problematic example:

submodule F where                                                                   
  parameter                                                                         
    type T : *                                                                   
                                                                                 
  newtype NT = { field : T }                                                     
  nt         = NT { field = undefined }                                          
                                                                                 
                                                                                 
submodule M where                                                                
                                                                                 
  import submodule F where                                                       
    type T = [32]                                                                
                                                                                 
  test = nt.field 

My current hypothesis is that the problem is that newtype values are not instantiated correctly.