REPL panics when attempting to evaluate function in focused, parameterized submodule #1989
Description
Given the following Cryptol file:
// Bug.cry
interface submodule I where
type T : *
submodule M where
import interface submodule I
b : Bit
b = True
Note that b is defined in a parameterized submodule M, but its type does not depend on the type T in any way. What happens if we try to evaluate b? If you try to do so using Cryptol 3.5.0, you'll get a lookupVar panic that is very similar to the one reported in #1872:
Details
$ ~/Software/cryptol-3.5.0/bin/cryptol Bug.cry -c ":focus submodule M" -c ":eval b"
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
%< ---------------------------------------------------
Revision: 6173b60ad40822a1563ea4f569b04a70806b67fd
Branch: release-3.5.0 (uncommited files present)
Location: lookupVar
Message: Undefined variable
Name {nUnique = 4681, nInfo = GlobalName UserName (OrigName {ogNamespace = NSValue, ogModule = Nested (TopModule (ModMain "Bug.cry")) (Ident False NormalName "M"), ogSource = FromDefinition, ogName = Ident False NormalName "b", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {pLine = 10, pCol = 3, pColOffset = 2}, to = Position {pLine = 10, pCol = 4, pColOffset = 3}, source = "Bug.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
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.5.0-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/TypeCheck/Monad.hs:787:20 in cryptol-3.5.0-inplace:Cryptol.TypeCheck.Monad
%< ---------------------------------------------------
#1988 will partially address this, but even after the changes from #1988, the program above will still cause Cryptol to panic. After the changes from #1988, it will instead trigger an evalExpr panic. Here is the panic that you get with the native evaluator:
Details
$ cabal -v0 run exe:cryptol -- Bug.cry -c ":focus submodule M" -c "b"
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
%< ---------------------------------------------------
Revision: bc4889367e0463907fc8446d58e945e1fa061563
Branch: issue1872 (uncommited files present)
Location: [Eval] evalExpr
Message: var `Main::M::b` (4681) is not defined
[4128 <<prim>> 4129 -> <polymorphic value>
4130 -> <polymorphic value> 4131 <<prim>> 4132 <<prim>>
4133 <<prim>> 4134 <<prim>> 4135 <<prim>> 4136 <<prim>>
4137 <<prim>> 4139 <<prim>> 4141 <<prim>> 4143 <<prim>>
4144 <<prim>> 4145 <<prim>> 4146 <<prim>> 4148 <<prim>>
4149 <<prim>> 4150 <<prim>> 4151 <<prim>> 4152 <<prim>>
4154 <<prim>> 4155 <<prim>> 4156 <<prim>> 4157 <<prim>>
4158 <<prim>> 4159 <<prim>> 4161 <<prim>> 4162 <<prim>>
4164 <<prim>> 4165 <<prim>> 4166 <<prim>> 4167 <<prim>>
4168 <<prim>> 4170 <<prim>> 4171 <<prim>>
4172 -> <polymorphic value> 4173 -> <polymorphic value>
4175 <<prim>> 4176 <<prim>> 4177 <<prim>> 4178 <<prim>>
4179 -> <polymorphic value> 4180 -> <polymorphic value>
4181 -> <polymorphic value> 4183 <<prim>>
4184 -> <polymorphic value> 4185 -> <polymorphic value>
4186 -> <polymorphic value> 4188 <<prim>> 4189 <<prim>>
4191 <<prim>> 4192 <<prim>> 4193 <<prim>> 4194 <<prim>>
4195 -> <function> 4196 -> <function> 4197 -> <function>
4198 <<prim>> 4199 <<prim>> 4200 -> <polymorphic value>
4201 -> <polymorphic value> 4202 -> <polymorphic value>
4203 -> <polymorphic value> 4204 -> <polymorphic value>
4205 <<prim>> 4206 <<prim>> 4207 <<prim>> 4208 <<prim>>
4209 <<prim>> 4210 <<prim>> 4211 -> <polymorphic value>
4212 <<prim>> 4213 <<prim>> 4214 <<prim>> 4215 <<prim>>
4216 <<prim>> 4217 <<prim>> 4218 -> <polymorphic value>
4219 -> <polymorphic value> 4220 -> <polymorphic value>
4221 -> <polymorphic value> 4222 <<prim>> 4223 <<prim>>
4224 <<prim>> 4225 <<prim>> 4226 <<prim>>
4227 -> <polymorphic value> 4228 <<prim>>
4229 -> <polymorphic value> 4230 <<prim>> 4231 <<prim>>
4232 -> <polymorphic value> 4233 -> <polymorphic value>
4234 -> <polymorphic value> 4235 -> <polymorphic value>
4236 -> <polymorphic value> 4237 <<prim>> 4238 <<prim>>
4239 <<prim>> 4240 <<prim>> 4241 <<prim>>
4242 -> <polymorphic value> 4243 <<prim>>
4244 -> <polymorphic value> 4245 -> <polymorphic value>
4246 <<prim>> 4247 <<prim>> 4248 -> <polymorphic value>
4249 -> <polymorphic value> 4250 -> <polymorphic value>
4251 -> <polymorphic value> 4252 -> <polymorphic value>
4253 -> <polymorphic value> 4254 <<prim>> 4255 <<prim>>
4256 -> <polymorphic value> 4257 -> <polymorphic value>
4258 -> <polymorphic value> 4259 -> <polymorphic value>
4260 <<prim>> 4261 -> <polymorphic value>
4262 -> <polymorphic value> 4263 -> <polymorphic value>
4264 -> <polymorphic value> 4265 -> <polymorphic value>
4266 -> <polymorphic value> 4267 -> <polymorphic value>
4268 -> <polymorphic value>]
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.5.0.99-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/Eval.hs:197:9 in cryptol-3.5.0.99-inplace:Cryptol.Eval
%< ---------------------------------------------------
And here is the panic that you get with the reference evaluator:
Details
$ cabal -v0 run exe:cryptol -- Bug.cry -c ":focus submodule M" -c ":eval b"
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
%< ---------------------------------------------------
Revision: bc4889367e0463907fc8446d58e945e1fa061563
Branch: issue1872 (uncommited files present)
Location: [Reference Evaluator]evalExpr
Message: var `Main::M::b` is not defined
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.5.0.99-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/Eval/Reference.lhs:1960:19 in cryptol-3.5.0.99-inplace:Cryptol.Eval.Reference
%< ---------------------------------------------------
I think that at the very least, attempting to evaluate b should result in an error message like the one seen in #1623 (i.e., Expression depends on definitions from a parameterized module).