Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[New module system] newtype out of order crash #1511

Closed
WeeknightMVP opened this issue Mar 28, 2023 · 0 comments
Closed

[New module system] newtype out of order crash #1511

WeeknightMVP opened this issue Mar 28, 2023 · 0 comments

Comments

@WeeknightMVP
Copy link

module M where

v: [1]
v = MOOD.SAD.value                // crashes unless newtype is declared above (regardless of where fields are)
// v = (MOOD.SAD : MOOD_t).value  // works no matter where newtype and fields are

newtype MOOD_t = { value: [1] }

MOOD = { HAPPY = MOOD_t { value = 0b1 }
       , SAD   = MOOD_t { value = 0b0 } }

The above module crashes when trying to load in functors-merge:

$ ./cry run
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0.99 (9b63a18, modified)
https://cryptol.net  :? for help

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

%< ---------------------------------------------------
  Revision:  9b63a18044e0861a05a3c91213b6d383b2289911
  Branch:    functors-merge (uncommited files present)
  Location:  lookupVar
  Message:   Undefined vairable
             Name {nUnique = 5244, nInfo = GlobalName UserName (OrigName {ogNamespace = NSValue, ogModule = TopModule (ModName "M" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "MOOD_t"}), nFixity = Nothing, nL\
oc = Range {from = Position {line = 6, col = 9}, to = Position {line = 6, col = 15}, source = ".../M.cry"}}
             IVARS
             Cryptol::number_4701
             Cryptol::demote_4702
             Cryptol::length_4703
             Cryptol::fromTo_4704
             Cryptol::fromToLessThan_4705
...
             Cryptol::zip_4831
             Cryptol::zipWith_4832
             Cryptol::uncurry_4833
             Cryptol::curry_4834
             Cryptol::iterate_4835
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/TypeCheck/Monad.hs:776:20 in cryptol-2.13.0.99-inplace:Cryptol.TypeCheck.Monad
%< ---------------------------------------------------

Explicitly coercing the constant to the newtype, moving the newtype declaration to precede it, or loading the module in main branch Cryptol works as expected.

@yav yav closed this as completed in 05412e9 Jun 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant