diff --git a/design/WhitePaper.md b/design/WhitePaper.md
index 9fdf062f14e..93fcf317d0e 100644
--- a/design/WhitePaper.md
+++ b/design/WhitePaper.md
@@ -159,6 +159,60 @@ Finally, it would sometimes be desirable to have extended syntax for multi-line
 The Motoko type system has a number of known gaps that stand in the way of certain forms of abstraction and composition.
 
 
+#### Newtypes
+
+Motoko supports `newtype` declarations that introduce a nominal wrapper around an existing type.
+Unlike `type` aliases (which are structurally transparent), a `newtype` is fully opaque: no implicit conversion exists between the newtype and its underlying representation.
+
+```
+newtype Time = Int;
+let t : Time = Time(123);    // explicit wrapping via constructor
+let n : Int = t.unwrap;      // explicit unwrapping via .unwrap
+```
+
+The declaration introduces both a type `Time` and a value `Time` — the constructor function of type `Int -> Time`.
+
+Newtypes can have type parameters.
+Variance of each type parameter is computed from its usage in the right-hand side, consistent with how `type` aliases work:
+
+```
+newtype Map<K, V> = MapInternals<K, V>;
+let m : Map<Text, Nat> = Map<Text, Nat>(internal);
+let i = m.unwrap;  // : MapInternals<Text, Nat>
+```
+
+##### Semantics
+
+- **Opacity.** A newtype `T` and its underlying type `U` are distinct for subtyping and equality. `T </: U` and `U </: T`. Values must be explicitly wrapped/unwrapped.
+- **Zero-cost.** At runtime, newtype values have the same representation as the underlying type. The constructor and `.unwrap` are identity operations.
+- **Nominal.** Two newtypes with the same underlying type are distinct: `newtype A = Int` and `newtype B = Int` produce incompatible types.
+- **Constructor.** The newtype name is bound as both a type and a value (the constructor function). For `newtype T<A> = U<A>`, the constructor has type `<A>(U<A>) -> T<A>`.
+- **Unwrap.** Values of newtype are given a virtual `.unwrap` field (analogous to how arrays have `.size`). For a value `v : T<A>`, `v.unwrap : U<A>`.
+
+##### Candid Serialization
+
+Newtypes are a Motoko-only concept. When serializing to Candid, newtypes are transparent: `Time` serializes as `Int`, `Map<K, V>` serializes as its underlying record type.
+
+##### Stable Storage and Migrations
+
+For `.most` files (stable type signatures), newtypes are treated like type aliases. This allows users to freely add, rename, or remove newtypes across upgrades without breaking migration compatibility.
+
+Newtypes are preserved in error messages (e.g., `Time` rather than `Int`) for better diagnostics.
+
+##### Implementation
+
+The `newtype` declaration introduces a new type constructor kind `Newtype(binds, body)` alongside the existing `Def` (transparent alias) and `Abs` (abstract/parameter). Key design choices:
+
+- **`normalize`** does *not* expand `Newtype`, preserving opacity during type checking. This is the fundamental difference from `Def`.
+- **`promote`** does *not* expand `Newtype`, preventing implicit promotion in subtyping contexts.
+- **Lowering.** During desugaring, `Newtype` kinds are mutated to `Def`, making them transparent for downstream IR passes and codegen. The constructor is emitted as an identity function binding.
+
+##### Future Work
+
+- Pattern matching on newtypes.
+- Methods on newtypes.
+
+
 #### Type Fields ([#760](https://github.com/dfinity/motoko/issues/760))
 
 Motoko allows type members in objects and modules:
diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt
index 0b6e0633b1f..b21d66fd0af 100644
--- a/doc/md/examples/grammar.txt
+++ b/doc/md/examples/grammar.txt
@@ -335,6 +335,7 @@
 <dec_nonvar> ::= 
     'let' <pat> '=' <exp>
     'type' <id> ('<' <list(<typ_bind>, ',')> '>')? '=' <typ>
+    'newtype' <id> ('<' <list(<typ_bind>, ',')> '>')? '=' <typ>
     <shared_pat_opt> 'func' <func_pat> (':' <typ>)? <func_body>
     <parenthetical>? <obj_or_class_dec>
     'mixin' <pat_plain> <obj_body>
diff --git a/src/docs/extract.ml b/src/docs/extract.ml
index 3e5411a753f..5e099d8907d 100644
--- a/src/docs/extract.ml
+++ b/src/docs/extract.ml
@@ -224,7 +224,7 @@ struct
                   } )
         | _ -> Some (mk_xref (Xref.XValue name), extract_value_doc Var rhs name)
         )
-    | Source.{ it = Syntax.TypD (name, ty_args, typ); _ } ->
+    | Source.{ it = Syntax.TypD (name, ty_args, typ) | Syntax.NewtypeD (name, ty_args, typ); _ } ->
         let doc_typ =
           match typ.it with
           | Syntax.ObjT (_, fields) ->
diff --git a/src/docs/namespace.ml b/src/docs/namespace.ml
index 7b0014f9480..c2d661bc3d0 100644
--- a/src/docs/namespace.ml
+++ b/src/docs/namespace.ml
@@ -54,7 +54,8 @@ let from_module =
                   (StringMap.of_seq (List.to_seq bound_names))
                   acc.values;
             }
