Lift newtypes from a TCon to a full-fledged constructor

of `Type`.  This allows us to directly carry the `Newtype`
instead of having to look it up in a table at use sites.

cryptol-remote-api/src/CryptolServer/Data/Type.hs

@@ -211,6 +211,8 @@ instance JSON.ToJSON JSONType where
         , "name" .= show (ppWithNames ns v)
         ]
       convert (TUser _n _args def) = convert def
+      convert (TNewtype nt ts) =
+        error "JSON conversion of newtypes is not yet supported TODO"
       convert (TRec fields) =
         JSON.object
         [ "type" .= T.pack "record"

src/Cryptol/Eval.hs

@@ -269,8 +269,14 @@ evalNewtypeDecl ::
   SEval sym (GenEvalEnv sym)
 evalNewtypeDecl _sym nt = pure . bindVarDirect (ntName nt) (foldr tabs con (ntParams nt))
   where
-  tabs _tp body = PTyPoly (\ _ -> body)
   con           = PFun PPrim
+
+  tabs tp body =
+    case tpKind tp of
+      KType -> PTyPoly  (\ _ -> body)
+      KNum  -> PNumPoly (\ _ -> body)
+      k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show (pp k)]
+
 {-# INLINE evalNewtypeDecl #-}
 
 
@@ -382,6 +388,7 @@ isValueType ntEnv env Forall{ sVars = [], sProps = [], sType = t0 }
   go (TVSeq _ x)  = go x
   go (TVTuple xs) = and (map go xs)
   go (TVRec xs)   = and (fmap go xs)
+  go (TVNewtype _ _ xs) = and (fmap go xs)
   go _            = False
 
 isValueType _ _ _ = False

src/Cryptol/Eval/Concrete.hs

@@ -80,12 +80,14 @@ toExpr prims t0 v0 = findOne (go t0 v0)
              Left _ -> mismatch -- different fields
              Right efs -> pure (ERec efs)
 
-      (TVNewtype (UserTC nm _) _ tfs, VRecord vfs) ->
+      (TVNewtype nt ts tfs, VRecord vfs) ->
         do -- NB, vfs first argument to keep their display order
            res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs
            case res of
              Left _ -> mismatch -- different fields
-             Right efs -> pure (EApp (EVar nm) (ERec efs))
+             Right efs ->
+               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts
+                in pure (EApp f (ERec efs))
 
       (TVTuple ts, VTuple tvs) ->
         do guard (length ts == length tvs)

src/Cryptol/Eval/Type.hs

@@ -39,7 +39,8 @@ data TValue
   | TVTuple [TValue]          -- ^ @ (a, b, c )@
   | TVRec (RecordMap Ident TValue) -- ^ @ { x : a, y : b, z : c } @
   | TVFun TValue TValue       -- ^ @ a -> b @
-  | TVNewtype UserTC [Either Nat' TValue]
+  | TVNewtype Newtype
+              [Either Nat' TValue]
               (RecordMap Ident TValue)     -- ^ a named newtype
   | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type
     deriving (Generic, NFData, Eq)
@@ -59,14 +60,15 @@ tValTy tv =
     TVTuple ts  -> tTuple (map tValTy ts)
     TVRec fs    -> tRec (fmap tValTy fs)
     TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)
-    TVNewtype u vs _ -> tNewtype u (map arg vs)
-    TVAbstract u vs -> tAbstract u (map arg vs)
+    TVNewtype nt vs _ -> tNewtype nt (map tNumValTy vs)
+    TVAbstract u vs -> tAbstract u (map tNumValTy vs)
 
- where
-   arg x = case x of
-             Left Inf     -> tInf
-             Left (Nat n) -> tNum n
-             Right v      -> tValTy v
+tNumTy :: Nat' -> Type
+tNumTy Inf     = tInf
+tNumTy (Nat n) = tNum n
+
+tNumValTy :: Either Nat' TValue -> Type
+tNumValTy = either tNumTy tValTy
 
 
 instance Show TValue where
@@ -126,6 +128,10 @@ evalType ntEnv env ty =
 
     TUser _ _ ty'  -> evalType ntEnv env ty'
     TRec fields    -> Right $ TVRec (fmap val fields)
+
+    TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody ntEnv env nt tvs
+        where tvs = map (evalType ntEnv env) ts
+
     TCon (TC c) ts ->
       case (c, ts) of
         (TCBit, [])     -> Right $ TVBit
@@ -141,16 +147,6 @@ evalType ntEnv env ty =
         (TCTuple _, _)  -> Right $ TVTuple (map val ts)
         (TCNum n, [])   -> Left $ Nat n
         (TCInf, [])     -> Left $ Inf
-        (TCNewtype u@(UserTC nm _),vs) ->
-            case Map.lookup nm ntEnv of
-              Just nt ->
-                let vs' = map (evalType ntEnv env) vs
-                 in Right $ TVNewtype u vs' $ evalNewtypeBody ntEnv env nt vs'
-              Nothing -> evalPanic "evalType"
-                            [ "Unknown newtype"
-                            , "*** Name: " ++ show (pp nm)
-                            ]
-
         (TCAbstract u,vs) ->
             case kindOf ty of
               KType -> Right $ TVAbstract u (map (evalType ntEnv env) vs)

src/Cryptol/IR/FreeVars.hs

@@ -140,18 +140,15 @@ instance FreeVars Type where
 
       TUser _ _ t -> freeVars t
       TRec fs     -> freeVars (recordElements fs)
-
+      TNewtype nt ts -> freeVars nt <> freeVars ts
 
 instance FreeVars TVar where
   freeVars tv = case tv of
                   TVBound p -> mempty { tyParams = Set.singleton p }
                   _         -> mempty
 
 instance FreeVars TCon where
-  freeVars tc =
-    case tc of
-     TC (TCNewtype (UserTC n _)) -> mempty { tyDeps = Set.singleton n }
-     _ -> mempty
+  freeVars _tc = mempty
 
 instance FreeVars Newtype where
   freeVars nt = foldr rmTParam base (ntParams nt)

src/Cryptol/ModuleSystem/InstantiateModule.hs

@@ -244,6 +244,7 @@ instance Inst Type where
       TUser x ts t  -> TUser y (inst env ts) (inst env t)
         where y = Map.findWithDefault x x (tyNameMap env)
       TRec fs       -> TRec (fmap (inst env) fs)
+      TNewtype nt ts -> TNewtype (inst env nt) (inst env ts)
 
 instance Inst TCon where
   inst env tc =
@@ -254,7 +255,6 @@ instance Inst TCon where
 instance Inst TC where
   inst env tc =
     case tc of
-      TCNewtype x  -> TCNewtype (inst env x)
       TCAbstract x -> TCAbstract (inst env x)
       _            -> tc
 

src/Cryptol/Parser.y

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

src/Cryptol/Symbolic.hs

@@ -55,7 +55,7 @@ import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.Eval.Value
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Solver.InfNat
-import           Cryptol.Eval.Type (TValue(..), evalType,NewtypeEnv,tValTy)
+import           Cryptol.Eval.Type (TValue(..), evalType,NewtypeEnv,tValTy,tNumValTy)
 import           Cryptol.Utils.Ident (Ident,prelPrim,floatPrim)
 import           Cryptol.Utils.RecordMap
 import           Cryptol.Utils.Panic
@@ -145,7 +145,7 @@ data FinType
     | FTSeq Integer FinType
     | FTTuple [FinType]
     | FTRecord (RecordMap Ident FinType)
-    | FTNewtype UserTC [Either Nat' TValue] (RecordMap Ident FinType)
+    | FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType)
 
 finType :: TValue -> Maybe FinType
 finType ty =
@@ -321,11 +321,13 @@ varToExpr prims = go
   go :: FinType -> VarShape Concrete.Concrete -> Expr
   go ty val =
     case (ty,val) of
-      (FTNewtype (UserTC nm _) _ tfs, VarRecord vfs) ->
+      (FTNewtype nt ts tfs, VarRecord vfs) ->
         let res = zipRecords (\_lbl v t -> go t v) vfs tfs
          in case res of
               Left _ -> mismatch -- different fields
-              Right efs -> EApp (EVar nm) (ERec efs)
+              Right efs ->
+                let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts
+                 in EApp f (ERec efs)
 
       (FTRecord tfs, VarRecord vfs) ->
         let res = zipRecords (\_lbl v t -> go t v) vfs tfs

src/Cryptol/Transform/AddModParams.hs

@@ -289,16 +289,12 @@ instance Inst Type where
         where ts1 = inst ps ts
               t1  = inst ps t
 
-      TCon tc ts ->
-        case tc of
-          TC (TCNewtype (UserTC x k))
-            | needsInst ps x -> TCon (TC (TCNewtype (UserTC x (k1 k))))
-                                     (newTs ++ ts1)
-          _ -> TCon tc ts1
-        where
-        ts1 = inst ps ts
-        newTs = instTyParams ps
-        k1 k = foldr (:->) k (map kindOf newTs)
+      TNewtype nt ts
+        | needsInst ps (ntName nt) -> TNewtype (inst ps nt) (instTyParams ps ++ ts1)
+        | otherwise -> TNewtype nt ts1
+        where ts1 = inst ps ts
+
+      TCon tc ts -> TCon tc (inst ps ts)
 
       TVar x | Just x' <- isTParam ps x -> TVar (TVBound x')
              | otherwise  -> ty

src/Cryptol/TypeCheck/CheckModuleInstance.hs

@@ -112,7 +112,7 @@ checkTyParams func inst =
            src = CtPartialTypeFun nm
        mapM_ (newGoal src) (ntConstraints nt)
 
-       return (tp, TCon (TC (TCNewtype (UserTC nm k2))) [])
+       return (tp, TNewtype nt [])
 
   -- Check that a type parameter defined as another type parameter is OK
   checkTP tp tp1 =

src/Cryptol/TypeCheck/Kind.hs

@@ -261,10 +261,9 @@ checkTUser x ts k =
        checkKind (TUser x ts1 t1) k k1
 
   checkNewTypeUse nt =
-    do let tc = newtypeTyCon nt
-       (ts1,_) <- appTy ts (kindOf tc)
+    do (ts1,_) <- appTy ts (kindOf nt)
        ts2 <- checkParams (ntParams nt) ts1
-       return (TCon tc ts2)
+       return (TNewtype nt ts2)
 
   checkAbstractTypeUse absT =
     do let tc   = abstractTypeTC absT

src/Cryptol/TypeCheck/Sanity.hs

@@ -68,6 +68,10 @@ checkType ty =
       do ks <- mapM checkType ts
          checkKind (kindOf tc) ks
 
+    TNewtype nt ts ->
+      do ks <- mapM checkType ts
+         checkKind (kindOf nt) ks
+
     TVar tv -> lookupTVar tv
 
     TRec fs ->
@@ -369,6 +373,12 @@ convertible t1 t2 = go t1 t2
                                | tc1 == tc2 -> goMany ts1 ts2
                             _ -> err
 
+         TNewtype nt1 ts1 ->
+            case other of
+              TNewtype nt2 ts2
+                | nt1 == nt2 -> goMany ts1 ts2
+              _ -> err
+
          TRec fs ->
            case other of
              TRec gs ->

src/Cryptol/TypeCheck/SimpType.hs

@@ -19,6 +19,7 @@ tRebuild' withUser = go
         | otherwise -> go t
       TVar _        -> ty
       TRec xs       -> TRec (fmap go xs)
+      TNewtype nt xs -> TNewtype nt (map go xs)
       TCon tc ts    -> tCon tc (map go ts)
 
 tRebuild :: Type -> Type

src/Cryptol/TypeCheck/Solver/Selector.hs

@@ -10,7 +10,7 @@ module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where
 
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.InferTypes
-import Cryptol.TypeCheck.Monad( InferM, unify, newGoals, lookupNewtype
+import Cryptol.TypeCheck.Monad( InferM, unify, newGoals
                               , newType, applySubst, solveHasGoal
                               , newParamName
                               )
@@ -66,21 +66,18 @@ solveSelector sel outerT =
 
     (RecordSel l _, ty) ->
       case ty of
-        TRec fs  -> return (lookupField l fs)
+        TRec fs -> return (lookupField l fs)
+        TNewtype nt ts ->
+          case lookupField l (ntFields nt) of
+            Nothing -> return Nothing
+            Just t ->
+              do let su = listParamSubst (zip (ntParams nt) ts)
+                 newGoals (CtPartialTypeFun (ntName nt))
+                   $ apSubst su $ ntConstraints nt
+                 return $ Just $ apSubst su t
+
         TCon (TC TCSeq) [len,el] -> liftSeq len el
         TCon (TC TCFun) [t1,t2]  -> liftFun t1 t2
-        TCon (TC (TCNewtype (UserTC x _))) ts ->
-          do mb <- lookupNewtype x
-             case mb of
-               Nothing -> return Nothing
-               Just nt ->
-                 case lookupField l (ntFields nt) of
-                   Nothing -> return Nothing
-                   Just t  ->
-                     do let su = listParamSubst (zip (ntParams nt) ts)
-                        newGoals (CtPartialTypeFun x)
-                          $ apSubst su $ ntConstraints nt
-                        return $ Just $ apSubst su t
         _ -> return Nothing
 
     (TupleSel n _, ty) ->

src/Cryptol/TypeCheck/Solver/Utils.hs

@@ -22,6 +22,7 @@ splitVarSummands ty0 = [ (x,t1) | (x,t1) <- go ty0, tNum (0::Int) /= t1 ]
   go ty = case ty of
             TVar x      -> return (x, tNum (0::Int))
             TRec {}     -> []
+            TNewtype{}  -> []
             TUser _ _ t -> go t
             TCon (TF TCAdd) [t1,t2] ->
               do (a,yes) <- go t1
@@ -45,6 +46,7 @@ splitConstSummand ty =
   case ty of
     TVar {}     -> Nothing
     TRec {}     -> Nothing
+    TNewtype{}  -> Nothing
     TUser _ _ t -> splitConstSummand t
     TCon (TF TCAdd) [t1,t2] ->
       do (k,t1') <- splitConstSummand t1
@@ -63,6 +65,7 @@ splitConstFactor ty =
   case ty of
     TVar {}     -> Nothing
     TRec {}     -> Nothing
+    TNewtype{}  -> Nothing
     TUser _ _ t -> splitConstFactor t
     TCon (TF TCMul) [t1,t2] ->
       do (k,t1') <- splitConstFactor t1

src/Cryptol/TypeCheck/Subst.hs

@@ -240,7 +240,8 @@ apSubstMaybe su ty =
       do (ts1, t1) <- anyJust2 (anyJust (apSubstMaybe su)) (apSubstMaybe su) (ts, t)
          Just (TUser f ts1 t1)
 
-    TRec fs       -> TRec `fmap` (anyJust (apSubstMaybe su) fs)
+    TRec fs -> TRec `fmap` (anyJust (apSubstMaybe su) fs)
+    TNewtype nt ts -> TNewtype nt `fmap` anyJust (apSubstMaybe su) ts
     TVar x -> applySubstToVar su x
 
 lookupSubst :: TVar -> Subst -> Maybe Type
@@ -315,6 +316,7 @@ apSubstTypeMapKeys su = go (\_ x -> x) id
     tm' = TM { tvar = Map.fromList   vars
              , tcon = fmap (lgo merge atNode) tcon
              , trec = fmap (lgo merge atNode) trec
+             , tnewtype = fmap (lgo merge atNode) tnewtype
              }
 
     -- partition out variables that have been replaced with more specific types

src/Cryptol/TypeCheck/TCon.hs

@@ -142,7 +142,6 @@ instance HasKind TC where
       TCSeq     -> KNum :-> KType :-> KType
       TCFun     -> KType :-> KType :-> KType
       TCTuple n -> foldr (:->) KType (replicate n KType)
-      TCNewtype x -> kindOf x
       TCAbstract x -> kindOf x
 
 instance HasKind PC where
@@ -237,7 +236,6 @@ data TC     = TCNum Integer            -- ^ Numbers
             | TCFun                    -- ^ @_ -> _@
             | TCTuple Int              -- ^ @(_, _, _)@
             | TCAbstract UserTC        -- ^ An abstract type
-            | TCNewtype UserTC         -- ^ user-defined, @T@
               deriving (Show, Eq, Ord, Generic, NFData)
 
 
@@ -337,7 +335,6 @@ instance PP TC where
       TCTuple 0 -> text "()"
       TCTuple 1 -> text "(one tuple?)"
       TCTuple n -> parens $ hcat $ replicate (n-1) comma
-      TCNewtype u -> pp u
       TCAbstract u -> pp u
 
 instance PP UserTC where