diff --git a/src/go/types/NOTES b/src/go/types/NOTES
index e08636cb1a..a75cfb89bf 100644
--- a/src/go/types/NOTES
+++ b/src/go/types/NOTES
@@ -2,16 +2,14 @@ This file works as a sort of notebook/implementation log. It replaces my noteboo
 so we have a better track record. I only switched to this file recently, hence it is incomplete.
 
 TODO
+- type assertions on/against parameterized types
+- no need for error messages where a _ type parameter cannot be inferred (_ cannot be used)
 - use Underlying() to return a type parameter's bound? investigate!
 - better error message when declaring a contract local to a function (parser gets out of sync)
 - if type parameters are repeated in recursive instantiation, they must be the same order (not yet checked)
-- interface embedding doesn't take care of literal type constraints yet
-  (need an allTypes list, like we have an allMethods list?)
-- type assertions on/against parameterized types
 - use []*TypeParam for tparams in subst? (unclear)
 
 OPEN ISSUES
-- a contract that is used earlier than its declaration may not be set up yet
 - instantiating a parameterized function type w/o value or result parameters may have unexpected side-effects
   (we don't make a copy of the signature in some cases) - investigate
 - using a contract and enumerating type arguments currently leads to an error (e.g. func f(type T C(T)) (x T) ... )
diff --git a/src/go/types/README b/src/go/types/README
index 93f15b9f44..c09bb8a3cf 100644
--- a/src/go/types/README
+++ b/src/go/types/README
@@ -6,16 +6,15 @@ This code contains changes to go/types and the go/* support libraries
 to type-check generic code as outlined in the latest contracts proposal
 and presented by Ian Lance Taylor at GopherCon 2019 in San Diego.
 
-CAUTION: PROTOTYPE. THERE ARE KNOWN (AND UNKNOWN) BUGS.
+CAUTION: PROTOTYPE. THERE ARE KNOWN AND UNKNOWN BUGS.
 
 Read and use this code at your own risk.
 
 STATUS
 
-With some exceptions (see below), the most complex aspects of the contracts
-proposal have been implemented and somewhat tested (but expect bugs).
-go/types can now type-check all the *.go2 test files in the testdata and
-examples directories.
+Most aspects of the contracts proposal have been implemented and somewhat
+tested (but expect bugs). go/types can now type-check all the *.go2 test
+files in the testdata and examples directories.
 
 ALTERNATIVE NOTATION
 
@@ -72,19 +71,17 @@ and interfaces and the question if they can be mixed and how.
 Interfaces are the fundamental underlying typing mechanism;
 contracts are syntactic sugar that may improve readability.
 
-KNOWN ISSUES
+MAJOR KNOWN ISSUES
 
 - importing of packages exporting generic code is not implemented
   (and won't be implemented in this prototype)
+- various type-specific operations (such as indexing, sending a
+  message, type assertions, etc.) on expressions of a generic type
+  don't work yet (but are relatively easy to implement going forward)
 - error messages are reasonable but expect them to be significantly
   better in a real implementation (the subscript numbers on type
   parameters are there to visually identify different parameters
   with the same name)
-- embedding of interfaces ignores (the notationally new) type
-  lists in interfaces
-- various type-specific operations (such as indexing, sending a
-  message, etc.) on expressions of a generic type don't work
-  yet (but are relatively easy to implement, going forward)
 - gofmt works only partly with parameterized code
 
 See also the NOTES file for a more up-to-date documentation of the
@@ -93,12 +90,21 @@ current state and issues.
 TO PLAY WITH THIS PROTOTYPE
 
 - Cherry-pick this CL on top of tip (the cherry-pick was tested with
-  tip at 4d5bb9c609):
+  tip at bf26847240):
 
   git fetch "https://go.googlesource.com/go" ... && git cherry-pick FETCH_HEAD
 
   (replace the ... with the respective information from Gerrit's CL page)
 
+- In the go/types directory, verify that the tests run:
+
+  go test
+
+  (If this causes a vet error, run "go test -vet off" instead.)
+
+  Note: This version of go/types is built in "debug" mode (see check.go:17)
+  and does extra checks. As a consequence it may run a bit slower than usual.
+
 - In the go/types directory, build the gotype command:
 
   go build gotype.go
@@ -127,5 +133,6 @@ Updates:
 12/15/2019: Significant progress with much of the functionality present.
 12/19/2019: Several bugs around type bounds checking fixed; more complex examples.
 12/20/2019: Treat contracts as objects, not types anymore. Various bug fixes and more examples.
+1/2/2020: Implemented contract embedding. Various bug fixes.
 
 Change-Id: I29839b5e95d7050fce1dcb3334d3d324883cf76f
diff --git a/src/go/types/builtins.go b/src/go/types/builtins.go
index a68da1205f..2ff8142755 100644
--- a/src/go/types/builtins.go
+++ b/src/go/types/builtins.go
@@ -677,7 +677,7 @@ func (check *Checker) applyTypeFunc(f func(Type) Type, x Type) Type {
 		// construct a suitable new type parameter
 		tpar := NewTypeName(token.NoPos, nil /* = Universe pkg */, "<type parameter>", nil)
 		ptyp := check.NewTypeParam(tpar, 0, nil) // assigns type to tpar as a side-effect
