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

Numeric Constraint Guards Throw Error in Parameterized Modules #1486

Closed
mariosge opened this issue Dec 23, 2022 · 1 comment
Closed

Numeric Constraint Guards Throw Error in Parameterized Modules #1486

mariosge opened this issue Dec 23, 2022 · 1 comment

Comments

@mariosge
Copy link

Even though Numeric Constraint Guards look to be working properly in a non-parameterized module, a bug appears in parameterized ones.

How to reproduce:

  1. Contents of spec.cry:
module spec = parameterized where

type m = 1
  1. Contents of parameterized.cry:
module parameterized where

parameter
    type m : #

len : {n} (fin n) => [n] -> Integer
len xs | n == 0 => 0
       | n >  0 => 1 + len (drop `{1} xs)
  1. Run $ cryptol spec.cry

  2. Outcome:

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

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  inst
  Message:   This is not implemented for EPropGuards yet.
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptl-2.13.0.99-324846d2:Cryptol.Utils.Panic
  panic, called at src/Cryptol/ModuleSystem/InstantiateModule.hs:222:36 in cryptl-2.13.0.99-324846d2:Cryptol.ModuleSystem.InstantiateModule
%< --------------------------------------------------- 

I built Cryptol from source using commit: 953673b.
ghc version: 8.10.7
cabal version: 3.6.2.0

@yav
Copy link
Member

yav commented Dec 23, 2022

Ah yes, this works with the new module system (PR: #1363)

@yav yav closed this as completed Aug 10, 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