diff --git a/prelude/index.1ml b/prelude/index.1ml
index c783108e..787f9325 100644
--- a/prelude/index.1ml
+++ b/prelude/index.1ml
@@ -79,7 +79,7 @@ List = {
 
 ;;
 
-Zero :> {type t} = {type t = {}}
+Zero :> {type t} = {}
 
 ;;
 
diff --git a/regression.1ml b/regression.1ml
index defd2502..de6d1cfd 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -2,6 +2,13 @@ local import "basis"
 
 ;;
 
+assert b =
+  if not b then
+    Text.print "Assertion failed"
+    System.exit 1
+
+;;
+
 record_inference x = x.works_a_little
 
 ;;
@@ -52,6 +59,16 @@ Equivalence: {
 
 ;;
 
+type MONOID = {type t, empty: t, (++): t -> t ~> t}
+cat (M: MONOID) = List.foldl M.++ M.empty
+do assert (cat {empty = 0, (++) = (+)} (40 :: (2 :: nil)) == 42)
+
+Poly: {type t} = {} ;; Poly 'x = {type t = x}
+do 1: Poly.t
+do "": Poly.t
+
+;;
+
 AmateurOptics = {
   type FUNCTOR = {
     type t a
@@ -274,7 +291,6 @@ N :> {
   type Z
   type S _
 } = {
-  type Z   = {}
   type S _ = {}
 }
 
diff --git a/sub.ml b/sub.ml
index 001bc175..bcf49109 100644
--- a/sub.ml
+++ b/sub.ml
@@ -139,7 +139,7 @@ let rec sub_typ env t1 t2 ps =
     | StrT(tr1), StrT(tr2) ->
       let ts, zs, fs = sub_row env tr1 tr2 ps in
       ts, zs,
-      IL.TupE(List.map2 (fun (l, _) f -> l, IL.AppE(f, IL.DotE(e1, l))) tr2 fs)
+      IL.TupE(List.map2 (fun (l, _) f -> l, f l e1) tr2 fs)
 
     | TupT(tr1), TupT(tr2) ->
       let zs = equal_row env tr1 tr2 ps in
@@ -291,9 +291,19 @@ and sub_row env tr1 tr2 ps =
     [], [], []
   | (l, t2)::tr2' ->
     Trace.sub (lazy ("[sub_row] l = " ^ l));
+    let t1, zs, app =
+      try List.assoc l tr1, [], fun f l x -> IL.AppE(f, IL.DotE(x, l)) with
+      | Not_found ->
+        if is_base_typ t2 && is_small_typ t2
+        then
+          let t, zs = guess_typ (Env.domain_typ env) BaseK in
+          let s = ExT([], t) in
+          TypT(s), zs, fun f _ _ -> IL.AppE(f, IL.LamE("_", erase_extyp s, IL.TupE[]))
+        else
+          raise (Sub (Struct(l, Missing)));
+    in
     let ts1, zs1, f =
-      try sub_typ env (List.assoc l tr1) t2 ps with
-      | Not_found -> raise (Sub (Struct(l, Missing)))
+      try sub_typ env t1 t2 ps with
       | Sub e -> raise (Sub (Struct(l, e)))
     in
     let rec psubst p t =
@@ -305,7 +315,7 @@ and sub_row env tr1 tr2 ps =
     let su = List.map2 psubst (Lib.List.take (List.length ts1) ps) ts1 in
     let ps' = Lib.List.drop (List.length ts1) ps in
     let ts2, zs2, fs = sub_row env tr1 (subst_row su tr2') ps' in
-    ts1 @ ts2, zs1 @ zs2, f::fs
+    ts1 @ ts2, zs @ zs1 @ zs2, app f::fs
 
 and equal_typ env t1 t2 =
   Trace.sub (lazy ("[equal_typ] t1 = " ^ string_of_norm_typ t1));
diff --git a/types.ml b/types.ml
index 7dfc3c9b..07b84678 100644
--- a/types.ml
+++ b/types.ml
@@ -118,6 +118,22 @@ let rec project_typ ls t =
   | _ -> raise Not_found
 
 
+(* *)
+
+let is_base_typ = function
+  | TypT(_) -> true
+  | VarT(_, _)
+  | PrimT(_)
+  | StrT(_)
+  | FunT(_, _, _, _)
+  | WrapT(_)
+  | LamT(_, _)
+  | AppT(_, _)
+  | TupT(_)
+  | DotT(_, _)
+  | RecT(_, _)
+  | InferT(_) -> false
+
 (* Size check *)
 
 let undecidable_flag = ref false
diff --git a/types.mli b/types.mli
index 66532b62..c5166628 100644
--- a/types.mli
+++ b/types.mli
@@ -99,6 +99,9 @@ val diff_row : 'a row -> 'a row -> 'a row
 
 val project_typ : lab list -> typ -> typ (* raise Not_found *)
 
+(* *)
+
+val is_base_typ : typ -> bool
 
 (* Size check *)