-        | Syntax.TypD (id, _, _) ->
+        | Syntax.TypD (id, _, _)
+        | Syntax.NewtypeD (id, _, _) ->
             {
               acc with
               types = StringMap.add id.it (mk_xref (Xref.XType id.it)) acc.types;
diff --git a/src/gen-grammar/grammar.sed b/src/gen-grammar/grammar.sed
index 404c5d8e9d3..96f92771fa7 100644
--- a/src/gen-grammar/grammar.sed
+++ b/src/gen-grammar/grammar.sed
@@ -52,6 +52,7 @@ s/VAR/\'var\'/g
 s/SHROP/\' >>\'/g
 s/SHRASSIGN/\'>>=\'/g
 s/UNDERSCORE/\'_\'/g
+s/NEWTYPE/\'newtype\'/g
 s/TYPE/\'type\'/g
 s/TRANSIENT/\'transient\'/g
 s/TRY/\'try\'/g
diff --git a/src/ir_def/check_ir.ml b/src/ir_def/check_ir.ml
index b3100c2315a..e79d7250cca 100644
--- a/src/ir_def/check_ir.ml
+++ b/src/ir_def/check_ir.ml
@@ -197,7 +197,8 @@ let rec check_typ env typ : unit =
     List.iter (check_typ env) typs;
     begin
       match Cons.kind c with
-      | T.Def (tbs,_) ->
+      | T.Def (tbs,_)
+      | T.Newtype (tbs,_) ->
         check_con env c;
         check_typ_bounds env tbs typs no_region
       | T.Abs (tbs, _) ->
@@ -288,7 +289,7 @@ and check_con env c =
   else
   begin
     env.seen := T.ConSet.add c !(env.seen);
-    let T.Abs (binds,typ) | T.Def (binds, typ) = Cons.kind c in
+    let T.Abs (binds,typ) | T.Def (binds, typ) | T.Newtype (binds, typ) = Cons.kind c in
     check env no_region (not (T.is_mut typ)) "type constructor RHS is_mut";
     let cs, ce = check_typ_binds env binds in
     let ts = List.map (fun c -> T.Con (c, [])) cs in
diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml
index 1c695fab6d4..00df2711d0a 100644
--- a/src/ir_passes/async.ml
+++ b/src/ir_passes/async.ml
@@ -221,6 +221,8 @@ let transform prog =
       Abs (t_binds typ_binds, t_typ typ)
     | Def (typ_binds,typ) ->
       Def (t_binds typ_binds, t_typ typ)
+    | Newtype (typ_binds,typ) ->
+      Newtype (t_binds typ_binds, t_typ typ)
 
   and t_con c =
     match Cons.kind c with
diff --git a/src/ir_passes/erase_typ_field.ml b/src/ir_passes/erase_typ_field.ml
index 9788f1977dc..fd8b2919cc6 100644
--- a/src/ir_passes/erase_typ_field.ml
+++ b/src/ir_passes/erase_typ_field.ml
@@ -68,6 +68,8 @@ let transform prog =
       T.Abs (t_binds typ_binds, t_typ typ)
     | T.Def (typ_binds,typ) ->
       T.Def (t_binds typ_binds, t_typ typ)
+    | T.Newtype (typ_binds,typ) ->
+      T.Newtype (t_binds typ_binds, t_typ typ)
 
   and t_con c =
     match Cons.kind c with
diff --git a/src/js/astjs.ml b/src/js/astjs.ml
index 485ab356169..c424fc2c159 100644
--- a/src/js/astjs.ml
+++ b/src/js/astjs.ml
@@ -550,6 +550,10 @@ module Make (Cfg : Config) = struct
         to_js_object "TypD"
           ([ id x ] @ List.map typ_bind_js tp @ [ syntax_typ_js t ]
           |> Array.of_list)
+    | NewtypeD (x, tp, t) ->
+        to_js_object "NewtypeD"
+          ([ id x ] @ List.map typ_bind_js tp @ [ syntax_typ_js t ]
+          |> Array.of_list)
     | ClassD (eo, sp, s, x, tp, p, rt, i, dfs) ->
         to_js_object "ClassD"
           (parenthetical eo
diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml
index 67cc21ccb42..7f44e01b27e 100644
--- a/src/lowering/desugar.ml
+++ b/src/lowering/desugar.ml
@@ -121,6 +121,8 @@ and exp' at note = function
     (blob_dotE x.it (exp e)).it
   | S.DotE (e, x, _) when T.is_prim T.Text e.note.S.note_typ ->
     (text_dotE x.it (exp e)).it
+  | S.DotE (e, x, _) when x.it = "unwrap" && T.is_con e.note.S.note_typ -> (* TODO: the kind changed to Def in this T.Con, extract `is_newtype` function and document this *)
+    (exp e).it (* Newtype .unwrap is identity *)
   | S.DotE (e, x, _) ->
     begin match T.as_obj_sub [x.it] e.note.S.note_typ with
     | T.Actor, _ -> I.PrimE (I.ActorDotPrim x.it, [exp e])
@@ -616,7 +618,7 @@ and export_runtime_information self_id =
   [{ it = I.{ name = lab; var = v }; at = no_region; note = typ }])
 
 and build_stabs (df : S.dec_field) : stab option list = match df.it.S.dec.it with
-  | S.TypD _ -> []
+  | S.TypD _ | S.NewtypeD _ -> []
   | S.MixinD _ -> assert false
   | S.IncludeD(_, arg, note) ->
     (* TODO: This is ugly. It would be a lot nicer if we didn't have to split
@@ -998,6 +1000,33 @@ and dec' d =
     end
   | S.VarD (i, e) -> [I.VarD (i.it, e.note.S.note_typ, exp e)]
   | S.TypD _ -> []
+  | S.NewtypeD (id, binds, _) ->
+    let c = Option.get id.note in
+    let tbs_closed, t_body_closed = match Cons.kind c with
+    | T.Newtype (tbs, t) ->
+      (* Mutate Newtype kind to Def so downstream IR/codegen sees a transparent alias *)
+      Cons.unsafe_set_kind c (T.Def (tbs, t));
+      tbs, t
+    | _ -> assert false
+    in
+    (* Build polymorphic identity function type for the newtype constructor *)
+    let tbs' = typ_binds binds in
+    let vars = List.map (fun (tb : I.typ_bind) -> T.Con (tb.it.I.con, [])) tbs' in
+    let inner_t = T.open_ vars t_body_closed in
+    let newtype_ret = T.Con (c, vars) in
+    let type_var_args = List.mapi (fun i tb -> T.Var (tb.T.var, i)) tbs_closed in
+    let ctor_typ = T.Func (T.Local, T.Returns, tbs_closed, [t_body_closed], [T.Con (c, type_var_args)]) in
+    (* Build identity function binding for the newtype constructor *)
+    let arg_var = fresh_var "x" inner_t in
+    let arg = { it = id_of_var arg_var; at = no_region; note = inner_t } in
+    let ctor_body = varE arg_var in
+    let ctor_func =
+      { it = I.FuncE (id.it, T.Local, T.Returns, tbs', [arg], [newtype_ret], ctor_body);
+        at = no_region;
+        note = Note.{ def with typ = ctor_typ } }
+    in
+    let ctor_pat = { it = I.VarP id.it; at = no_region; note = ctor_typ } in
+    [I.LetD (ctor_pat, ctor_func)]
   | S.MixinD _ -> []
   | S.IncludeD(_, args, note) ->
     let { imports = is; pat = p; decs } = Option.get !note in
diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml
index 0c067aca143..09b57f78786 100644
--- a/src/mo_def/arrange.ml
+++ b/src/mo_def/arrange.ml
@@ -284,6 +284,8 @@ module Make (Cfg : Config) = struct
     | VarD (x, e) -> "VarD" $$ [id x; exp e]
     | TypD (x, tp, t) ->
       "TypD" $$ [id x] @ List.map typ_bind tp @ [typ t]
+    | NewtypeD (x, tp, t) ->
+      "NewtypeD" $$ [id x] @ List.map typ_bind tp @ [typ t]
     | ClassD (eo, sp, s, x, tp, p, rt, i, dfs) ->
       "ClassD" $$
         parenthetical eo
diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml
index b7252d8781d..e50a21985e1 100644
--- a/src/mo_def/syntax.ml
+++ b/src/mo_def/syntax.ml
@@ -259,6 +259,7 @@ and dec' =
   | LetD of pat * exp * exp option             (* immutable, with an optional fail block *)
   | VarD of id * exp                           (* mutable *)
   | TypD of typ_id * typ_bind list * typ       (* type *)
+  | NewtypeD of typ_id * typ_bind list * typ   (* newtype *)
   | ClassD of                                  (* class *)
       exp option * sort_pat * obj_sort * typ_id * typ_bind list * pat * typ option * id * dec_field list
   | MixinD of pat * dec_field list             (* mixin *)
diff --git a/src/mo_frontend/bi_match.ml b/src/mo_frontend/bi_match.ml
index 34df6e98fa8..f6d6b8eadaa 100644
--- a/src/mo_frontend/bi_match.ml
+++ b/src/mo_frontend/bi_match.ml
@@ -296,6 +296,8 @@ let bi_match_typs ctx =
         bi_match_typ rel eq inst any (open_ ts1 t) t2
       | _, Def (tbs, t) -> (* TBR this may fail to terminate *)
         bi_match_typ rel eq inst any t1 (open_ ts2 t)
+      | Newtype _, Newtype _ when Cons.eq con1 con2 ->
+        bi_match_list bi_equate_typ rel eq inst any ts1 ts2
       | _ when Cons.eq con1 con2 ->
         assert (ts1 = []);
         assert (ts2 = []);
diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml
index a7fc48fd836..b3de44f0128 100644
--- a/src/mo_frontend/definedness.ml
+++ b/src/mo_frontend/definedness.ml
@@ -184,7 +184,7 @@ and dec msgs d = match d.it with
   | LetD (p, e, None) -> pat msgs p +++ exp msgs e
   | LetD (p, e, Some f) -> pat msgs p +++ exp msgs e +++ exp msgs f
   | VarD (i, e) -> (M.empty, S.singleton i.it) +++ exp msgs e
-  | TypD (i, tp, t) -> (M.empty, S.empty)
+  | TypD (i, tp, t) | NewtypeD (i, tp, t) -> (M.empty, S.empty)
   | ClassD (eo, csp, s, i, tp, p, t, i', dfs) ->
      ((M.empty, S.singleton i.it) +++
      (* TBR: treatment of eo *)
diff --git a/src/mo_frontend/effect.ml b/src/mo_frontend/effect.ml
index e0785f49536..e374b768b65 100644
--- a/src/mo_frontend/effect.ml
+++ b/src/mo_frontend/effect.ml
@@ -147,7 +147,7 @@ and infer_effect_dec dec =
   | LetD (_, e, None)
   | VarD (_, e) ->
     effect_exp e
-  | TypD _
+  | TypD _ | NewtypeD _
   | ClassD _
   | MixinD _
   | IncludeD _ ->
diff --git a/src/mo_frontend/error_reporting.ml b/src/mo_frontend/error_reporting.ml
index ba8c2ba303f..ac03f2dd102 100644
--- a/src/mo_frontend/error_reporting.ml
+++ b/src/mo_frontend/error_reporting.ml
@@ -138,4 +138,5 @@ let terminal2token (type a) (symbol : a terminal) : token =
       | T_WRAPMULASSIGN -> WRAPMULASSIGN
       | T_WRAPPOWASSIGN -> WRAPPOWASSIGN
       | T_PIPE -> PIPE
+      | T_NEWTYPE -> NEWTYPE
       | T_WEAK -> WEAK
diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly
index 3bbb9f23b75..4ff83c5bc10 100644
--- a/src/mo_frontend/parser.mly
+++ b/src/mo_frontend/parser.mly
@@ -225,7 +225,7 @@ and objblock eo s id ty dec_fields =
 %token AWAIT AWAITSTAR AWAITQUEST ASYNC ASYNCSTAR BREAK CASE CATCH CONTINUE DO LABEL DEBUG
 %token IF IGNORE IN IMPLICIT ELSE SWITCH LOOP WHILE FOR RETURN TRY THROW FINALLY WITH
 %token ARROW ASSIGN
-%token FUNC TYPE OBJECT ACTOR CLASS PUBLIC PRIVATE SHARED SYSTEM QUERY
+%token FUNC TYPE NEWTYPE OBJECT ACTOR CLASS PUBLIC PRIVATE SHARED SYSTEM QUERY
 %token SEMICOLON SEMICOLON_EOL COMMA COLON SUB DOT QUEST BANG
 %token AND OR NOT
 %token IMPORT INCLUDE MODULE MIXIN
@@ -963,6 +963,8 @@ dec_nonvar :
       LetD (p', e', None) @? at $sloc }
   | TYPE x=typ_id tps=type_typ_params_opt EQ t=typ
     { TypD(x, tps, t) @? at $sloc }
+  | NEWTYPE x=typ_id tps=type_typ_params_opt EQ t=typ
+    { NewtypeD(x, tps, t) @? at $sloc }
   | sp=shared_pat_opt FUNC
       xf_tps_p=func_pat t=annot_opt fb=func_body
     { (* This is a hack to support local func declarations that return a computed async.
diff --git a/src/mo_frontend/printers.ml b/src/mo_frontend/printers.ml
index e18d9416d8d..bb55efe29d7 100644
--- a/src/mo_frontend/printers.ml
+++ b/src/mo_frontend/printers.ml
@@ -168,6 +168,7 @@ let repr_of_symbol : xsymbol -> (string * string) =
   | X (T T_ADDOP) -> unop "+"
   | X (T T_ACTOR) -> simple_token "actor"
   | X (T T_PIPE) -> simple_token "|>"
+  | X (T T_NEWTYPE) -> simple_token "newtype"
   | X (T T_WEAK) -> simple_token "weak"
   (* non-terminals *)
   | X (N N_bl) -> "<bl>", "<bl>"
diff --git a/src/mo_frontend/source_lexer.mll b/src/mo_frontend/source_lexer.mll
index b62af0e5c7d..ba40e0a3b13 100644
--- a/src/mo_frontend/source_lexer.mll
+++ b/src/mo_frontend/source_lexer.mll
@@ -256,6 +256,7 @@ rule token mode = parse
   | "throw" { THROW }
   | "to_candid" { TO_CANDID }
   | "true" { BOOL true }
+  | "newtype" { NEWTYPE }
   | "type" { TYPE }
   | "var" { VAR }
   | "weak" { WEAK }
diff --git a/src/mo_frontend/source_token.ml b/src/mo_frontend/source_token.ml
index d0185cca08d..5ba7f554648 100644
--- a/src/mo_frontend/source_token.ml
+++ b/src/mo_frontend/source_token.ml
@@ -125,6 +125,7 @@ type token =
   | PRIM
   | PIPE
   | UNDERSCORE
+  | NEWTYPE
   | WEAK
   | COMPOSITE
   (* Trivia *)
@@ -261,6 +262,7 @@ let to_parser_token :
   | UNDERSCORE -> Ok Parser.UNDERSCORE
   | COMPOSITE -> Ok Parser.COMPOSITE
   | PIPE -> Ok Parser.PIPE
+  | NEWTYPE -> Ok Parser.NEWTYPE
   | WEAK -> Ok Parser.WEAK
   (*Trivia *)
   | SINGLESPACE -> Error (Space 1)
@@ -399,6 +401,7 @@ let string_of_parser_token = function
   | Parser.UNDERSCORE -> "UNDERSCORE"
   | Parser.COMPOSITE -> "COMPOSITE"
   | Parser.PIPE -> "PIPE"
+  | Parser.NEWTYPE -> "NEWTYPE"
   | Parser.WEAK -> "WEAK"
 
 let is_lineless_trivia : token -> void trivia option = function
diff --git a/src/mo_frontend/static.ml b/src/mo_frontend/static.ml
index 5e4502b3259..f3d2966933d 100644
--- a/src/mo_frontend/static.ml
+++ b/src/mo_frontend/static.ml
@@ -98,7 +98,7 @@ and exp_fields m efs = List.iter (fun (ef : exp_field) ->
   exp m ef.it.exp) efs
 
 and dec m d = match d.it with
-  | TypD _ | ClassD _ | MixinD _ -> ()
+  | TypD _ | NewtypeD _ | ClassD _ | MixinD _ -> ()
   | ExpD e -> exp m e
   | LetD (p, e, fail) -> pat m p; exp m e; Option.iter (exp m) fail
   | VarD _ | IncludeD _ -> err m d.at
diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml
index d3a26bbe4f3..30ec4a7f5a8 100644
--- a/src/mo_frontend/traversals.ml
+++ b/src/mo_frontend/traversals.ml
@@ -68,7 +68,7 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
      f { exp with it = IgnoreE (over_exp f exp1)}
 
 and over_dec (f : exp -> exp) (d : dec) : dec = match d.it with
-  | TypD _ -> d
+  | TypD _ | NewtypeD _ -> d
   | ExpD e -> { d with it = ExpD (over_exp f e)}
   | VarD (x, e) ->
      { d with it = VarD (x, over_exp f e)}
diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml
index 9d58291f208..88b33acf85d 100644
--- a/src/mo_frontend/typing.ml
+++ b/src/mo_frontend/typing.ml
@@ -518,6 +518,7 @@ let check_closed env id k at =
   let is_typ_param c =
     match Cons.kind c with
     | T.Def _
+    | T.Newtype _
     | T.Abs( _, T.Pre) -> false (* an approximated type constructor *)
     | T.Abs( _, _) -> true in
   let typ_params = T.ConSet.filter is_typ_param env.cons in
@@ -808,7 +809,7 @@ and check_typ' env typ : T.typ =
   | PathT (path, typs) ->
     let c = check_typ_path env path in
     let ts = List.map (check_typ env) typs in
-    let T.Def (tbs, _) | T.Abs (tbs, _) = Cons.kind c in
+    let T.Def (tbs, _) | T.Abs (tbs, _) | T.Newtype (tbs, _) = Cons.kind c in
     let tbs' = List.map (fun tb -> { tb with T.bound = T.open_ ts tb.T.bound }) tbs in
     check_typ_bounds env tbs' ts (List.map (fun typ -> typ.at) typs) typ.at;
     T.Con (c, ts)
@@ -1177,7 +1178,7 @@ let rec is_explicit_exp e =
 and is_explicit_dec d =
   match d.it with
   | ExpD e | LetD (_, e, _) | VarD (_, e) -> is_explicit_exp e
-  | TypD _ -> true
+  | TypD _ | NewtypeD _ -> true
   | ClassD (_, _, _, _, _, p, _, _, dfs) ->
     is_explicit_pat p &&
     List.for_all (fun (df : dec_field) -> is_explicit_dec df.it.dec) dfs
@@ -1316,6 +1317,10 @@ let text_obj () =
     {lab = "size";  typ = Func (Local, Returns, [], [], [Prim Nat]); src = empty_src};
   ]
 
+let newtype_obj t =
+  T.Object,
+  [ T.{lab = "unwrap"; typ = t; src = empty_src} ]
+
 
 (* Expressions *)
 
@@ -2301,6 +2306,7 @@ and try_infer_dot_exp env at exp id (desc, pred) =
   let t0, t1 = infer_exp_and_promote env exp in
   let fields =
     try Ok(T.as_obj_sub [id.it] t1) with Invalid_argument _ ->
+    try Ok(newtype_obj (T.as_newtype_sub t1)) with Invalid_argument _ ->
     try Ok(array_obj (T.as_array_sub t1)) with Invalid_argument _ ->
     try Ok(blob_obj (T.as_prim_sub T.Blob t1)) with Invalid_argument _ ->
     try Ok(text_obj (T.as_prim_sub T.Text t1)) with Invalid_argument _ ->
@@ -3648,6 +3654,7 @@ and vis_dec src dec xs : visibility_env =
   | ExpD _ -> xs
   | LetD (pat, _, _) -> vis_pat src pat xs
   | VarD (id, _) -> vis_val_id src id xs
+  | NewtypeD (id, _, _)
   | ClassD (_, _, _, id, _, _, _, _, _) ->
     vis_val_id src {id with note = ()} (vis_typ_id src id xs)
   | TypD (id, _, _) -> vis_typ_id src id xs
@@ -4243,7 +4250,7 @@ and infer_dec env dec : T.typ =
     let obj_sort : obj_sort = { it = T.Mixin ; at = no_region; note = { it = true; at = no_region; note = () } }  in
     let t' = infer_obj { env' with check_unused = false } obj_sort None dec_fields dec.at in
     T.normalize t'
-  | TypD _ ->
+  | TypD _ | NewtypeD _ ->
     T.unit
   in
   let eff = A.infer_effect_dec dec in
@@ -4350,7 +4357,7 @@ and gather_dec env scope dec : Scope.t =
       | _ -> error env pat.at "M0229" "mixins may only be imported by binding to a name"
   )
   | VarD (id, _) -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id Scope.Declaration)
-  | TypD (id, binds, _) | ClassD (_, _, _, id, binds, _, _, _, _) ->
+  | TypD (id, binds, _) | NewtypeD (id, binds, _) | ClassD (_, _, _, id, binds, _, _, _, _) ->
     let open Scope in
     if T.Env.mem id.it scope.typ_env then
       error_duplicate env "type " id;
@@ -4371,6 +4378,7 @@ and gather_dec env scope dec : Scope.t =
       | Some c -> c
     in
     let val_env = match dec.it with
+      | NewtypeD _
       | ClassD _ ->
         if T.Env.mem id.it scope.val_env then
           error_duplicate env "" id;
@@ -4512,6 +4520,17 @@ and infer_dec_typdecs env dec : Scope.t =
       typ_env = T.Env.singleton id.it c;
       con_env = infer_id_typdecs env dec.at id c k;
     }
+  | NewtypeD (id, binds, typ) ->
+    let c = T.Env.find id.it env.typs in
+    let cs, tbs, te, ce = check_typ_binds {env with pre = true} binds in
+    let env' = adjoin_typs env te ce in
+    let t = check_typ env' typ in
+    let k = T.Newtype (T.close_binds cs tbs, T.close cs t) in
+    check_closed env id k dec.at;
+    Scope.{ empty with
+      typ_env = T.Env.singleton id.it c;
+      con_env = infer_id_typdecs env dec.at id c k;
+    }
   | ClassD (exp_opt, shared_pat, obj_sort, id, binds, pat, _typ_opt, self_id, dec_fields) ->
      (*TODO exp_opt *)
     let c = T.Env.find id.it env.typs in
@@ -4601,6 +4620,20 @@ and infer_dec_valdecs env dec : Scope.t =
       typ_env = T.Env.singleton id.it c;
       con_env = T.ConSet.singleton c;
     }
