Have a go at fixing #1483

This is also fixes some longstanding tech debt where we were reusing the
name for the type of a newtype and the constructor of a newtype

src/Cryptol/Eval.hs

@@ -319,7 +319,7 @@ evalNewtypeDecl ::
   Newtype ->
   GenEvalEnv sym ->
   SEval sym (GenEvalEnv sym)
-evalNewtypeDecl _sym nt = pure . bindVarDirect (ntName nt) (foldr tabs con (ntParams nt))
+evalNewtypeDecl _sym nt = pure . bindVarDirect (ntConName nt) (foldr tabs con (ntParams nt))
   where
   con           = PFun PPrim
 

src/Cryptol/Eval/Concrete.hs

@@ -87,7 +87,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
            case res of
              Left _ -> mismatch -- different fields
              Right efs ->
-               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts
+               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts
                 in pure (EApp f (ERec efs))
 
       (TVTuple ts, VTuple tvs) ->

src/Cryptol/Eval/Reference.lhs

@@ -545,7 +545,7 @@ newtypes is thus basically just an identity function
 that consumes and ignores its type arguments.
 
 > evalNewtypeDecl :: Env -> Newtype -> Env
-> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env
+> evalNewtypeDecl env nt = bindVar (ntConName nt, pure val) env
 >   where
 >     val = foldr tabs con (ntParams nt)
 >     con = VFun (\x -> x)

src/Cryptol/IR/TraverseNames.hs

@@ -209,14 +209,16 @@ instance TraverseNames Newtype where
   traverseNamesIP nt = mk <$> traverseNamesIP (ntName nt)
                           <*> traverseNamesIP (ntParams nt)
                           <*> traverseNamesIP (ntConstraints nt)
+                          <*> traverseNamesIP (ntConName nt)
                           <*> traverseRecordMap (\_ -> traverseNamesIP)
                                                 (ntFields nt)
     where
-    mk a b c d = nt { ntName = a
-                    , ntParams = b
-                    , ntConstraints = c
-                    , ntFields = d
-                    }
+    mk a b c d e = nt { ntName = a
+                      , ntParams = b
+                      , ntConstraints = c
+                      , ntConName = d
+                      , ntFields = e
+                      }
 
 instance TraverseNames ModTParam where
   traverseNamesIP nt = mk <$> traverseNamesIP (mtpName nt)

src/Cryptol/ModuleSystem/Binds.hs

@@ -359,15 +359,13 @@ instance BindsNames (InModule (ParameterType PName)) where
        ntName <- newTop NSType ns thing Nothing srcRange
        return (singletonNS NSType thing ntName)
 
--- NOTE: we use the same name at the type and expression level, as there's only
--- ever one name introduced in the declaration. The names are only ever used in
--- different namespaces, so there's no ambiguity.
 instance BindsNames (InModule (Newtype PName)) where
   namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $
     do let Located { .. } = nName
-       ntName <- newTop NSType ns thing Nothing srcRange
-       -- XXX: the name reuse here is sketchy
-       return (singletonNS NSType thing ntName `mappend` singletonNS NSValue thing ntName)
+       ntName    <- newTop NSType  ns thing Nothing srcRange
+       ntConName <- newTop NSValue ns thing Nothing srcRange
+       return (singletonNS NSType thing ntName `mappend`
+               singletonNS NSValue thing ntConName)
 
 -- | The naming environment for a single declaration.
 instance BindsNames (InModule (Decl PName)) where

src/Cryptol/ModuleSystem/Exports.hs

@@ -11,7 +11,7 @@ import Control.DeepSeq(NFData)
 import GHC.Generics (Generic)
 
 import Cryptol.Parser.AST
-import Cryptol.Parser.Names(namesD,tnamesD,tnamesNT)
+import Cryptol.Parser.Names(namesD,tnamesD,namesNT,tnamesNT)
 import Cryptol.ModuleSystem.Name
 
 exportedDecls :: Ord name => [TopDecl name] -> ExportSpec name
@@ -23,7 +23,8 @@ exportedNames decl =
       Decl td -> map exportBind  (names  namesD td)
               ++ map exportType (names tnamesD td)
       DPrimType t -> [ exportType (thing . primTName <$> t) ]
-      TDNewtype nt -> map exportType (names tnamesNT nt)
+      TDNewtype nt -> map exportType (names tnamesNT nt) ++
+                      map exportBind (names namesNT nt)
       Include {}  -> []
       DImport {} -> []
       DParamDecl {} -> []

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -264,8 +264,14 @@ unqualifiedEnv IfaceDecls { .. } =
   tySyns  = mconcat [ singletonNS NSType (toPName n) n
                     | n <- Map.keys ifTySyns ]
 
