Regression (Undefined vairable) in program that uses submodules, functors, and interfaces

[RyanGlScott]

Given the following Cryptol files:

// BInterface.cry
interface module BInterface where

type BTy : *

// BFunctor.cry
module BFunctor where

import interface BInterface as BI

type BTy = BI::BTy

b : BTy -> ()
b _ = ()

// A.cry
module A where

submodule B = BFunctor where
  type BTy = ()

// Test.cry
module Test where

import A as A
import submodule A::B as B

The following works with Cryptol 3.1.0:

$ ~/Software/cryptol-3.1.0/bin/cryptol Test.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.1.0
https://cryptol.net  :? for help

Loading module Cryptol
Loading interface module BInterface
Loading module BFunctor
Loading module A
Loading module Test
Test> B::b ()
()

But not with the master branch of Cryptol:

$ cabal run exe:cryptol -- Test.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.1.0.99 (19ebc25, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading interface module BInterface
Loading module BFunctor
Loading module A
Loading module Test
Test> B::b ()
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  19ebc256f88c30c68526268ba55b51a6d61405ed
  Branch:    master (uncommited files present)
  Location:  lookupVar
  Message:   Undefined vairable
             Name {nUnique = 4686, nInfo = GlobalName UserName (OrigName {ogNamespace = NSValue, ogModule = Nested (TopModule (ModName "A" NormalName)) (Ident False NormalName "B"), ogSource = FromFunctorInst, ogName = Ident False NormalName "b", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 9, col = 1}, to = Position {line = 9, col = 2}, source = "./BFunctor.cry"}}
             IVARS
             Cryptol::number_4128
             Cryptol::demote_4129
             Cryptol::length_4130
             Cryptol::fromTo_4131
             Cryptol::fromToLessThan_4132
             Cryptol::fromToBy_4133
             Cryptol::fromToByLessThan_4134
             Cryptol::fromToDownBy_4135
             Cryptol::fromToDownByGreaterThan_4136
             Cryptol::fromThenTo_4137
             Cryptol::fraction_4139
             Cryptol::zero_4141
             (Cryptol::&&_4143)
             (Cryptol::||_4144)
             (Cryptol::^_4145)
             Cryptol::complement_4146
             Cryptol::fromInteger_4148
             (Cryptol::+_4149)
             (Cryptol::-_4150)
             (Cryptol::*_4151)
             Cryptol::negate_4152
             (Cryptol::/_4154)
             (Cryptol::%_4155)
             Cryptol::toInteger_4156
             (Cryptol::^^_4157)
             Cryptol::infFrom_4158
             Cryptol::infFromThen_4159
             Cryptol::recip_4161
             (Cryptol::/._4162)
             Cryptol::ceiling_4164
             Cryptol::floor_4165
             Cryptol::trunc_4166
             Cryptol::roundAway_4167
             Cryptol::roundToEven_4168
             (Cryptol::==_4170)
             (Cryptol::!=_4171)
             (Cryptol::===_4172)
             (Cryptol::!==_4173)
             (Cryptol::<_4175)
             (Cryptol::>_4176)
             (Cryptol::<=_4177)
             (Cryptol::>=_4178)
             Cryptol::min_4179
             Cryptol::max_4180
             Cryptol::abs_4181
             (Cryptol::<$_4183)
             (Cryptol::>$_4184)
             (Cryptol::<=$_4185)
             (Cryptol::>=$_4186)
             Cryptol::None_4188
             Cryptol::Some_4189
             Cryptol::Ok_4191
             Cryptol::Err_4192
             Cryptol::True_4193
             Cryptol::False_4194
             (Cryptol::/\_4195)
             (Cryptol::\/_4196)
             (Cryptol::==>_4197)
             (Cryptol::/$_4198)
             (Cryptol::%$_4199)
             Cryptol::carry_4200
             Cryptol::scarry_4201
             Cryptol::sborrow_4202
             Cryptol::zext_4203
             Cryptol::sext_4204
             (Cryptol::>>$_4205)
             Cryptol::lg2_4206
             Cryptol::toSignedInteger_4207
             Cryptol::ratio_4208
             Cryptol::fromZ_4209
             (Cryptol::#_4210)
             Cryptol::splitAt_4211
             Cryptol::join_4212
             Cryptol::split_4213
             Cryptol::reverse_4214
             Cryptol::transpose_4215
             Cryptol::take_4216
             Cryptol::drop_4217
             Cryptol::tail_4218
             Cryptol::head_4219
             Cryptol::last_4220
             Cryptol::groupBy_4221
             (Cryptol::<<_4222)
             (Cryptol::>>_4223)
             (Cryptol::<<<_4224)
             (Cryptol::>>>_4225)
             (Cryptol::@_4226)
             (Cryptol::@@_4227)
             (Cryptol::!_4228)
             (Cryptol::!!_4229)
             Cryptol::update_4230
             Cryptol::updateEnd_4231
             Cryptol::updates_4232
             Cryptol::updatesEnd_4233
             Cryptol::generate_4234
             Cryptol::sort_4235
             Cryptol::sortBy_4236
             Cryptol::pmult_4237
             Cryptol::pdiv_4238
             Cryptol::pmod_4239
             Cryptol::parmap_4240
             Cryptol::deepseq_4241
             Cryptol::rnf_4242
             Cryptol::error_4243
             Cryptol::undefined_4244
             Cryptol::assert_4245
             Cryptol::random_4246
             Cryptol::trace_4247
             Cryptol::traceVal_4248
             Cryptol::and_4249
             Cryptol::or_4250
             Cryptol::all_4251
             Cryptol::any_4252
             Cryptol::map_4253
             Cryptol::foldl_4254
             Cryptol::foldl'_4255
             Cryptol::foldr_4256
             Cryptol::foldr'_4257
             Cryptol::sum_4258
             Cryptol::product_4259
             Cryptol::scanl_4260
             Cryptol::scanr_4261
             Cryptol::repeat_4262
             Cryptol::elem_4263
             Cryptol::zip_4264
             Cryptol::zipWith_4265
             Cryptol::uncurry_4266
             Cryptol::curry_4267
             Cryptol::iterate_4268
             BFunctor::b_4680
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Monad.hs:775:20 in cryptol-3.1.0.99-inplace:Cryptol.TypeCheck.Monad
%< --------------------------------------------------- 

The commit which introduced this regression is 19ebc25 (Only grab public IfaceDecls from other modules.).

Aside from the panic itself, the message in the panic has a typo: Undefined vairable should be Undefined variable.

[RyanGlScott]

cc @mccleeary-galois @yav

[RyanGlScott]

@mccleeary-galois has offered to look into this in #1650. If the fix proves non-trivial, we can consider reverting the changes from #1642 (which introduced this regression) for the time being.

[yav]

Hm, I was wondering if something like this might happen (due to the comment in the definition of ModContext) . I suspect that the correct fix here would be to revert the change form #1642, and instead look at the use sites to see why private things were appearing at the REPL.

More generally, we really need to come up with a reasonable model of what we want to be in scope on the REPL. Other related issues to this one are: #689, #998, #1382, #1553

[mccleeary-galois]

Reverting and reopening #1642 and adding test for this in PR.