Parameterized function types + other crash

parameterized.cry:

module parameterized where                                                                                                          
parameter                                                                                                                           
  type A : #                                                                                                                        
  type B : #                                                                                                                        
                                                                                                                                    
  f : [A] -> [B]

instantiation.cry:

module instantiation = parameterized where                                                                                          
  type A = 2                                                                                                                        
  type B = 2                                                                                                                        
                                                                                                                                    
  f x = x

I expected this to make f monomorphic, e.g. as f : [2] -> [2], but it loads as:

$ cryptol-2.7.0-CentOS7-64/bin/cryptol
version 2.7.0

Loading module Cryptol
Cryptol> :l instantiation.cry
Loading module Cryptol
Loading module parameterized
Loading module instantiation
instantiation> :t f
f : {a} a -> a

With other definitions of f appropriate for the A and B set in the instantiation, I get more polymorphic types that seem to be inferred from the function's definition instead of using the type declared in the parameterized module, f : [A] -> [B].

While trying other definitions, I also encountered the following crash.
parameterized.cry: as above
crash.cry: (note the incorrect definitions of A and B)

module crash = parameterized where                                                                                                  
  A = 2                                                                                                                             
  B = 2                                                                                                                             
                                                                                                                                    
  f x = take`{2} x

This will cause the crash:

$ cryptol-2.7.0-CentOS7-64/bin/cryptol
version 2.7.0

Loading module Cryptol
Cryptol> :l crash.cry
Loading module Cryptol
Loading module parameterized
Loading module crash
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  Cryptol.TypeCheck.Monad.extendSubst
  Message:   Escaped quantified variables:
             Substitution:  ?crash::f_1`850 := parameterized::A - 2
             Vars in scope: []
             Escaped:       [parameterized::A]
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Monad.hs:559:16 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.TypeCheck.Monad
%< ---------------------------------------------------

$

However, using other definitions of f sometimes only produces errors.

[yav]

Thanks for reporting this, there's definitely something wrong with the instantiation of value parameters.

We don't have much documentation on parameterized modules, as the current design was a bit of an experiment, so we may want to still tweak it in various way. Here are a couple of things that might be confusing:

1. The parameters of a module are not considered to be definitions in the module---in particular, they are not exported by the module. So a module like parameterized is a bit odd as it does not define anything. If you wanted to have a parameterized module that exports its parameters you'd have to add definitions to do so manually. For example:

module P where 
parameter type ParamA : # 

// This type has the same value as the parameter and will be exported
type A = ParamA    

2. The definitions inside an instantiating module, such as crash for example, are only there to help define the parameters, and are not themselves exported by the instantiated module, which defines the exact same set of names as the parameterized module.

[yav]

I had a look at this, and it doesn't crash anymore, I suspect some of the previous fixes to the module system have fixed that bug.

As to why f is not monomorphic: when instantiation is loaded at the command line, we see what's in scope of the instantiation, not the instantiated module, which might be a bit confusing. With the new module system design we are a lot more explicit about things like that, so I think we can close this.