GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Add implcit imports for modules defined by instantiation #1691

Closed yav closed 4 months ago

yav commented 4 months ago

Consider the following example:


module M where

submodule A where
  x = 2

submodule F where
  parameter
    a: Integer

   z = a + 5

submodule B = submodule F {submodule  A }

This defines 3 submodules, 2 normal ones and a functor. At the moment we add implicit imports for simple modules, such as A, but not ones defined by instantiation (e.g., B).

I think it'd be more consistent to also add an import for B. We still can't add implicit imports for things inside B, because at this stage we don't know what F is, and therefore we can't tell what it defines (so we don't know what to import)