+  | NewtypeD (id, _, _) ->
+    let c = Option.get id.note in
+    let tbs, t_body = match Cons.kind c with
+      | T.Newtype (tbs, t) -> tbs, t
+      | _ -> assert false
+    in
+    let type_args = List.mapi (fun i tb -> T.Var (tb.T.var, i)) tbs in
+    let newtype_typ = T.Con (c, type_args) in
+    let ctor_typ = T.Func (T.Local, T.Returns, tbs, [t_body], [newtype_typ]) in
+    Scope.{ empty with
+      typ_env = T.Env.singleton id.it c;
+      con_env = T.ConSet.singleton c;
+      val_env = singleton id ctor_typ;
+    }
   | MixinD (_, _) -> Scope.empty
   | ClassD (_exp_opt, _shared_pat, obj_sort, id, typ_binds, pat, _, _, _) ->
     if obj_sort.it = T.Actor then begin
diff --git a/src/mo_frontend/variance.ml b/src/mo_frontend/variance.ml
index 2d70d683302..f14848cda5f 100644
--- a/src/mo_frontend/variance.ml
+++ b/src/mo_frontend/variance.ml
@@ -56,7 +56,8 @@ let update ?(start = Covariant) env t =
       | Con (c, ts) ->
         (match Cons.kind c with
         | Abs _ -> ()
-        | Def (_, t) -> go p (open_ ts t)) (* TBR this may fail to terminate *)
+        | Def (_, t)
+        | Newtype (_, t) -> go p (open_ ts t)) (* TBR this may fail to terminate *)
       | Array t | Opt t | Weak t (*TBR*) -> go p t
       | Mut t -> go Invariant t
       | Async (s, t1, t2) ->
