From 31cd9fea436ad7ef8b70966d4645106075b5f214 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Thu, 22 Jul 2021 14:40:52 +0300
Subject: [PATCH] The types of module parameters use constraints

Fixes #1240
---
 src/Cryptol/ModuleSystem/Renamer.hs | 7 ++++++-
 tests/issues/issue1240.cry          | 8 ++++++++
 tests/issues/issue1240.icry         | 1 +
 tests/issues/issue1240.icry.stdout  | 3 +++
 4 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/issues/issue1240.cry
 create mode 100644 tests/issues/issue1240.icry
 create mode 100644 tests/issues/issue1240.icry.stdout

diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
index 0b13eeb77..aabbe6d9a 100644
--- 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
new file mode 100644
index 000000000..46191f4e6
--- /dev/null
+++ 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
new file mode 100644
index 000000000..740955ca8
--- /dev/null
+++ 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
new file mode 100644
index 000000000..eb41aed59
--- /dev/null
+++ b/tests/issues/issue1240.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test