Add nominal type constructors in scope.

Fixes #1617

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 = [] }
 

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

tests/issues/issue1617.icry

@@ -0,0 +1,2 @@
+:set coreLint=true
+:load issue1617.cry

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