diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 7abfd4e72f..1f26acca70 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -297,9 +297,12 @@ mkCryEnv env = (types, _) <- liftModuleM modEnv $ do prims <- MB.getPrimMap - -- noIfaceParams because we don't support translating functors yet - TM.inpVars `fmap` MB.genInferInput P.emptyRange prims - MI.noIfaceParams ifaceDecls + infInp <- MB.genInferInput P.emptyRange prims MI.noIfaceParams ifaceDecls + let newtypeCons = Map.fromList + [ (T.ntName nt, T.newtypeConType nt) + | nt <- Map.elems (TM.inpNewtypes infInp) + ] + pure (newtypeCons `Map.union` TM.inpVars infInp) let types' = Map.union (eExtraTypes env) types let terms = eTermEnv env let cryEnv = C.emptyEnv diff --git a/intTests/test_1870/A.cry b/intTests/test_1870/A.cry new file mode 100644 index 0000000000..cd9a5e814c --- /dev/null +++ b/intTests/test_1870/A.cry @@ -0,0 +1,4 @@ +module A where + +newtype A = { x : [8] } + diff --git a/intTests/test_1870/test.saw b/intTests/test_1870/test.saw new file mode 100644 index 0000000000..5986959782 --- /dev/null +++ b/intTests/test_1870/test.saw @@ -0,0 +1,5 @@ +import "A.cry"; + +// Make sure that `newtypes` work. +// Specifically, that `A` is in scope. +print {{ A { x = 2 } }};