[Parameterized Modules] Variable Substitution Crash

[WeeknightMVP]

BlockCipher.cry:

module BlockCipher where

parameter
  type Key: *
  type Block: *

  encrypt_block: Key -> Block -> Block

Kaboom.cry:

module Kaboom = BlockCipher where

parameter
  type _k: #

type Key = [8 * _k]
type Block = [64]
type RoundKey = [64]

aux : RoundKey -> Block -> Block
aux RK P = zero

// key_schedule : Key -> RoundKey
key_schedule K = zero
  where
    _ = [ groupBy`{4} K ]

// encrypt_block : Key -> Block -> Block
encrypt_block key pt = aux (key_schedule key) pt

> chcp 65001
Active code page: 65001
> cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.8.1 (1e1f7af, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :m Kaboom
Loading module BlockCipher
Loading module Kaboom
cryptol: 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:  Cryptol.TypeCheck.Monad.extendSubst
  Message:   Escaped quantified variables:
             Substitution:  ?Kaboom::encrypt_block_1`934 := 2 * Kaboom::_k
             Vars in scope: []
             Escaped:       [Kaboom::_k]
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\TypeCheck\Monad.hs:561:16 in cryptol-2.8.1-CsLNPSw0BJM1P20gctBZPn:Cryptol.TypeCheck.Monad
%< ---------------------------------------------------

Uncommenting either of the type signatures for key_schedule or encrypt_block avoids the crash. Commenting out where _ = [ groupBy`{4} K ] produces an error for insufficient polymorphism:

[error] at ...\Kaboom.cry:19:1--19:14:
  The type ?Kaboom::encrypt_block_1`949 is not sufficiently polymorphic.
    It cannot depend on quantified variables: _k
  where
  ?Kaboom::encrypt_block_1`949 is 1st type argument of 'encrypt_block' at ...\Kaboom.cry:19:1--19:14
  _k is module parameter _k at ...\Kaboom.cry:4:8--4:10

[yav]

Thanks for reporting this. It looks like we forgot to add the module parameters as being in scope somewhere, probably when checking module instantiations.