From e5251eef980e201d3fa9f55b881cc142f325427c Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Wed, 31 Jan 2024 11:21:39 -0800
Subject: [PATCH] Add nominal type constructors in scope.

Fixes #1617
---
 src/Cryptol/TypeCheck/Sanity.hs    | 15 ++++++++++++---
 tests/issues/issue1617.cry         |  8 ++++++++
 tests/issues/issue1617.icry        |  2 ++
 tests/issues/issue1617.icry.stdout |  8 ++++++++
 4 files changed, 30 insertions(+), 3 deletions(-)
 create mode 100644 tests/issues/issue1617.cry
 create mode 100644 tests/issues/issue1617.icry
 create mode 100644 tests/issues/issue1617.icry.stdout

diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs
index e8008fbfe..fb850f6a4 100644
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@@ -51,6 +51,8 @@ tcModule env m = case runTcM env check of
   where check = foldr withTVar k1 (map mtpParam (Map.elems (mParamTypes m)))
         k1    = foldr withAsmp k2 (map thing (mParamConstraints m))
         k2    = withVars (Map.toList (fmap mvpType (mParamFuns m)))
+              $ withVars (concatMap nominalTypeConTypes
+                                                (Map.elems (mNominalTypes m)))
               $ checkDecls (mDecls m)
 
 onlyNonTrivial :: [ProofObligation] -> [ProofObligation]
@@ -575,9 +577,16 @@ runTcM env (TcM m) =
                                       , let x = mtpParam tp ]
           , roAsmps = map thing (mpnConstraints allPs)
           , roRange = emptyRange
-          , roVars  = Map.union
-                        (fmap mvpType (mpnFuns allPs))
-                        (inpVars env)
+          , roVars  = Map.unions
+                        [ fmap mvpType (mpnFuns allPs)
+                        , inpVars env
+                        , Map.fromList
+                            [ c
+                            | nt <- Map.elems (inpNominalTypes env)
+                            , c  <- nominalTypeConTypes nt
+                            ]
+                        ]
+
           }
   rw = RW { woProofObligations = [] }
 
diff --git a/tests/issues/issue1617.cry b/tests/issues/issue1617.cry
new file mode 100644
index 000000000..908009fa3
--- /dev/null
+++ b/tests/issues/issue1617.cry
@@ -0,0 +1,8 @@
+// Bar.cry
+newtype T = { unT : [8] }
+enum M = A | B
+
+f : T
+f = T { unT = 0 }
+
+g = A
diff --git a/tests/issues/issue1617.icry b/tests/issues/issue1617.icry
new file mode 100644
index 000000000..051d2a104
--- /dev/null
+++ b/tests/issues/issue1617.icry
@@ -0,0 +1,2 @@
+:set coreLint=true
+:load issue1617.cry
diff --git a/tests/issues/issue1617.icry.stdout b/tests/issues/issue1617.icry.stdout
new file mode 100644
index 000000000..1732b7f8f
--- /dev/null
+++ b/tests/issues/issue1617.icry.stdout
@@ -0,0 +1,8 @@
+Loading module Cryptol
+Loading module Cryptol
+{n, a, b, c} n == min n n
+{a, n} (fin n) => inf == inf * (1 * (1 * 1))
+{a, n} (fin n) => n / 2 == n - n /^ 2
+{n, a, b} n == min n n
+{n} (n >= 1, fin n) => (fin n, n >= 1)
+Loading module Main