Merge pull request #1245 from GaloisInc/T1240

The types of module parameters use constraints
GaloisInc · Jul 22, 2021 · e78195a · e78195a
2 parents 5b21f36 + 31cd9fe
commit e78195a
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 1 deletion.
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -256,7 +256,12 @@ renameTopDecls' info ds =
       TDNewtype {}            -> False
       DParameterType {}       -> False
       DParameterConstraint {} -> False
-      DParameterFun {}        -> False
+
+      DParameterFun {}        -> True
+      -- Here we may need the constraints to validate the type
+      -- (e.g., if the parameter is of type `Z a`)
+
+
       DModule tl              -> any usesCtrs (mDecls m)
         where NestedModule m = tlValue tl
       DImport {}              -> False

diff --git a/tests/issues/issue1240.cry b/tests/issues/issue1240.cry
@@ -0,0 +1,8 @@
+module test where
+
+parameter
+
+  type a : #
+  type constraint (fin a, a >= 1)
+
+  b : Z a
diff --git a/tests/issues/issue1240.icry b/tests/issues/issue1240.icry
@@ -0,0 +1 @@
+:load issue1240.cry
diff --git a/tests/issues/issue1240.icry.stdout b/tests/issues/issue1240.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test