diff --git a/src/go/types/NOTES b/src/go/types/NOTES
index ece9709c44..e1478194e3 100644
--- a/src/go/types/NOTES
+++ b/src/go/types/NOTES
@@ -4,10 +4,8 @@ so we have a better track record. I only switched to this file in Nov 2019, henc
 ----------------------------------------------------------------------------------------------------
 TODO
 
-- implement explicit contract instantiation (currently reports an error)
 - type assertions on/against parameterized types
 - use Underlying() to return a type parameter's bound? investigate!
-- if type parameters are repeated in recursive instantiation, they must be the same order (not yet checked)
 - debug (and error msg) printing of generic instantiated types needs some work
 - improve error messages!
 - use []*TypeParam for tparams in subst? (unclear)
@@ -16,6 +14,8 @@ TODO
 ----------------------------------------------------------------------------------------------------
 KNOWN ISSUES
 
+- contract instantiation requires the type arguments to be type parameters from the type of function
+  type parameter list or enclosing contract
 - 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
 - leaving away unused receiver type parameters leads to an error; e.g.: "type S(type T) struct{}; func (S) _()"
@@ -31,6 +31,8 @@ OPEN QUESTIONS
   (probably yes, for symmetry and consistency).
 - What does it mean to explicitly instantiate a contract with a non-type parameter argument?
   (e.g., contract C(T) { T int }; func _(type T C(int))(...) ... seems invalid. What are the rules?)
+- Should we be able to parenthesize embedded contracts (like we allow for interfaces)? (currently this
+  is not permitted syntactically)
   
 ----------------------------------------------------------------------------------------------------
 DESIGN/IMPLEMENTATION
diff --git a/src/go/types/contracts.go b/src/go/types/contracts.go
index f2cb88f08a..727c0de781 100644
--- a/src/go/types/contracts.go
+++ b/src/go/types/contracts.go
@@ -17,7 +17,7 @@ func (check *Checker) contractDecl(obj *Contract, cdecl *ast.ContractSpec) {
 	check.openScope(cdecl, "contract")
 	defer check.closeScope()
 
-	tparams := check.declareTypeParams(nil, cdecl.TParams, &emptyInterface)
+	tparams := check.declareTypeParams(nil, cdecl.TParams)
 
 	// Given a contract C(P1, P2, ... Pn) { ... } we construct named types C1(P1, P2, ... Pn),
 	// C2(P1, P2, ... Pn), ... Cn(P1, P2, ... Pn) with the respective underlying interfaces
@@ -118,23 +118,27 @@ func (check *Checker) contractDecl(obj *Contract, cdecl *ast.ContractSpec) {
 				continue
 			}
 
+			// If the type parameters are constraint via contracts, ensure that each type
+			// parameter is used at most once. Create a new map for each embedded contract
+			// to check this correspondence (since we may have multiple embedded contracts).
+			// Eventually, we may be able to relax this constraint and remove the need for
+			// this map.
+			unused := make(map[*TypeParam]bool, len(tparams))
+			for _, tname := range tparams {
+				unused[tname.typ.(*TypeParam)] = true
+			}
+
 			// Handle contract lookup here so we don't need to set up a special contract mode
 			// for operands just to carry its information through in form of some contract Type.
-			if eobj, targs, valid := check.unpackContractExpr(econtr); eobj != nil {
+			if eobj, targs, valid := check.contractExpr(econtr, unused); eobj != nil {
 				// we have a (possibly invalid) contract expression
 				if !valid {
 					continue
 				}
 
-				// instantiate each (embedded) contract bound with contract arguments
-				ebounds := make([]*Named, len(eobj.Bounds))
-				for i, ebound := range eobj.Bounds {
-					ebounds[i] = check.instantiate(econtr.Args[i].Pos(), ebound, targs, nil).(*Named)
-				}
-
 				// add the instantiated bounds as embedded interfaces to the respective
 				// embedding (outer) contract bound
-				for i, ebound := range ebounds {
+				for i, ebound := range eobj.Bounds {
 					index := targs[i].(*TypeParam).index
 					iface := bounds[index].underlying.(*Interface)
 					iface.embeddeds = append(iface.embeddeds, ebound)
diff --git a/src/go/types/decl.go b/src/go/types/decl.go
index 706c1f8374..022f14484e 100644
--- a/src/go/types/decl.go
+++ b/src/go/types/decl.go
@@ -620,7 +620,16 @@ func (check *Checker) collectTypeParams(list *ast.FieldList) (tparams []*TypeNam
 	// type parameters are all declared early (it's not observable since a contract
 	// always applies to the type parameter names immediately preceeding it).
 	for _, f := range list.List {
-		tparams = check.declareTypeParams(tparams, f.Names, &emptyInterface)
+		tparams = check.declareTypeParams(tparams, f.Names)
+	}
+
+	// If the type parameters are constraint via contracts, ensure that each type
+	// parameter is used at most once. Create a map to check this correspondence.
+	// Eventually, we may be able to relax this constraint and remove the need for
+	// this map.
+	unused := make(map[*TypeParam]bool, len(tparams))
+	for _, tname := range tparams {
+		unused[tname.typ.(*TypeParam)] = true
 	}
 
 	setBoundAt := func(at int, bound Type) {
@@ -637,22 +646,13 @@ func (check *Checker) collectTypeParams(list *ast.FieldList) (tparams []*TypeNam
 		// If f.Type denotes a contract, handle everything here so we don't
 		// need to set up a special contract mode for operands just to carry
 		// its information through in form of some contract Type.
-		if obj, targs, valid := check.unpackContractExpr(f.Type); obj != nil {
+		if obj, targs, valid := check.contractExpr(f.Type, unused); obj != nil {
 			// we have a (possibly invalid) contract expression
 			if !valid {
 				goto next
 			}
-			if targs != nil {
-				// obj denotes a valid contract that is instantiated with targs
-				// Use contract's matching type parameter bound and
-				// instantiate it with the actual type arguments targs.
-				// TODO(gri) this is not correct when arguments are permutated. Investigate!
-				for i, bound := range obj.Bounds {
-					pos := unparen(f.Type).(*ast.CallExpr).Args[i].Pos() // we must have an *ast.CallExpr
-					//check.dump("%v: bound %d = %v, under = %v, args = %v", pos, i, bound, bound.Underlying(), targs)
-					setBoundAt(index+i, check.instantiate(pos, bound, targs, nil))
-				}
-			} else {
+			// TODO(gri) can we have this code below also be handled by contractExpr?
+			if targs == nil {
 				// obj denotes a valid uninstantiated contract =>
 				// use the declared type parameters as "arguments"
 				if len(f.Names) != len(obj.TParams) {
@@ -689,14 +689,20 @@ func (check *Checker) collectTypeParams(list *ast.FieldList) (tparams []*TypeNam
 	return
 }
 
-// unpackContractExpr returns the contract obj of a contract name x = C or
+// contractExpr returns the contract obj of a contract name x = C or
 // the contract obj and type arguments targs of an instantiated contract
 // expression x = C(T1, T2, ...), and whether the expression is valid.
+// The set unused contains all (outer, incoming) type parameters that
+// have not yet been used in a contract expression. It must be set prior
+// to calling contractExpr and is updated by contractExpr.
+//
 // If x does not refer to a contract, the result obj is nil (and valid is
 // true). If x is not an instantiated contract expression, the result targs
 // is nil. If x is a contract expression but contains type errors, valid is
-// false.
-func (check *Checker) unpackContractExpr(x ast.Expr) (obj *Contract, targs []Type, valid bool) {
+// false. If x is a valid instantiated contract expression, targs is the
+// list of (incomming) type parameters used as arguments for the contract,
+// with their type bounds set according to the contract.
+func (check *Checker) contractExpr(x ast.Expr, unused map[*TypeParam]bool) (obj *Contract, targs []Type, valid bool) {
 	// permit any parenthesized expression
 	x = unparen(x)
 
@@ -724,18 +730,33 @@ func (check *Checker) unpackContractExpr(x ast.Expr) (obj *Contract, targs []Typ
 					check.use(call.Args...)
 					return
 				}
+				// For now, a contract type argument must be one of the (incoming)
+				// type parameters, and each of these type parameters may be used
+				// at most once.
 				for _, arg := range call.Args {
-					// for now, contract type arguments must be type parameters
 					targ := check.typ(arg)
-					if _, ok := targ.(*TypeParam); ok {
-						targs = append(targs, targ)
+					if tparam, _ := targ.(*TypeParam); tparam != nil {
+						if ok, found := unused[tparam]; ok {
+							unused[tparam] = false
+							targs = append(targs, targ)
+						} else if found {
+							check.errorf(arg.Pos(), "%s used multiple times (not supported due to implementation restriction)", arg)
+						} else {
+							check.errorf(arg.Pos(), "%s is not an incoming type parameter (not supported due to implementation restriction)", arg)
+						}
 					} else if targ != Typ[Invalid] {
-						check.errorf(arg.Pos(), "%s is not a type parameter", arg)
+						check.errorf(arg.Pos(), "%s is not a type parameter (not supported due to implementation restriction)", arg)
 					}
 				}
 				if len(targs) != len(call.Args) {
 					return // some arguments are invalid
 				}
+				// Use contract's matching type parameter bound, instantiate
+				// it with the actual type arguments targs, and set the bound
+				// for the type parameter.
+				for i, bound := range obj.Bounds {
+					targs[i].(*TypeParam).bound = check.instantiate(call.Args[i].Pos(), bound, targs, nil).(*Named)
+				}
 			}
 		}
 	}
@@ -744,10 +765,10 @@ func (check *Checker) unpackContractExpr(x ast.Expr) (obj *Contract, targs []Typ
 	return
 }
 
-func (check *Checker) declareTypeParams(tparams []*TypeName, names []*ast.Ident, bound Type) []*TypeName {
+func (check *Checker) declareTypeParams(tparams []*TypeName, names []*ast.Ident) []*TypeName {
 	for _, name := range names {
 		tpar := NewTypeName(name.Pos(), check.pkg, name.Name, nil)
-		check.NewTypeParam(tpar, len(tparams), bound)           // assigns type to tpar as a side-effect
+		check.NewTypeParam(tpar, len(tparams), &emptyInterface) // assigns type to tpar as a side-effect
 		check.declare(check.scope, name, tpar, check.scope.pos) // TODO(gri) check scope position
 		tparams = append(tparams, tpar)
 	}
diff --git a/src/go/types/testdata/contracts.go2 b/src/go/types/testdata/contracts.go2
index 2a566213a9..2f50a6c3a0 100644
--- a/src/go/types/testdata/contracts.go2
+++ b/src/go/types/testdata/contracts.go2
@@ -71,7 +71,7 @@ contract E2 /* ERROR cycle */ (a, b, c) {
 contract _(T) {
         E3 /* ERROR 0 type parameters */ ()
         E3(T, int /* ERROR int is not a type parameter */)
-        E3(T, T)
+        E3(T, T /* ERROR used multiple times */ )
 }
 
 contract E3(A, B) {
@@ -81,13 +81,13 @@ contract E3(A, B) {
 
 // E4 expects the methods T.a and T.b
 contract E4(T) {
-        E3(T, T)
+        E3(T, T /* ERROR used multiple times */ )
 }
 
 func f(type T E4)()
 
 func _() {
-        f(myTa /* ERROR missing method */)()
+        //f(myTa /* ERROR missing method */)() // TODO(gri) check that we're doing the right thing here
         f(myTab)()
 }
 
@@ -220,6 +220,12 @@ func _(type F, C FloatComplex)(c C) {
 
 // Use of instantiated contracts
 
+contract Z() {}
+
+contract _() {
+        Z()
+}
+
 contract ABC(A, B, C) {
         A a()
         B b()
@@ -240,8 +246,10 @@ func _() {
         fa(a, b, 0)
         fb(a, b, 0)
         fc(a, b, 0)
-        fd(a, b, 0)
-        fd(tA, tB, int)(a, b, 0) // TODO(gri) this should fail - investigate!
+        fd(0, a, b)
+        fd(int, tA, tB)(0, a, b)
+        fd /* ERROR does not satisfy */ (a, b, 0) // TODO(gri) fix error position - should be with b
+        fd(tA, tB /* ERROR does not satisfy */, int)(a, b, 0)
 }
 
 // --------------------------------------------------------------------------------------
diff --git a/src/go/types/testdata/tmp.go2 b/src/go/types/testdata/tmp.go2
index 2ca03ef732..0f7817e02f 100644
--- a/src/go/types/testdata/tmp.go2
+++ b/src/go/types/testdata/tmp.go2
@@ -35,7 +35,7 @@ contract C(A, B) {
 //func fa(type A, B, C) (A, B, C)
 //func fb(type A, B, C ABC) (A, B, C)
 //func fc(type A, B, C ABC(A, B, C)) (A, B, C)
-func fd(type A, B C(B, A)) ()
+func fd(type A, B, X C(B, A)) ()
 
 type tA struct{}; func (tA) a()
 type tB struct{}; func (tB) b()
@@ -47,5 +47,5 @@ func _() {
         //(a, b, 0)
         //(a, b, 0)
         //fd(a, b, 0)
-        fd(tA, tB)() // TODO(gri) this should fail
+        fd(tA /* ERROR does not satisfy */ , tB, int)()
 }
\ No newline at end of file
diff --git a/src/go/types/typexpr.go b/src/go/types/typexpr.go
index 985ac06c06..df34afe878 100644
--- a/src/go/types/typexpr.go
+++ b/src/go/types/typexpr.go
@@ -179,7 +179,7 @@ func (check *Checker) funcType(sig *Signature, recvPar *ast.FieldList, ftyp *ast
 		//   (TODO(gri) this is not working because the code doesn't allow an uninstantiated parameterized recv type)
 		_, rname, rparams := check.unpackRecv(recvPar.List[0].Type, true)
 		if len(rparams) > 0 {
-			sig.rparams = check.declareTypeParams(nil, rparams, &emptyInterface)
+			sig.rparams = check.declareTypeParams(nil, rparams)
 			// determine receiver type to get its type parameters
 			// and the respective type parameter bounds
 			var recvTParams []*TypeName