Panic with Arrow Kinds in Parameterized Modules

[j-christensen1]

I was trying to generalize the behavior of something like this:

module NotParameterized where

  type Arrow n = n + 1

  f: {n} () => [n] -> [Arrow n]
  f x = [True] # x

by leaving Arrow and f parameters.

module Parameterized where

    parameter
        type Arrow: # -> #

        f: {n} () => [n] -> [Arrow n]

This panics, however:

version 3.3.0 (285c30d)
https://cryptol.net  :? for help

Loading module Cryptol
Loading interface module Parameterized__parameter
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  285c30d32e38ba50476260f7d5b4fac6afd16471
  Branch:    release-3.3.0 (uncommited files present)
  Location:  Kind.checkTUser.checkModuleParam
  Message:   Unexpected parameters
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.3.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:394:10 in cryptol-3.3.0-inplace:Cryptol.TypeCheck.Kind
%< --------------------------------------------------- 

[yav]

Thanks! This is not supposed to work---aparently we forgot to check that the kinds of parameters are limited to # and * (i.e., no kind functions in parameters)

[j-christensen1]

Ah! I figured it may not be supported.