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] (^^) crashes on unqualified exponent in inter-module function instantiation #1510

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

Comments

@WeeknightMVP
Copy link

In functors-merge, Cryptol crashes when trying to coerce an unqualified exponent for (^^) in a functor instantiation across modules. (Whether parameters are used is not relevant to the crash.)

// F.cry
module F where

parameter
  type n: #

submodule S where
  parameter
    type m: #

  x : Integer
  x = 0 ^^ 1  // crashes
  // x = 0 ^^ (1 : Integer)  // works

// T.cry
module T where

import F where
  type n = 1

import submodule S where
  type m = 1
$ ./cry run
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0.99 (9b63a18, modified)
Cryptol> :m T
Loading module Cryptol
Loading interface module `parameter` interface of F
Loading module F
Loading module T
T> x
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:  [Eval] expV
  Message:   TCon (TC TCBit) [] not int class `Integral`
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/Generic.hs:528:16 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Generic
%< ---------------------------------------------------

Explicitly qualifying the exponent as an Integer works as expected, as does evaluating the expression outside a nested submodule...

// G.cry
module G where
  parameter
    type n: #

  x : Integer
  x = 0 ^^ 1  // works

// U.cry
module U where

import G where
  type n = 1
$ ./cry run
...
Cryptol> 0 ^^ 1 : Integer
0
Cryptol> :m U
Loading module Cryptol
Loading interface module `parameter` interface of G
Loading module G
Loading module U
U> x
0

... or doing all of the above in a single module.

// X.cry
module X where

submodule S where
  parameter
    type n: #

  submodule S' where
    parameter
      type m: #

    x : Integer
    x = 0 ^^ 1  // works

import submodule S where
  type n = 1

import submodule S' where
  type m = 1
$ ./cry run
...
Cryptol> :m X
Loading module Cryptol
Loading module X
X> x
0
yav added a commit that referenced this issue Mar 28, 2023
yav added a commit that referenced this issue Mar 28, 2023
@yav yav closed this as completed Mar 29, 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

2 participants