diff --git a/src/mo_idl/mo_to_idl.ml b/src/mo_idl/mo_to_idl.ml
index 0e652c885d9..670955b9fc2 100644
--- a/src/mo_idl/mo_to_idl.ml
+++ b/src/mo_idl/mo_to_idl.ml
@@ -34,7 +34,7 @@ module MakeState() = struct
   let monomorphize_con vs c =
     let name = normalize_name (Cons.name c) in
     match Cons.kind c with
-    | Def _ ->
+    | Def _ | Newtype _ ->
       let id = (c, vs) in
       let (k, n) =
         match TypeMap.find_opt id !type_map with
@@ -92,7 +92,8 @@ module MakeState() = struct
     | Var (s, i) -> assert false
     | Con (c, ts) ->
       (match Cons.kind c with
-       | Def (_, t) ->
+       | Def (_, t)
+       | Newtype (_, t) ->
          I.(match open_ ts t with
             | Prim p -> prim p
             | Any -> PrimT Reserved
diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml
index 6f3ca88c5bc..960b031ef56 100644
--- a/src/mo_interpreter/interpret.ml
+++ b/src/mo_interpreter/interpret.ml
@@ -554,7 +554,9 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
     interpret_exp env exp1 (fun v1 -> k V.(Tup [v1; Text id.it]))
   | DotE (exp1, id, _) ->
     interpret_exp env exp1 (fun v1 ->
-      match v1 with
+      if id.it = "unwrap" && T.is_con exp1.note.note_typ then (* TODO: same as desugaring *)
+        k v1 (* newtype .unwrap is identity *)
+      else match v1 with
       | V.Obj fs ->
         k (find id.it fs)
       | V.Array vs ->
@@ -1021,7 +1023,8 @@ and declare_dec dec : val_env =
     assert false
   | LetD (pat, _, _) -> declare_pat pat
   | VarD (id, _) -> declare_id id
-  | ClassD (_eo, _, _, id, _, _, _, _, _) -> declare_id {id with note = ()}
+  | NewtypeD (id, _, _)
+  | ClassD (_, _, _, id, _, _, _, _, _) -> declare_id {id with note = ()}
 
 and declare_decs decs ve : val_env =
   match decs with
@@ -1051,6 +1054,11 @@ and interpret_dec env dec (k : V.value V.cont) =
     )
   | TypD _ ->
     k V.unit
+  | NewtypeD (id, _, _) ->
+    (* Bind the constructor as an identity function: fun (x) = x *)
+    let v = V.local_func 1 1 (fun _ctxt v k -> k v) in
+    define_id env {id with note = ()} v;
+    k V.unit
   | MixinD _ -> k V.unit
   | IncludeD (_, _arg, _note) ->
      (* TODO
diff --git a/src/mo_types/expansive.ml b/src/mo_types/expansive.ml
index 78fb04439e1..057772c1e1f 100644
--- a/src/mo_types/expansive.ml
+++ b/src/mo_types/expansive.ml
@@ -130,7 +130,8 @@ let edges_typ cs c (es : EdgeSet.t) t : EdgeSet.t =
 
 let edges_con cs c es : EdgeSet.t =
   match Cons.kind c with
-  | Def (tbs, t) ->
+  | Def (tbs, t)
+  | Newtype (tbs, t) ->
     (* It's not clear we actually need to consider parameters bounds, since, unlike
        function type parameters, they don't introduce new subgoals during subtyping.
        But let's be conservative and consider them, until we find out that that's undesirable
@@ -148,7 +149,8 @@ let vertices cs =
   ConSet.fold
     (fun c vs ->
       match Cons.kind c with
-      | Def (tbs, t) ->
+      | Def (tbs, t)
+      | Newtype (tbs, t) ->
         let ws = List.mapi (fun i _tb -> (c, i)) tbs in
         List.fold_left (fun vs v -> VertexSet.add v vs) vs ws
       | Abs (tbs, t) ->
@@ -193,9 +195,9 @@ let is_expansive cs =
     (* Construct an error messages with optional debug info *)
     let op, sbs, st = Pretty.strings_of_kind (Cons.kind c) in
     let def = Printf.sprintf "type %s%s %s %s" (Cons.name c) sbs op st in
-    let x = match Cons.kind c with Def(tbs, _) | Abs(tbs, _) ->
+    let x = match Cons.kind c with Def(tbs, _) | Abs(tbs, _) | Newtype(tbs, _) ->
       (List.nth tbs i).var in
-    let dys = match Cons.kind d with Def(tbs, _) | Abs(tbs, _) ->
+    let dys = match Cons.kind d with Def(tbs, _) | Abs(tbs, _) | Newtype(tbs, _) ->
       Printf.sprintf "%s<%s>" (Cons.name d)
         (String.concat "," (List.mapi (fun k _ ->
           if i = k then "-" ^ x ^"-" else "_") tbs))
diff --git a/src/mo_types/productive.ml b/src/mo_types/productive.ml
index e97992dacff..0f02cf35c73 100644
--- a/src/mo_types/productive.ml
+++ b/src/mo_types/productive.ml
@@ -37,7 +37,8 @@ let non_productive cs =
         | Param n ->
           begin
           match Cons.kind d with
-          | Def (tbs, t) ->
+          | Def (tbs, t)
+          | Newtype (tbs, t) ->
             assert (n < List.length tbs); (* assume types are arity-correct *)
             rhs cs (List.nth ts n)
           | Abs (tbs, t) ->
@@ -60,7 +61,8 @@ let non_productive cs =
           Nonproductive
         else
           let t = match Cons.kind c with
-            | Def (_, t) -> t
+            | Def (_, t)
+            | Newtype (_, t) -> t
             | _ -> assert false
           in
           rhs (ConSet.add c cs) t
diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml
index fb3df1536c8..50fdda00769 100644
--- a/src/mo_types/type.ml
+++ b/src/mo_types/type.ml
@@ -78,6 +78,7 @@ and con = kind Cons.t
 and kind =
   | Def of bind list * typ
   | Abs of bind list * typ
+  | Newtype of bind list * typ
 
 let empty_src = {depr = None; track_region = Source.no_region; region = Source.no_region}
 
@@ -599,12 +600,20 @@ let rec normalize = function
   | t -> t
 
 let rec promote = function
-  | Con (con, ts) ->
-    let Def (tbs, t) | Abs (tbs, t) = Cons.kind con
-    in promote (reduce tbs t ts)
+  | Con (con, ts) as t ->
+    (match Cons.kind con with
+    | Def (tbs, t) | Abs (tbs, t) -> promote (reduce tbs t ts)
+    | Newtype _ -> t)
   | Named (_, t) -> promote t
   | t -> t
 
+let rec eliminate_con = function
+  | Con (con, ts) ->
+    (match Cons.kind con with
+    | Def (tbs, t) | Abs (tbs, t) | Newtype (tbs, t) -> eliminate_con (reduce tbs t ts))
+  | Named (_, t) -> eliminate_con t
+  | t -> t
+
 (* Projections *)
 
 let is_non = function Non -> true | _ -> false
@@ -673,6 +682,12 @@ let as_array_sub t = match promote t with
   | Array t -> t
   | Non -> Non
   | _ -> invalid "as_array_sub"
+let as_newtype_sub t = match t with
+  | Con (c, ts) ->
+    (match Cons.kind c with
+    | Newtype (_, t_body) -> open_ ts t_body
+    | _ -> invalid "as_newtype_sub")
+  | _ -> invalid "as_newtype_sub"
 let as_opt_sub t = match promote t with
   | Opt t -> t
   | Prim Null -> Non
@@ -756,7 +771,7 @@ let lookup_typ_deprecation l tfs =
 
 let rec span = function
   | Var _ | Pre -> assert false
-  | Con _ as t -> span (promote t)
+  | Con _ as t -> span (eliminate_con t)
   | Prim Null -> Some 1
   | Prim Bool -> Some 2
   | Prim (Nat | Int | Float | Text | Blob | Error | Principal | Region) -> None
@@ -823,7 +838,8 @@ and cons_typ_field inTyp {typ = c; _} cs =
 and cons_kind' inTyp k cs =
   match k with
   | Def (tbs, t)
-  | Abs (tbs, t) ->
+  | Abs (tbs, t)
+  | Newtype (tbs, t) ->
     cons' inTyp t (List.fold_right (cons_bind inTyp) tbs cs)
 
 let cons t = cons' true t ConSet.empty
@@ -853,7 +869,8 @@ let concrete t =
       | Con (c, ts) ->
         (match Cons.kind c with
         | Abs _ -> false
-        | Def (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *)
+        | Def (_, t)
+        | Newtype (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *)
         )
       | Array t | Opt t | Mut t -> go t
       | Async (s, t1, t2) -> go t2 (* t1 is a phantom type *)
@@ -898,8 +915,9 @@ let paths p t =
         List.iter (fun f -> go (DotP (p, f.lab)) f.typ) fs
       | Con (c, ts) ->
         (match Cons.kind c with
-        | Abs (_, t) -> go p (open_ ts t)
-        | Def (_, t) -> go p (open_ ts t)
+        | Abs (_, t)
+        | Def (_, t)
+        | Newtype (_, t) -> go p (open_ ts t) (* TODO: correct? *)
         )
       (* explicit match in case we add a constructor later *)
       | Var _ | Pre
@@ -937,7 +955,8 @@ let serializable allow_mut t =
       | Con (c, ts) ->
         (match Cons.kind c with
         | Abs _ -> false
-        | Def (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *)
+        | Def (_, t)
+        | Newtype (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *)
         )
       | Array t | Opt t -> go t
       | Tup ts -> List.for_all go ts
@@ -967,7 +986,8 @@ let find_unshared t =
       | Con (c, ts) ->
         (match Cons.kind c with
         | Abs _ -> None
-        | Def (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *)
+        | Def (_, t)
+        | Newtype (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *)
         )
       | Array t | Opt t -> go t
       | Tup ts -> List.find_map go ts
@@ -1358,7 +1378,8 @@ and eq_typ d rel eq t1 t2 = rel_typ d eq eq t1 t2
 and eq_kind' eq k1 k2 : bool =
   match k1, k2 with
   | Def (tbs1, t1), Def (tbs2, t2)
-  | Abs (tbs1, t1), Abs (tbs2, t2) ->
+  | Abs (tbs1, t1), Abs (tbs2, t2)
+  | Newtype (tbs1, t1), Newtype (tbs2, t2) ->
     (match rel_binds (RelArg.sub []) eq eq tbs1 tbs2 with
     | Some ts -> eq_typ (RelArg.sub []) eq eq (open_ ts t1) (open_ ts t2)
     | None -> false
@@ -1369,7 +1390,8 @@ and eq_con' d eq c1 c2 =
   match Cons.kind c1, Cons.kind c2 with
   | (Def (tbs1, t1)) as k1, (Def (tbs2, t2) as k2) ->
     eq_kind' eq k1 k2
-  | Abs _, Abs _ ->
+  | Abs _, Abs _
+  | Newtype _, Newtype _ ->
     Cons.eq c1 c2
   | Def (tbs1, t1), Abs (tbs2, t2)
   | Abs (tbs2, t2), Def (tbs1, t1) ->
@@ -1377,6 +1399,9 @@ and eq_con' d eq c1 c2 =
     | Some ts -> eq_typ d eq eq (open_ ts t1) (Con (c2, ts))
     | None -> false
     )
+  | Newtype _, (Def _ | Abs _)
+  | (Def _ | Abs _), Newtype _ ->
+    false
 
 let eq_binds ?(src_fields = empty_srcs_tbl ()) tbs1 tbs2 =
   with_src_field_updates_predicate src_fields (fun () ->
@@ -1497,7 +1522,8 @@ let rec inhabited_typ co t =
   | Var _ -> true  (* TODO(rossberg): consider bound *)
   | Con (c, ts) ->
     (match Cons.kind c with
-    | Def (tbs, t') -> (* TBR this may fail to terminate *)
+    | Def (tbs, t')
+    | Newtype (tbs, t') -> (* TBR this may fail to terminate *)
       inhabited_typ co (open_ ts t')
     | Abs (tbs, t') ->
       inhabited_typ co t')
@@ -1551,6 +1577,9 @@ let rec has_no_subtypes_or_supertypes m co = function
         s := S.add t !s;
         has_no_subtypes_or_supertypes m co (reduce tbs def ts)
       end
+    | Newtype _ ->
+      (* Newtypes are nominal; no implicit sub/supertypes *)
+      true
     )
   | Mut _ -> true
   | Named (_, t) -> has_no_subtypes_or_supertypes m co t
@@ -2273,7 +2302,8 @@ and pp_binds vs vs' ppf = function
 and pps_of_kind' vs k =
   let op, tbs, t =
     match k with
-    | Def (tbs, t) -> "=", tbs, t
+    | Def (tbs, t)
+    | Newtype (tbs, t) -> "=", tbs, t
     | Abs (tbs, t) -> "<:", tbs, t
   in
   let vs' = vars_of_binds vs tbs in
@@ -2313,7 +2343,7 @@ and pp_stab_sig ppf sig_ =
       | Def ([], Prim p) when string_of_con c = string_of_prim p -> false
       | Def ([], Any) when string_of_con c = "Any" -> false
       | Def ([], Non) when string_of_con c = "None" -> false
-      | Def _ -> true
+      | Def _ | Newtype _ -> true
       | Abs _ -> false) cs in
     ConSet.elements cs' in
   let tfs =
@@ -2345,12 +2375,13 @@ let rec pp_typ_expand' vs ppf t =
   | Con (c, ts) ->
     (match Cons.kind c with
     | Abs _ -> pp_typ' vs ppf t
-    | Def _ ->
-      match normalize t with
+    | Def (_, t_body) | Newtype (_, t_body) ->
+      let t' = open_ ts t_body in
+      (match t' with
       | Prim _ | Any | Non -> pp_typ' vs ppf t
-      | t' -> fprintf ppf "%a = %a"
+      | _ -> fprintf ppf "%a = %a"
         (pp_typ' vs) t
-        (pp_typ_expand' vs) t'
+        (pp_typ_expand' vs) t')
     )
   | _ -> pp_typ' vs ppf t
 
diff --git a/src/mo_types/type.mli b/src/mo_types/type.mli
index 67a55c0f148..a7489f2bca9 100644
--- a/src/mo_types/type.mli
+++ b/src/mo_types/type.mli
@@ -69,6 +69,7 @@ and con = kind Cons.t
 and kind =
   | Def of bind list * typ
   | Abs of bind list * typ
+  | Newtype of bind list * typ
 
 val empty_src : src
 
@@ -166,6 +167,7 @@ val as_prim_sub : prim -> typ -> unit
 val as_obj_sub : string list -> typ -> obj_sort * field list
 val as_variant_sub : string -> typ -> field list
 val as_array_sub : typ -> typ
+val as_newtype_sub : typ -> typ
 val as_opt_sub : typ -> typ
 val as_tup_sub : int -> typ -> typ list
 val as_unit_sub : typ -> unit
diff --git a/src/mo_values/operator.ml b/src/mo_values/operator.ml
index 860d5fdfe2e..2686e3a6e36 100644
--- a/src/mo_values/operator.ml
+++ b/src/mo_values/operator.ml
@@ -177,7 +177,8 @@ let structural_equality t =
     | T.Con (c, ts) -> (
         match Mo_types.Cons.kind c with
         | T.Abs _ -> assert false
-        | T.Def (_, t) -> go (T.open_ ts t) (* TBR this may fail to terminate *)
+        | T.Def (_, t)
+        | T.Newtype (_, t) -> go (T.open_ ts t) (* TBR this may fail to terminate *)
         )
     | T.Array t ->
         fun v1 v2 ->
diff --git a/test/core-stub/src/Map.mo b/test/core-stub/src/Map.mo
index c1db4b6a492..3dd27b2265c 100644
--- a/test/core-stub/src/Map.mo
+++ b/test/core-stub/src/Map.mo
@@ -3,15 +3,12 @@
 import Types "Types";
 
 module {
-  public type Map<K, V> = Types.Map<K, V>;
-
-  type Node<K, V> = Types.Map.Node<K, V>;
-  type Data<K, V> = Types.Map.Data<K, V>;
-  type Internal<K, V> = Types.Map.Internal<K, V>;
-  type Leaf<K, V> = Types.Map.Leaf<K, V>;
+  public newtype Map<K, V> = Types.MapT.MapInternals<K, V>;
+  // public type Map<K, V> = Types.Map<K, V>;
 
   public func empty<K, V>() : Map<K, V> {
-    {
+    // TODO: when `Map` is a type alias for a Map newtype, `Map` cannot be used here, as there is no value constructor called `Map`, the type alias is not introducing a constructor.
+    Map<K, V>({
       var root = #leaf({
         data = {
           kvs = [var null];
@@ -19,12 +16,12 @@ module {
         }
       });
       var size_ = 0
-    }
+    })
   };
 
 
   public func get<K, V>(self : Map<K, V>, compare : (implicit : (K, K) -> Types.Order), key : K) : ?V {
-    switch (self.root) {
+    switch (self.unwrap.root) {
       case (#internal _) { null };
       case (#leaf(leafNode)) {
         let ?x = leafNode.data.kvs[0] else return null;
@@ -35,7 +32,7 @@ module {
 
 
   public func add<K, V>(self : Map<K, V>, compare : (implicit : (K, K) -> Types.Order), key : K, value : V) {
-    switch (self.root) {
+    switch (self.unwrap.root) {
       case (#internal _) { };
       case (#leaf(leafNode)) {
         switch (leafNode.data.kvs[0]) {
diff --git a/test/core-stub/src/Time.mo b/test/core-stub/src/Time.mo
new file mode 100644
index 00000000000..835484e8c7a
--- /dev/null
+++ b/test/core-stub/src/Time.mo
@@ -0,0 +1,7 @@
+/// Stub for Time.
+
+module {
+  public newtype Time = Int;
+
+  public func now() : Time { Time(0) };
+}
diff --git a/test/core-stub/src/Types.mo b/test/core-stub/src/Types.mo
index 18257444ae1..659af93d06a 100644
--- a/test/core-stub/src/Types.mo
+++ b/test/core-stub/src/Types.mo
@@ -5,7 +5,7 @@ module {
   public type Order = { #less; #equal; #greater };
   public type Result<T, E> = { #ok : T; #err : E };
 
-  public module Map {
+  public module MapT {
     public type Node<K, V> = {
       #leaf : Leaf<K, V>;
       #internal : Internal<K, V>
@@ -25,11 +25,11 @@ module {
       data : Data<K, V>
     };
 
-    public type Map<K, V> = {
+    public type MapInternals<K, V> = {
       var root : Node<K, V>;
       var size_ : Nat
     }
   };
 
-  public type Map<K, V> = Map.Map<K, V>;
+  // public newtype Map<K, V> = MapT.MapInternals<K, V>;
 }
diff --git a/test/fail/newtype.mo b/test/fail/newtype.mo
new file mode 100644
index 00000000000..9b5f45bb4d4
--- /dev/null
+++ b/test/fail/newtype.mo
@@ -0,0 +1,22 @@
+// newtype error cases
+
+newtype Time = Int;
+newtype Duration = Int;
+
+// cannot assign Int where Time is expected
+func m1() { let bad1 : Time = 123 };
+
+// cannot assign Time where Int is expected
+func m2() { let bad2 : Int = Time(0) };
+
+// cannot assign Time where Duration is expected (different newtypes over same type)
+func m3() { let bad3 : Duration = Time(0) };
+
+// cannot assign Duration where Time is expected
+func m4() { let bad4 : Time = Duration(0) };
+
+// cannot use Int arithmetic directly on Time
+func m5() { let bad5 = Time(1) + Time(2) };
+
+// cannot unwrap an Int (unwrap only exists on newtypes)
+func m6() { let bad6 = (42 : Int).unwrap };
diff --git a/test/fail/ok/newtype.tc.ok b/test/fail/ok/newtype.tc.ok
new file mode 100644
index 00000000000..75b43c5dd6b
--- /dev/null
+++ b/test/fail/ok/newtype.tc.ok
@@ -0,0 +1,34 @@
+newtype.mo:7.31-7.34: type error [M0050], literal of type
+  Nat
+does not have expected type
+  Time = Int
+newtype.mo:10.30-10.37: type error [M0096], expression of type
+  Time = Int
+cannot produce expected type
+  Int
+because the type 
+  Time
+ is not compatible with type 
+  Int
+newtype.mo:13.35-13.42: type error [M0096], expression of type
+  Time = Int
+cannot produce expected type
+  Duration = Int
+because the type 
+  Time
+ is not compatible with type 
+  Duration
+newtype.mo:16.31-16.42: type error [M0096], expression of type
+  Duration = Int
+cannot produce expected type
+  Time = Int
+because the type 
+  Duration
+ is not compatible with type 
+  Time
+newtype.mo:19.24-19.41: type error [M0060], operator is not defined for operand types
+  Time = Int
+and
+  Time = Int
+newtype.mo:22.25-22.33: type error [M0070], expected object type, but expression produces type
+  Int
diff --git a/test/fail/ok/newtype.tc.ret.ok b/test/fail/ok/newtype.tc.ret.ok
new file mode 100644
index 00000000000..69becfa16f9
--- /dev/null
+++ b/test/fail/ok/newtype.tc.ret.ok
@@ -0,0 +1 @@
+Return code 1
diff --git a/test/fail/ok/type-alias-path.tc.ok b/test/fail/ok/type-alias-path.tc.ok
index 8ebdb05e0ee..56cabc41df0 100644
--- a/test/fail/ok/type-alias-path.tc.ok
+++ b/test/fail/ok/type-alias-path.tc.ok
@@ -1,21 +1,21 @@
-type-alias-path.mo:18.41-18.42: type error [M0096], expression of type
-  {m1 : M1.Map<Nat, Text>; m2 : MyMap.Map<Nat, Text>}
+type-alias-path.mo:19.41-19.42: type error [M0096], expression of type
+  {m1 : M1.Map<Nat, Text>; m2 : MapT.MapInternals<Nat, Text>}
 cannot produce expected type
   {m2 : M1.Map<Nat, Text>}
 because expected field `map` is missing from type 
-  {var root : Node<Nat, Text>; var size_ : Nat}
+  {var root : MapT.Node<Nat, Text>; var size_ : Nat}
  of `M1.Map` (used by `m2`)
-type-alias-path.mo:21.17-21.52: type error [M0096], expression of type
-  (m : MyMap.Map<Nat, Text>) -> ()
+type-alias-path.mo:22.17-22.60: type error [M0096], expression of type
+  (m : MapT.MapInternals<Nat, Text>) -> ()
 cannot produce expected type
   M1.Map<Nat, Text> -> ()
-type-alias-path.mo:24.24-24.33: type error [M0096], expression of type
+type-alias-path.mo:25.24-25.33: type error [M0096], expression of type
   <K, V>(self : MyMap.Map<K, V>, compare : (implicit : (K, K) -> Order),
          key : K) ->
     ?V
 cannot produce expected type
   () -> ()
-type-alias-path.mo:29.10-29.12: type error [M0096], expression of type
+type-alias-path.mo:30.10-30.12: type error [M0096], expression of type
   {x : MyType}
 cannot produce expected type
   {x : MyType}
diff --git a/test/fail/ok/wrong-call-args.tc.ok b/test/fail/ok/wrong-call-args.tc.ok
index e0dae3029ac..1c3e78355a6 100644
--- a/test/fail/ok/wrong-call-args.tc.ok
+++ b/test/fail/ok/wrong-call-args.tc.ok
@@ -19,7 +19,7 @@ wrong-call-args.mo:45.5-45.17: type error [M0098], cannot apply function of type
          key : K) ->
     ?V
 to argument of type
-  {var root : Types.Map.Node<Text, Text>; var size_ : Nat}
+  Map.Map<Text, Text>
 because there is no way to satisfy subtyping
   ?V  <:  ()  (for the expected return type) 
 wrong-call-args.mo:48.27-48.39: type error [M0096], expression of type
diff --git a/test/fail/type-alias-path.mo b/test/fail/type-alias-path.mo
index 4ed5967f083..d9f90c0aa0f 100644
--- a/test/fail/type-alias-path.mo
+++ b/test/fail/type-alias-path.mo
@@ -1,5 +1,6 @@
 //MOC-FLAG --package core ../core-stub/src
 import MyMap "mo:core/Map";
+import { MapT } "mo:core/Types";
 
 // Have 2 files with the same import name, but different paths.
 import IM1 "type-alias-path/importM1";
@@ -14,11 +15,11 @@ module M1 {
 module Main {
   func inv<T>(t : T) : T -> () = func(_ : T) = ();
   func check<T>(t : T, _ : T -> ()) {};
-  func showRecord(r : {m1 : M1.Map<Nat, Text>; m2 : MyMap.Map<Nat, Text>}) {
+  func showRecord(r : {m1 : M1.Map<Nat, Text>; m2 : MapT.MapInternals<Nat, Text>}) {
     let _ : {m2 : M1.Map<Nat, Text> } = r;
   };
-  func showBimatch(r : {m1 : M1.Map<Nat, Text>; m2 : MyMap.Map<Nat, Text>}) {
-    check(r.m1, func(m : MyMap.Map<Nat, Text>) = ());
+  func showBimatch(r : {m1 : M1.Map<Nat, Text>; m2 : MapT.MapInternals<Nat, Text>}) {
+    check(r.m1, func(m : MapT.MapInternals<Nat, Text>) = ());
   };
   func showTransitiveImport() {
     let _ : () -> () = MyMap.get // the error message mentions `Types.Order` that is NOT imported here
diff --git a/test/run/newtype-module.mo b/test/run/newtype-module.mo
new file mode 100644
index 00000000000..065fb3c0520
--- /dev/null
+++ b/test/run/newtype-module.mo
@@ -0,0 +1,9 @@
+//MOC-FLAG --package core ../core-stub/src
+
+import Time "mo:core/Time";
+
+let t : Time.Time = Time.now();
+assert (t.unwrap == 0);
+
+let t2 : Time.Time = Time.Time(42);
+assert (t2.unwrap == 42);
diff --git a/test/run/newtype.mo b/test/run/newtype.mo
new file mode 100644
index 00000000000..20994e874e1
--- /dev/null
+++ b/test/run/newtype.mo
@@ -0,0 +1,35 @@
+// basic newtype declaration and usage
+
+newtype Time = Int;
+
+// construction
+let time : Time = Time(123);
+
+// unwrap
+let n : Int = time.unwrap;
+assert (n == 123);
+
+// roundtrip
+let time2 = Time(42);
+assert (time2.unwrap == 42);
+
+// newtype with negative value
+let neg = Time(-1);
+assert (neg.unwrap == -1);
+
+// newtype in function signatures
+func addTimes(a : Time, b : Time) : Int {
+  a.unwrap + b.unwrap
+};
+assert (addTimes(Time(10), Time(20)) == 30);
+
+// nested usage
+func wrapAndUnwrap(x : Int) : Int {
+  Time(x).unwrap
+};
+assert (wrapAndUnwrap(99) == 99);
+
+// constructor as a first-class function
+let ctor : Int -> Time = Time;
+let t3 = ctor(7);
+assert (t3.unwrap == 7);