-  ntTypes = mconcat [ singletonNS NSType (toPName n) n
-                    | n <- Map.keys ifNewtypes ]
+  ntTypes = mconcat [ n
+                    | nt <- Map.elems ifNewtypes
+                    , let tname = T.ntName nt
+                          cname = T.ntConName nt
+                    , n  <- [ singletonNS NSType (toPName tname) tname
+                            , singletonNS NSValue (toPName cname) cname
+                            ]
+                    ]
 
   absTys  = mconcat [ singletonNS NSType (toPName n) n
                     | n <- Map.keys ifAbstractTypes ]

src/Cryptol/ModuleSystem/Renamer.hs

@@ -873,11 +873,14 @@ instance Rename Decl where
 instance Rename Newtype where
   rename n      =
     shadowNames (nParams n) $
-    do name' <- rnLocated (renameType NameBind) (nName n)
-       depsOf (NamedThing (thing name')) $
+    do nameT <- rnLocated (renameType NameBind) (nName n)
+       nameC <- renameVar  NameBind (nConName n)
+
+       depsOf (NamedThing (thing nameT)) $
          do ps'   <- traverse rename (nParams n)
             body' <- traverse (traverse rename) (nBody n)
-            return Newtype { nName   = name'
+            return Newtype { nName   = nameT
+                           , nConName = nameC
                            , nParams = ps'
                            , nBody   = body' }
 

src/Cryptol/Parser.y

@@ -467,9 +467,9 @@ propguards_quals                   :: { [Located (Prop PName)] }
 
 newtype                 :: { Newtype PName }
   : 'newtype' qname '=' newtype_body
-                           { Newtype $2 [] (thing $4) }
+                           { Newtype $2 [] (thing $2) (thing $4) }
   | 'newtype' qname tysyn_params '=' newtype_body
-                           { Newtype $2 (reverse $3) (thing $5) }
+                           { Newtype $2 (reverse $3) (thing $2) (thing $5) }
 
 newtype_body            :: { Located (RecordMap Ident (Range, Type PName)) }
   : '{' '}'                {% mkRecord (rComb $1 $2) (Located emptyRange) [] }

src/Cryptol/Parser/AST.hs

@@ -490,10 +490,12 @@ data Pragma   = PragmaNote String
               | PragmaProperty
                 deriving (Eq, Show, Generic, NFData)
 
-data Newtype name = Newtype { nName   :: Located name        -- ^ Type name
-                            , nParams :: [TParam name]       -- ^ Type params
-                            , nBody   :: Rec (Type name)     -- ^ Body
-                            } deriving (Eq, Show, Generic, NFData)
+data Newtype name = Newtype
+  { nName     :: Located name        -- ^ Type name
+  , nParams   :: [TParam name]       -- ^ Type params
+  , nConName  :: !name               -- ^ Constructor function name
+  , nBody     :: Rec (Type name)     -- ^ Body
+  } deriving (Eq, Show, Generic, NFData)
 
 -- | A declaration for a type with no implementation.
 data PrimType name = PrimType { primTName :: Located name
@@ -1440,9 +1442,10 @@ instance NoPos (Decl name) where
       DLocated   x _   -> noPos x
 
 instance NoPos (Newtype name) where
-  noPos n = Newtype { nName   = noPos (nName n)
-                    , nParams = nParams n
-                    , nBody   = fmap noPos (nBody n)
+  noPos n = Newtype { nName     = noPos (nName n)
+                    , nParams   = nParams n
+                    , nConName  = nConName n
+                    , nBody     = fmap noPos (nBody n)
                     }
 
 instance NoPos (Bind name) where

src/Cryptol/Parser/Names.hs

@@ -20,6 +20,7 @@ module Cryptol.Parser.Names
   , tnamesD
   , namesB
   , namesP
+  , namesNT
 
   , boundNames
   , boundNamesSet
@@ -35,6 +36,9 @@ import qualified Data.Set as Set
 tnamesNT :: Newtype name -> ([Located name], ())
 tnamesNT x = ([ nName x ], ())
 
+namesNT :: Newtype name -> ([Located name], ())
+namesNT x = ([ (nName x) { thing = nConName x } ], ())
+
 -- | The names defined and used by a group of mutually recursive declarations.
 namesDs :: Ord name => [Decl name] -> ([Located name], Set name)
 namesDs ds = (defs, boundLNames defs (Set.unions frees))

src/Cryptol/Symbolic.hs

@@ -349,7 +349,7 @@ varToExpr prims = go
          in case res of
               Left _ -> mismatch -- different fields
               Right efs ->
-                let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts
+                let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts
                  in EApp f (ERec efs)
 
       (FTRecord tfs, VarRecord vfs) ->

src/Cryptol/TypeCheck/Interface.hs

@@ -38,6 +38,7 @@ genModDefines m =
   Set.unions
     [ Map.keysSet  (mTySyns m)
     , Map.keysSet  (mNewtypes m)
+    , Set.fromList (map ntConName (Map.elems (mNewtypes m)))
     , Map.keysSet  (mPrimTypes m)
     , Set.fromList (map dName (concatMap groupDecls (mDecls m)))
     , Map.keysSet  (mSubmodules m)

src/Cryptol/TypeCheck/Kind.hs

@@ -135,7 +135,7 @@ checkPropSyn (P.PropSyn x _ as ps) mbD =
 -- | Check a newtype declaration.
 -- XXX: Do something with constraints.
 checkNewtype :: P.Newtype Name -> Maybe Text -> InferM Newtype
-checkNewtype (P.Newtype x as fs) mbD =
+checkNewtype (P.Newtype x as con fs) mbD =
   do ((as1,fs1),gs) <- collectGoals $
        inRange (srcRange x) $
        do r <- withTParams NoWildCards newtypeParam as $
@@ -147,6 +147,7 @@ checkNewtype (P.Newtype x as fs) mbD =
      return Newtype { ntName   = thing x
                     , ntParams = as1
                     , ntConstraints = map goal gs
+                    , ntConName = con
                     , ntFields = fs1
                     , ntDoc = mbD
                     }

src/Cryptol/TypeCheck/ModuleInstance.hs

@@ -9,7 +9,6 @@ import qualified Data.Set as Set
 import Cryptol.Parser.Position(Located)
 import Cryptol.ModuleSystem.Interface(IfaceNames(..))
 import Cryptol.IR.TraverseNames(TraverseNames,mapNames)
-import Cryptol.Parser.AST(ImpName(..))
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)
 
@@ -97,6 +96,7 @@ instance ModuleInstance Newtype where
     Newtype { ntName        = moduleInstance (ntName nt)
             , ntParams      = ntParams nt
             , ntConstraints = moduleInstance (ntConstraints nt)
+            , ntConName     = moduleInstance (ntConName nt)
             , ntFields      = moduleInstance <$> ntFields nt
             , ntDoc         = ntDoc nt
             }

src/Cryptol/TypeCheck/Monad.hs

@@ -56,7 +56,7 @@ import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
 import qualified Cryptol.TypeCheck.SimpleSolver as Simple
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import           Cryptol.TypeCheck.PP(NameMap)
-import           Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets)
+import           Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets,debugShowUniques)
 import           Cryptol.Utils.Ident(Ident,Namespace(..),ModName)
 import           Cryptol.Utils.Panic(panic)
 
@@ -129,7 +129,10 @@ runInferM info m0 =
      let allPs = inpParams info
 
      let env = Map.map ExtVar (inpVars info)
-            <> Map.map (ExtVar . newtypeConType) (inpNewtypes info)
+            <> Map.fromList
+              [ (ntConName nt, ExtVar (newtypeConType nt))
+              | nt <- Map.elems (inpNewtypes info)
+              ]
             <> Map.map (ExtVar . mvpType) (mpnFuns allPs)
 
      let ro =         RO { iRange     = inpRange info
@@ -774,7 +777,7 @@ lookupVar x =
                    panic "lookupVar" $ [ "Undefined vairable"
                                      , show x
                                      , "IVARS"
-                                     ] ++ map (show . pp) (Map.keys mp)
+                                     ] ++ map (show . debugShowUniques . pp) (Map.keys mp)
 
 -- | Lookup a type variable.  Return `Nothing` if there is no such variable
 -- in scope, in which case we must be dealing with a type constant.
@@ -1150,7 +1153,7 @@ addTySyn t =
 addNewtype :: Newtype -> InferM ()
 addNewtype t =
   do updScope \r -> r { mNewtypes = Map.insert (ntName t) t (mNewtypes r) }
-     IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntName t)
+     IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntConName t)
                                                     (newtypeConType t)
                                                     (iBindTypes rw) }
 

src/Cryptol/TypeCheck/Type.hs

@@ -315,6 +315,7 @@ data TySyn  = TySyn { tsName        :: Name       -- ^ Name
 data Newtype  = Newtype { ntName   :: Name
                         , ntParams :: [TParam]
                         , ntConstraints :: [Prop]
+                        , ntConName :: !Name
                         , ntFields :: RecordMap Ident Type
                         , ntDoc :: Maybe Text
                         } deriving (Show, Generic, NFData)