Foreign imports don't seem to be able to access global type variables

[weaversa]

Full example here: https://github.com/weaversa/cryptol-ffi-tests

foreign sha384 : {tmp, b} (tmp == a, fin b, b == 384/8) => [a][8] -> [b][8]

/*
shatest_8> sha384 "12345678"
cryptol-osx: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  e261894654ceb3736f8de4a671f4cafc38ed6eba
  Branch:    master (uncommited files present)
  Location:  [Eval] evalType
  Message:   type variable not bound
             TVBound (TParam {tpUnique = 4669, tpKind = KNum, tpFlav = TPModParam (Name {nUnique = 4669, nInfo = Declared (TopModule (ModName "shatest")) UserName, nNamespace = NSType, nI\
dent = Ident False "a", nFixity = Nothing, nLoc = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}}), tpInfo = TVarInfo {tvarSource\
 = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}, tvarDesc = TVFromModParam (Name {nUnique = 4669, nInfo = Declared (TopModule (\
ModName "shatest")) UserName, nNamespace = NSType, nIdent = Ident False "a", nFixity = Nothing, nLoc = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, sourc\
e = "./shatest.cry"}})}})
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-2.13.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Type.hs:130:20 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Type
%< ---------------------------------------------------

[yav]

The FFI and guarded constraints don't work with the old module system implementation, but should work correctly on the functors-merge branch.

The status of that is that I don't know of any outstanding bugs, and I am not planning on implementing any more new features until the branch is merged---we can of course continue tweaking things and making it more convenient to use as we gain experience with it. The main blocker for merging it, is that I'd like to make sure that the algorithms in cryptol-specs work with the new module system. The reason some might not work (besides unknown bugs) are that there are 2 features of the old module system that are not supported in the new module system:

1. The "backtick" imports: these are the imports that instantiate a functor by adding the module parameters to all definitions. We decided against supporting that as it is a whole new flavor of module system---historically we implemented both styles of instantiation to see which might be more useful
2. "Functor composition": this is the part where you are instantiating a module, but the result is also a functor (e.g., module A = B where ... and the ... themselves have parameters). This one should not be hard to implement with the new module system, but we decided to postpone it for now, until we see a) if it is commonly used, and b) what's a reasonable syntax for it, as there were concerns that the old notation is kind of confusing as the resulting functor's parameters are in the argument to the functor being instantiated.

[yav]

I should clarify that the way this works (FFI interaction with nested modules/functors) in the new module system has some restrictions:

• FFI declarations may NOT appear in functors. So the above example "works" in the sense that you'd get a nicer error rather than a panic. The reason for that is that it is not at all clear what it would mean to "instantiate" a foreign declaration, as we have no way to change the external code to adapt it to the instantiation
• FFI declarations MAY appear in nested (non-functor) modules, but with the restriction that there is only a single FFI declaration with a given name in the whole file---the reason for that is to keep the mapping between Cryptol and external names simple