-		ptyp.bound = &Interface{allMethods: markComplete, types: resTypes}
+		ptyp.bound = &Interface{types: resTypes, allMethods: markComplete, allTypes: resTypes}
 
 		return ptyp
 	}
diff --git a/src/go/types/contracts.go b/src/go/types/contracts.go
index 2d83e10225..4ffc9ac771 100644
--- a/src/go/types/contracts.go
+++ b/src/go/types/contracts.go
@@ -254,6 +254,7 @@ func (check *Checker) typeConstraint(typ Type, why *string) bool {
 			check.typeConstraint(t.params, why) &&
 			check.typeConstraint(t.results, why)
 	case *Interface:
+		t.assertCompleteness()
 		for _, m := range t.allMethods {
 			if !check.typeConstraint(m.typ, why) {
 				return false
diff --git a/src/go/types/expr.go b/src/go/types/expr.go
index bd037e2abf..8fc20c8d07 100644
--- a/src/go/types/expr.go
+++ b/src/go/types/expr.go
@@ -513,12 +513,12 @@ func (check *Checker) convertUntyped(x *operand, target Type) {
 	// In case of a type parameter, conversion must succeed against
 	// all types enumerated by the the type parameter bound.
 	if t, _ := target.Underlying().(*TypeParam); t != nil {
-		types := t.Interface().types
+		types := t.Interface().allTypes
 		if len(types) == 0 {
 			goto Error
 		}
 
-		for _, t := range t.Interface().types {
+		for _, t := range types {
 			check.convertUntypedInternal(x, t)
 			if x.mode == invalid {
 				goto Error
diff --git a/src/go/types/infer.go b/src/go/types/infer.go
index 1e3c0a5ea6..ba0830df8b 100644
--- a/src/go/types/infer.go
+++ b/src/go/types/infer.go
@@ -144,9 +144,7 @@ func isParameterized(typ Type, seen map[Type]bool) (res bool) {
 		return isParameterized(t.params, seen) || isParameterized(t.results, seen)
 
 	case *Interface:
-		if t.allMethods == nil {
-			panic("incomplete method")
-		}
+		t.assertCompleteness()
 		for _, m := range t.allMethods {
 			if isParameterized(m.typ, seen) {
 				return true
diff --git a/src/go/types/subst.go b/src/go/types/subst.go
index ab311bf3a8..e168c1aa26 100644
--- a/src/go/types/subst.go
+++ b/src/go/types/subst.go
@@ -108,14 +108,14 @@ func (check *Checker) instantiate(pos token.Pos, typ Type, targs []Type, poslist
 		}
 
 		// targ's underlying type must also be one of the interface types listed, if any
-		if len(iface.types) == 0 {
+		if len(iface.allTypes) == 0 {
 			break // nothing to do
 		}
 
 		// if targ is itself a type parameter, each of its possible types must be in the
 		// list of iface types (i.e., the targ type list must be a subset of the iface types)
 		if targ, _ := targ.Underlying().(*TypeParam); targ != nil {
-			for _, t := range targ.Interface().types {
+			for _, t := range targ.Interface().allTypes {
 				if !iface.includes(t.Underlying()) {
 					// TODO(gri) match this error message with the one below (or vice versa)
 					check.softErrorf(pos, "%s does not satisfy %s (missing type %s)", targ, tpar.bound, t)
@@ -126,7 +126,7 @@ func (check *Checker) instantiate(pos token.Pos, typ Type, targs []Type, poslist
 		}
 
 		// otherwise, targ's underlying type must also be one of the interface types listed, if any
-		if len(iface.types) > 0 {
+		if len(iface.allTypes) > 0 {
 			// TODO(gri) must it be the underlying type, or should it just be the type? (spec question)
 			if !iface.includes(targ.Underlying()) {
 				check.softErrorf(pos, "%s does not satisfy %s (%s not found in %s)", targ, tpar.bound, targ, iface)
@@ -229,11 +229,12 @@ func (subst *subster) typ(typ Type) Type {
 
 	case *Interface:
 		methods, mcopied := subst.funcList(t.methods)
-		embeddeds, ecopied := subst.typeList(t.embeddeds)
 		types, tcopied := subst.typeList(t.types)
-		if mcopied || ecopied || tcopied {
-			iface := &Interface{methods: methods, embeddeds: embeddeds, types: types}
-			iface.Complete()
+		embeddeds, ecopied := subst.typeList(t.embeddeds)
+		if mcopied || tcopied || ecopied {
+			iface := &Interface{methods: methods, types: types, embeddeds: embeddeds}
+			subst.check.posMap[iface] = subst.check.posMap[t] // satisfy completeInterface requirement
+			subst.check.completeInterface(token.NoPos, iface)
 			return iface
 		}
 
diff --git a/src/go/types/testdata/contracts.go2 b/src/go/types/testdata/contracts.go2
index 8fee9f8493..43f228b471 100644
--- a/src/go/types/testdata/contracts.go2
+++ b/src/go/types/testdata/contracts.go2
@@ -99,6 +99,19 @@ type myTab struct{ myTa }
 
 func (myTab) b()
 
+contract E5(T) {
+        T int
+}
+
+contract E6(T) {
+        E5(T)
+        E5(T)
+}
+
+func _(type T E6)(x T) T {
+        return x + 1
+}
+
 // --------------------------------------------------------------------------------------
 // Contract satisfaction
 
diff --git a/src/go/types/testdata/tmp.go2 b/src/go/types/testdata/tmp.go2
index 64170db098..9f577750b4 100644
--- a/src/go/types/testdata/tmp.go2
+++ b/src/go/types/testdata/tmp.go2
@@ -4,35 +4,10 @@
 
 package p
 
-contract C1(a, b, c) {
-        a a()
-        b b()
-        c c()
-}
+type B1 interface{type int}
 
-contract C2(a, b) {
-        C1(a, b, b)
-}
+type T3(type P B1) P
 
-func f(type T, _ C2)(x T)
+type B2 interface{type int, string}
 
-type X struct{}
-
-func (X) a()
-//func (X) b()
-//func (X) c()
-
-func _() {
-        var x X
-        f(X, int)(x)
-}
-
-contract C3(x) {
-        C4(x)
-}
-
-contract C4(x) {
-//        C3(x)
-}
-
-contract C(A) { A C /* ERROR use of contract */ }
\ No newline at end of file
+func _(type P B2)(x T3(P /* ERROR missing type string */ ))
\ No newline at end of file
diff --git a/src/go/types/type.go b/src/go/types/type.go
index 94e9fef5dc..af56e87892 100644
--- a/src/go/types/type.go
+++ b/src/go/types/type.go
@@ -245,16 +245,16 @@ func (s *Signature) Variadic() bool { return s.variadic }
 // An Interface represents an interface type.
 type Interface struct {
 	methods   []*Func // ordered list of explicitly declared methods
+	types     []Type  // list of explicitly declared types (for contracts)
 	embeddeds []Type  // ordered list of explicitly embedded types
 
 	allMethods []*Func // ordered list of methods declared with or embedded in this interface (TODO(gri): replace with mset)
-
-	types []Type // for contracts
+	allTypes   []Type  // list of types declared with or embedded in this interface
 }
 
 // is reports whether interface t represents types that all satisfy pred.
 func (t *Interface) is(pred func(Type) bool) bool {
-	for _, t := range t.types {
+	for _, t := range t.allTypes {
 		if !pred(t) {
 			return false
 		}
@@ -363,7 +363,7 @@ func (t *Interface) Empty() bool { t.assertCompleteness(); return len(t.allMetho
 
 // includes reports whether the interface t includes the type typ.
 func (t *Interface) includes(typ Type) bool {
-	for _, t := range t.types {
+	for _, t := range t.allTypes {
 		if Identical(t, typ) {
 			return true
 		}
@@ -403,12 +403,16 @@ func (t *Interface) Complete() *Interface {
 		addMethod(m, true)
 	}
 
+	var types []Type
+	types = append(types, t.types...)
+
 	for _, typ := range t.embeddeds {
 		typ := typ.Underlying().(*Interface)
 		typ.Complete()
 		for _, m := range typ.allMethods {
 			addMethod(m, false)
 		}
+		types = append(types, typ.types...)
 	}
 
 	for i := 0; i < len(todo); i += 2 {
@@ -423,6 +427,7 @@ func (t *Interface) Complete() *Interface {
 		sort.Sort(byUniqueMethodName(methods))
 		t.allMethods = methods
 	}
+	t.allTypes = types
 
 	return t
 }
@@ -541,7 +546,9 @@ func (check *Checker) NewTypeParam(obj *TypeName, index int, bound Type) *TypePa
 }
 
 func (t *TypeParam) Interface() *Interface {
-	return t.bound.Underlying().(*Interface)
+	iface := t.bound.Underlying().(*Interface)
+	iface.Complete() // TODO(gri) should we use check.completeInterface instead?
+	return iface
 }
 
 // Implementations for Type methods.
diff --git a/src/go/types/typestring.go b/src/go/types/typestring.go
index c8f23ffa17..3b771a0e27 100644
--- a/src/go/types/typestring.go
+++ b/src/go/types/typestring.go
@@ -178,10 +178,10 @@ func writeType(buf *bytes.Buffer, typ Type, qf Qualifier, visited []Type) {
 				writeSignature(buf, m.typ.(*Signature), qf, visited)
 				empty = false
 			}
-			if !empty && len(t.types) > 0 {
+			if !empty && len(t.allTypes) > 0 {
 				buf.WriteString("; ")
 			}
-			for i, typ := range t.types {
+			for i, typ := range t.allTypes {
 				if i > 0 {
 					buf.WriteString(", ")
 				}
diff --git a/src/go/types/typexpr.go b/src/go/types/typexpr.go
index 6fd9d9d634..6b741c9058 100644
--- a/src/go/types/typexpr.go
+++ b/src/go/types/typexpr.go
@@ -630,7 +630,7 @@ func (check *Checker) interfaceType(ityp *Interface, iface *ast.InterfaceType, d
 	// type constraints
 	ityp.types = check.collectTypeConstraints(iface.Pos(), ityp.types, iface.Types)
 
-	if len(ityp.methods) == 0 && len(ityp.embeddeds) == 0 {
+	if len(ityp.methods) == 0 && len(ityp.types) == 0 && len(ityp.embeddeds) == 0 {
 		// empty interface
 		ityp.allMethods = markComplete
 		return
@@ -668,7 +668,7 @@ func (check *Checker) completeInterface(pos token.Pos, ityp *Interface) {
 		check.indent++
 		defer func() {
 			check.indent--
-			check.trace(pos, "=> %s", ityp)
+			check.trace(pos, "=> %s (methods = %v, types = %v)", ityp, ityp.allMethods, ityp.allTypes)
 		}()
 	}
 
@@ -718,6 +718,11 @@ func (check *Checker) completeInterface(pos token.Pos, ityp *Interface) {
 		addMethod(m.pos, m, true)
 	}
 
+	// collect types
+	// TODO(gri) report error for multiply explicitly declared identical types
+	var types []Type
+	types = append(types, ityp.types...)
+
 	posList := check.posMap[ityp]
 	for i, typ := range ityp.embeddeds {
 		pos := posList[i] // embedding position
@@ -731,12 +736,14 @@ func (check *Checker) completeInterface(pos token.Pos, ityp *Interface) {
 		for _, m := range typ.allMethods {
 			addMethod(pos, m, false) // use embedding position pos rather than m.pos
 		}
+		types = append(types, typ.allTypes...)
 	}
 
 	if methods != nil {
 		sort.Sort(byUniqueMethodName(methods))
 		ityp.allMethods = methods
 	}
+	ityp.allTypes = types
 }
 
 // byUniqueTypeName named type lists can be sorted by their unique type names.