diff --git a/cue/ast.go b/cue/ast.go
index 3a5db12..4c2dcf7 100644
--- a/cue/ast.go
+++ b/cue/ast.go
@@ -230,17 +230,43 @@
 			v1.doc = v.doc
 		}
 		ret = obj
-		for _, e := range n.Elts {
+		for i, e := range n.Elts {
 			switch x := e.(type) {
+			case *ast.Ellipsis:
+				if i != len(n.Elts)-1 {
+					return v1.walk(x.Type) // Generate an error
+				}
+				f := v.ctx().label("_", true)
+				sig := &params{}
+				sig.add(f, &basicType{newNode(x), stringKind})
+				template := &lambdaExpr{newNode(x), sig, &top{newNode(x)}}
+				v1.object.addTemplate(v.ctx(), token.NoPos, template)
+
 			case *ast.EmbedDecl:
-				// Only allowed at top-level.
-				return v1.errf(x, "emitting values is only allowed at top level")
+				e := v1.walk(x.Expr)
+				if isBottom(e) {
+					return e
+				}
+				if e.kind()&structKind == 0 {
+					return v1.errf(x, "can only embed structs (found %v)", e.kind())
+				}
+				ret = mkBin(v1.ctx(), x.Pos(), opUnifyUnchecked, ret, e)
+				obj = &structLit{}
+				v1.object = obj
+				ret = mkBin(v1.ctx(), x.Pos(), opUnifyUnchecked, ret, obj)
+
 			case *ast.Field, *ast.Alias:
 				v1.walk(e)
+
 			case *ast.ComprehensionDecl:
 				v1.walk(x)
 			}
 		}
+		if v.ctx().inDefinition > 0 {
+			// For embeddings this is handled in binOp, in which case the
+			// isClosed bit is cleared if a template is introduced.
+			obj.isClosed = obj.template == nil
+		}
 		if passDoc {
 			v.doc = v1.doc // signal usage of document back to parent.
 		}
@@ -271,10 +297,14 @@
 		ret = list
 
 	case *ast.Ellipsis:
-		return v.errf(n, "ellipsis (...) only allowed at end of list")
+		return v.errf(n, "ellipsis (...) only allowed at end of list or struct")
 
 	case *ast.ComprehensionDecl:
-		yielder := &yield{baseValue: newExpr(n.Field.Value)}
+		yielder := &yield{
+			baseValue: newExpr(n.Field.Value),
+			opt:       n.Field.Optional != token.NoPos,
+			def:       n.Field.Token == token.ISA,
+		}
 		fc := &fieldComprehension{
 			baseValue: newDecl(n),
 			clauses:   wrapClauses(v, yielder, n.Clauses),
@@ -334,6 +364,12 @@
 
 	case *ast.Field:
 		opt := n.Optional != token.NoPos
+		isDef := n.Token == token.ISA
+		if isDef {
+			ctx := v.ctx()
+			ctx.inDefinition++
+			defer func() { ctx.inDefinition-- }()
+		}
 		switch x := n.Label.(type) {
 		case *ast.Interpolation:
 			v.sel = "?"
@@ -345,9 +381,13 @@
 			yielder.key = v.walk(x)
 			yielder.value = v.walk(n.Value)
 			yielder.opt = opt
+			yielder.def = isDef
 			v.object.comprehensions = append(v.object.comprehensions, fc)
 
 		case *ast.TemplateLabel:
+			if isDef {
+				v.errf(x, "map element type cannot be a definition")
+			}
 			v.sel = "*"
 			f := v.label(x.Ident.Name, true)
 
@@ -358,11 +398,7 @@
 			v.setScope(n, template)
 			template.value = v.walk(n.Value)
 
-			if v.object.template == nil {
-				v.object.template = template
-			} else {
-				v.object.template = mkBin(v.ctx(), token.NoPos, opUnify, v.object.template, template)
-			}
+			v.object.addTemplate(v.ctx(), token.NoPos, template)
 
 		case *ast.BasicLit, *ast.Ident:
 			if internal.DropOptional && opt {
@@ -392,7 +428,7 @@
 					}
 				}
 				val := v.walk(n.Value)
-				v.object.insertValue(v.ctx(), f, opt, val, attrs, v.doc)
+				v.object.insertValue(v.ctx(), f, opt, isDef, val, attrs, v.doc)
 				v.doc = leftOverDoc
 			}
 
@@ -445,6 +481,8 @@
 
 			case "len":
 				return lenBuiltin
+			case "close":
+				return closeBuiltin
 			case "and":
 				return andBuiltin
 			case "or":
diff --git a/cue/binop.go b/cue/binop.go
index b52150c..99ad043 100644
--- a/cue/binop.go
+++ b/cue/binop.go
@@ -183,6 +183,8 @@
 	panic("unreachable: special-cased")
 }
 
+// add adds to a unification. Note that the value cannot be a struct and thus
+// there is no need to distinguish between checked and unchecked unification.
 func (x *unification) add(ctx *context, src source, v evaluated) evaluated {
 	for progress := true; progress; {
 		progress = false
@@ -218,7 +220,8 @@
 }
 
 func (x *unification) binOp(ctx *context, src source, op op, other evaluated) evaluated {
-	if op == opUnify {
+	if _, isUnify := op.unifyType(); isUnify {
+		// Cannot be checked unification.
 		u := &unification{baseValue: baseValue{src}}
 		u.values = append(u.values, x.values...)
 		if y, ok := other.(*unification); ok {
@@ -237,7 +240,7 @@
 
 func (x *top) binOp(ctx *context, src source, op op, other evaluated) evaluated {
 	switch op {
-	case opUnify:
+	case opUnify, opUnifyUnchecked:
 		return other
 	}
 	src = mkBin(ctx, src.Pos(), op, x, other)
@@ -328,7 +331,7 @@
 
 	newSrc := binSrc(src.Pos(), op, x, other)
 	switch op {
-	case opUnify:
+	case opUnify, opUnifyUnchecked:
 		k, _, msg := matchBinOpKind(opUnify, x.kind(), other.kind())
 		if k == bottomKind {
 			return ctx.mkErr(src, msg, opUnify, ctx.str(x), ctx.str(other), x.kind(), other.kind())
@@ -495,7 +498,7 @@
 func (x *customValidator) binOp(ctx *context, src source, op op, other evaluated) evaluated {
 	newSrc := binSrc(src.Pos(), op, x, other)
 	switch op {
-	case opUnify:
+	case opUnify, opUnifyUnchecked:
 		k, _, msg := matchBinOpKind(opUnify, x.kind(), other.kind())
 		if k == bottomKind {
 			return ctx.mkErr(src, msg, op, ctx.str(x), ctx.str(other), x.kind(), other.kind())
@@ -582,7 +585,7 @@
 
 func (x *structLit) binOp(ctx *context, src source, op op, other evaluated) evaluated {
 	y, ok := other.(*structLit)
-	_, isUnify := op.unifyType()
+	unchecked, isUnify := op.unifyType()
 	if !ok || !isUnify {
 		return ctx.mkIncompatible(src, op, x, other)
 	}
@@ -599,6 +602,7 @@
 		binSrc(src.Pos(), op, x, other), // baseValue
 		x.emit,                          // emit
 		nil,                             // template
+		x.isClosed || y.isClosed,        // isClosed
 		nil,                             // comprehensions
 		arcs,                            // arcs
 		nil,                             // attributes
@@ -629,6 +633,8 @@
 	if t != nil {
 		obj.template = ctx.copy(t)
 	}
+	// If unifying with a closed struct that does not have a template,
+	// we need to apply the template to all elements.
 
 	sz := len(x.comprehensions) + len(y.comprehensions)
 	obj.comprehensions = make([]*fieldComprehension, sz)
@@ -640,15 +646,38 @@
 	}
 
 	for _, a := range x.arcs {
+		found := false
+		for _, b := range y.arcs {
+			if a.feature == b.feature {
+				found = true
+				break
+			}
+		}
+		if !unchecked && !found && !y.allows(a.feature) {
+			if a.optional {
+				continue
+			}
+			return ctx.mkErr(src, y, "field %q not allowed in closed struct",
+				ctx.labelStr(a.feature))
+		}
 		cp := ctx.copy(a.v)
 		obj.arcs = append(obj.arcs,
-			arc{a.feature, a.optional, cp, nil, a.attrs, a.docs})
+			arc{a.feature, a.optional, a.definition, cp, nil, a.attrs, a.docs})
 	}
 outer:
 	for _, a := range y.arcs {
 		v := ctx.copy(a.v)
+		found := false
 		for i, b := range obj.arcs {
 			if a.feature == b.feature {
+				found = true
+				if a.definition != b.definition {
+					src := binSrc(x.Pos(), op, a.v, b.v)
+					return ctx.mkErr(src, "field %q declared as definition and regular field",
+						ctx.labelStr(a.feature))
+				}
+				// TODO: using opUnify here disables recursive opening in
+				// embedding. Change to op enable it.
 				v = mkBin(ctx, src.Pos(), opUnify, b.v, v)
 				obj.arcs[i].v = v
 				obj.arcs[i].cache = nil
@@ -662,11 +691,22 @@
 				continue outer
 			}
 		}
+		if !unchecked && !found && !x.allows(a.feature) {
+			if a.optional {
+				continue
+			}
+			return ctx.mkErr(a.v, x, "field %q not allowed in closed struct",
+				ctx.labelStr(a.feature))
+		}
 		a.setValue(v)
 		obj.arcs = append(obj.arcs, a)
 	}
 	sort.Stable(obj)
 
+	if unchecked && obj.template != nil {
+		obj.isClosed = false
+	}
+
 	return obj
 }
 
diff --git a/cue/builtin.go b/cue/builtin.go
index dc73586..c6fc328 100644
--- a/cue/builtin.go
+++ b/cue/builtin.go
@@ -91,7 +91,7 @@
 		for _, a := range pkg.arcs {
 			// Discard option status and attributes at top level.
 			// TODO: filter on capitalized fields?
-			obj.insertValue(ctx, a.feature, false, a.v, nil, a.docs)
+			obj.insertValue(ctx, a.feature, false, false, a.v, nil, a.docs)
 		}
 	}
 
@@ -138,6 +138,20 @@
 	},
 }
 
+var closeBuiltin = &builtin{
+	Name:   "close",
+	Params: []kind{structKind},
+	Result: structKind,
+	Func: func(c *callCtxt) {
+		s, ok := c.args[0].(*structLit)
+		if !ok {
+			c.ret = errors.Newf(c.args[0].Pos(), "struct argument must be concrete")
+			return
+		}
+		c.ret = s.close()
+	},
+}
+
 var andBuiltin = &builtin{
 	Name:   "and",
 	Params: []kind{listKind},
diff --git a/cue/context.go b/cue/context.go
index 9fa7323..29c50a1 100644
--- a/cue/context.go
+++ b/cue/context.go
@@ -31,8 +31,9 @@
 	constraints []*binaryExpr
 	evalStack   []bottom
 
-	inSum    int
-	cycleErr bool
+	inDefinition int
+	inSum        int
+	cycleErr     bool
 
 	noManifest bool
 
diff --git a/cue/copy.go b/cue/copy.go
index 5a6594b..a28eaa2 100644
--- a/cue/copy.go
+++ b/cue/copy.go
@@ -31,7 +31,7 @@
 	case *structLit:
 		arcs := make(arcs, len(x.arcs))
 
-		obj := &structLit{x.baseValue, nil, nil, nil, arcs, nil}
+		obj := &structLit{x.baseValue, nil, nil, x.isClosed, nil, arcs, nil}
 
 		defer ctx.pushForwards(x, obj).popForwards()
 
diff --git a/cue/debug.go b/cue/debug.go
index d7bfede..1db9eff 100644
--- a/cue/debug.go
+++ b/cue/debug.go
@@ -267,8 +267,19 @@
 		if p.showNodeRef {
 			p.writef("<%s>", p.ctx.ref(x))
 		}
-		writef("{")
-		if x.template != nil {
+		if x.isClosed {
+			write("C")
+		}
+		write("{")
+		topDefault := false
+		switch {
+		case x.template != nil:
+			lambda, ok := x.template.(*lambdaExpr)
+			if ok {
+				if _, topDefault = lambda.value.(*top); topDefault {
+					break
+				}
+			}
 			write("<>: ")
 			p.str(x.template)
 			write(", ")
@@ -280,6 +291,12 @@
 				p.write(", ")
 			}
 		}
+		if topDefault && !x.isClosed {
+			if len(x.arcs) > 0 {
+				p.write(", ")
+			}
+			p.write("...")
+		}
 		write("}")
 
 	case []arc:
@@ -302,7 +319,11 @@
 		if x.optional {
 			p.write("?")
 		}
-		p.write(": ")
+		if x.definition {
+			p.write(" :: ")
+		} else {
+			p.write(": ")
+		}
 		p.str(n)
 		if x.attrs != nil {
 			for _, a := range x.attrs.attr {
diff --git a/cue/eval.go b/cue/eval.go
index 3a99033..0a36b21 100644
--- a/cue/eval.go
+++ b/cue/eval.go
@@ -67,7 +67,7 @@
 		}
 		if n.val() == nil {
 			field := ctx.labelStr(x.feature)
-			if _, ok := sc.(*structLit); ok {
+			if st, ok := sc.(*structLit); ok && !st.isClosed {
 				return ctx.mkErr(x, codeIncomplete, "undefined field %q", field)
 			}
 			//	m.foo undefined (type map[string]bool has no field or method foo)
@@ -105,7 +105,10 @@
 				return ctx.mkErr(x, index, codeIncomplete, "field %q is optional", s)
 			}
 			if n.val() == nil {
-				return ctx.mkErr(x, index, codeIncomplete, "undefined field %q", s)
+				if !v.isClosed {
+					return ctx.mkErr(x, index, codeIncomplete, "undefined field %q", s)
+				}
+				return ctx.mkErr(x, index, "undefined field %q", s)
 			}
 			return n.cache
 		}
@@ -252,7 +255,7 @@
 func (x *listComprehension) evalPartial(ctx *context) evaluated {
 	s := &structLit{baseValue: x.baseValue}
 	list := &list{baseValue: x.baseValue, elem: s}
-	result := x.clauses.yield(ctx, func(k, v evaluated, _ bool) *bottom {
+	result := x.clauses.yield(ctx, func(k, v evaluated, _, _ bool) *bottom {
 		if !k.kind().isAnyOf(intKind) {
 			return ctx.mkErr(k, "key must be of type int")
 		}
diff --git a/cue/export.go b/cue/export.go
index 5f3611f..f834300 100644
--- a/cue/export.go
+++ b/cue/export.go
@@ -33,7 +33,7 @@
 }
 
 func export(ctx *context, v value, m options) (n ast.Node, imports []string) {
-	e := exporter{ctx, m, nil, map[label]bool{}, map[string]importInfo{}}
+	e := exporter{ctx, m, nil, map[label]bool{}, map[string]importInfo{}, false}
 	top, ok := v.evalPartial(ctx).(*structLit)
 	if ok {
 		top, err := top.expandFields(ctx)
@@ -94,6 +94,7 @@
 	stack   []remap
 	top     map[label]bool        // label to alias or ""
 	imports map[string]importInfo // pkg path to info
+	inDef   bool                  // TODO(recclose):use count instead
 }
 
 type importInfo struct {
@@ -202,6 +203,30 @@
 	return short
 }
 
+func hasTemplate(s *ast.StructLit) bool {
+	for _, e := range s.Elts {
+		if f, ok := e.(*ast.Field); ok {
+			if _, ok := f.Label.(*ast.TemplateLabel); ok {
+				return true
+			}
+		}
+	}
+	return false
+}
+
+func (p *exporter) closeOrOpen(s *ast.StructLit, isClosed bool) ast.Expr {
+	if isClosed && !p.inDef {
+		return &ast.CallExpr{
+			Fun:  ast.NewIdent("close"),
+			Args: []ast.Expr{s},
+		}
+	}
+	if !isClosed && p.inDef && !hasTemplate(s) {
+		s.Elts = append(s.Elts, &ast.Ellipsis{})
+	}
+	return s
+}
+
 func (p *exporter) expr(v value) ast.Expr {
 	// TODO: use the raw expression for convert incomplete errors downstream
 	// as well.
@@ -210,7 +235,7 @@
 		x := p.ctx.manifest(e)
 		if isIncomplete(x) {
 			if isBottom(e) {
-				p = &exporter{p.ctx, options{raw: true}, p.stack, p.top, p.imports}
+				p = &exporter{p.ctx, options{raw: true}, p.stack, p.top, p.imports, p.inDef}
 				return p.expr(v)
 			}
 			v = e
@@ -318,6 +343,12 @@
 		return &ast.UnaryExpr{Op: opMap[x.op], X: p.expr(x.x)}
 
 	case *binaryExpr:
+		// opUnifyUnchecked: represented as embedding. The two arguments must
+		// be structs.
+		if x.op == opUnifyUnchecked {
+			s := &ast.StructLit{}
+			return p.closeOrOpen(s, p.embedding(s, x))
+		}
 		return &ast.BinaryExpr{
 			X:  p.expr(x.left),
 			Op: opMap[x.op], Y: p.expr(x.right),
@@ -358,10 +389,29 @@
 		return bin
 
 	case *structLit:
-		expr, err := p.structure(x)
+		st, err := p.structure(x, !x.isClosed)
 		if err != nil {
 			return p.expr(err)
 		}
+		expr := p.closeOrOpen(st, x.isClosed)
+		switch {
+		case x.isClosed && x.template != nil:
+			l, ok := x.template.evalPartial(p.ctx).(*lambdaExpr)
+			if !ok {
+				break
+			}
+			if _, ok := l.value.(*top); ok {
+				break
+			}
+			expr = &ast.BinaryExpr{X: expr, Op: token.AND, Y: &ast.StructLit{
+				Elts: []ast.Decl{&ast.Field{
+					Label: &ast.TemplateLabel{
+						Ident: p.identifier(l.params.arcs[0].feature),
+					},
+					Value: p.expr(l.value),
+				}},
+			}}
+		}
 		return expr
 
 	case *fieldComprehension:
@@ -520,7 +570,7 @@
 	}
 }
 
-func (p *exporter) structure(x *structLit) (ret *ast.StructLit, err *bottom) {
+func (p *exporter) structure(x *structLit, addTempl bool) (ret *ast.StructLit, err *bottom) {
 	obj := &ast.StructLit{}
 	if doEval(p.mode) {
 		x, err = x.expandFields(p.ctx)
@@ -539,9 +589,13 @@
 	if x.emit != nil {
 		obj.Elts = append(obj.Elts, &ast.EmbedDecl{Expr: p.expr(x.emit)})
 	}
-	if !doEval(p.mode) && x.template != nil {
+	switch {
+	case !doEval(p.mode) && x.template != nil && addTempl:
 		l, ok := x.template.evalPartial(p.ctx).(*lambdaExpr)
 		if ok {
+			if _, ok := l.value.(*top); ok && !x.isClosed {
+				break
+			}
 			obj.Elts = append(obj.Elts, &ast.Field{
 				Label: &ast.TemplateLabel{
 					Ident: p.identifier(l.params.arcs[0].feature),
@@ -566,20 +620,26 @@
 			}
 			f.Optional = token.NoSpace.Pos()
 		}
+		if a.definition {
+			f.Token = token.ISA
+		}
 		if a.feature&hidden != 0 && p.mode.concrete && p.mode.omitHidden {
 			continue
 		}
+		oldInDef := p.inDef
+		p.inDef = a.definition || p.inDef
 		if !doEval(p.mode) {
 			f.Value = p.expr(a.v)
 		} else {
 			e := x.at(p.ctx, i)
 			if v := p.ctx.manifest(e); isIncomplete(v) && !p.mode.concrete && isBottom(e) {
-				p := &exporter{p.ctx, options{raw: true}, p.stack, p.top, p.imports}
+				p := &exporter{p.ctx, options{raw: true}, p.stack, p.top, p.imports, p.inDef}
 				f.Value = p.expr(a.v)
 			} else {
 				f.Value = p.expr(e)
 			}
 		}
+		p.inDef = oldInDef
 		if a.attrs != nil && !p.mode.omitAttrs {
 			for _, at := range a.attrs.attr {
 				f.Attrs = append(f.Attrs, &ast.Attribute{Text: at.text})
@@ -624,6 +684,31 @@
 	return obj, nil
 }
 
+func (p *exporter) embedding(s *ast.StructLit, n value) (closed bool) {
+	switch x := n.(type) {
+	case *structLit:
+		st, err := p.structure(x, true)
+		if err != nil {
+			n = err
+			break
+		}
+		s.Elts = append(s.Elts, st.Elts...)
+		return x.isClosed
+
+	case *binaryExpr:
+		if x.op != opUnifyUnchecked {
+			// should not happen
+			s.Elts = append(s.Elts, &ast.EmbedDecl{Expr: p.expr(x)})
+			return false
+		}
+		leftClosed := p.embedding(s, x.left)
+		rightClosed := p.embedding(s, x.right)
+		return leftClosed || rightClosed
+	}
+	s.Elts = append(s.Elts, &ast.EmbedDecl{Expr: p.expr(n)})
+	return false
+}
+
 // quote quotes the given string.
 func quote(str string, quote byte) string {
 	if strings.IndexByte(str, '\n') < 0 {
diff --git a/cue/export_test.go b/cue/export_test.go
index ce87d91..760a135 100644
--- a/cue/export_test.go
+++ b/cue/export_test.go
@@ -70,6 +70,8 @@
 				f: string
 			}`),
 	}, {
+		// Here the failed lookups are not considered permanent
+		// failures, as the structs are open.
 		in: `{ a: { b: 2.0, s: "abc" }, b: a.b, c: a.c, d: a["d"], e: a.t[2:3] }`,
 		out: unindent(`
 			{
@@ -83,6 +85,45 @@
 				e: a.t[2:3]
 			}`),
 	}, {
+		// Here the failed lookups are permanent failures as the structs are
+		// closed.
+		in: `{ a :: { b: 2.0, s: "abc" }, b: a.b, c: a.c, d: a["d"], e: a.t[2:3] }`,
+		out: unindent(`
+			{
+				a :: {
+					b: 2.0
+					s: "abc"
+				}
+				b: 2.0
+				c: _|_ /* undefined field "c" */
+				d: _|_ /* undefined field "d" */
+				e: _|_ /* undefined field "t" */
+			}`),
+	}, {
+		// a closed struct with template restrictions is exported as a
+		// conjunction of two structs.
+		in: `{
+			A :: { b: int }
+			a: A & { <_>: <10 }
+			B :: a
+		}`,
+		out: unindent(`
+		{
+			A :: {
+				b: int
+			}
+			a: close({
+				b: <10
+			}) & {
+				<_>: <10
+			}
+			B :: {
+				b: <10
+			} & {
+				<_>: <10
+			}
+		}`),
+	}, {
 		in: `{
 			a: 5*[int]
 			a: [1, 2, ...]
@@ -298,6 +339,87 @@
 			}
 		}`),
 	}, {
+		raw: true,
+		in: `{
+			emb :: {
+				a: 1
+
+				sub: {
+					f: 3
+				}
+			}
+			def :: {
+				emb
+
+				b: 2
+			}
+			f :: { a: 10 }
+			e :: {
+				f
+
+				b: int
+				<_>: <100
+			}
+		}`,
+		out: unindent(`
+		{
+			emb :: {
+				a: 1
+				sub f: 3
+			}
+			f :: {
+				a: 10
+			}
+			def :: {
+				emb
+
+				b: 2
+			}
+			e :: {
+				f
+		
+				<_>: <100
+				b:   int
+			}
+		}`),
+	}, {
+		raw:  true,
+		eval: true,
+		in: `{
+				reg: { foo: 1, bar: { baz: 3 } }
+				def :: {
+					a: 1
+
+					sub: reg
+				}
+				val: def
+			}`,
+		out: unindent(`
+		{
+			reg: {
+				foo: 1
+				bar baz: 3
+			}
+			def :: {
+				a: 1
+				sub: {
+					foo: 1
+					bar: {
+						baz: 3
+						...
+					}
+					...
+				}
+			}
+			val: close({
+				a: 1
+				sub: {
+					foo: 1
+					bar baz: 3
+				}
+			})
+		}`),
+	}, {
 		raw:  true,
 		eval: true,
 		in: `{
diff --git a/cue/kind.go b/cue/kind.go
index 1eec58a..a2a7235 100644
--- a/cue/kind.go
+++ b/cue/kind.go
@@ -196,7 +196,7 @@
 				return k, true, ""
 			}
 			return bottomKind, false, msg
-		case opUnify:
+		case opUnify, opUnifyUnchecked:
 			if a&nullKind != 0 {
 				return k, false, ""
 			}
@@ -256,7 +256,7 @@
 	}
 	// a and b have overlapping types.
 	switch op {
-	case opUnify:
+	case opUnify, opUnifyUnchecked:
 		// Increase likelihood of unification succeeding on first try.
 		return u, swap, ""
 
diff --git a/cue/op.go b/cue/op.go
index e13f965..5706c2d 100644
--- a/cue/op.go
+++ b/cue/op.go
@@ -134,6 +134,9 @@
 }
 
 func (op op) unifyType() (unchecked, ok bool) {
+	if op == opUnifyUnchecked {
+		return true, true
+	}
 	return false, op == opUnify
 }
 
@@ -143,6 +146,7 @@
 	opUnknown op = iota
 
 	opUnify
+	opUnifyUnchecked
 	opDisjunction
 
 	opLand
@@ -174,8 +178,11 @@
 var opStrings = []string{
 	opUnknown: "??",
 
-	opUnify:       "&",
-	opDisjunction: "|",
+	opUnify: "&",
+	// opUnifyUnchecked is internal only. Syntactically this is
+	// represented as embedding.
+	opUnifyUnchecked: "&!",
+	opDisjunction:    "|",
 
 	opLand: "&&",
 	opLor:  "||",
diff --git a/cue/resolve_test.go b/cue/resolve_test.go
index f14e91d..736bbc3 100644
--- a/cue/resolve_test.go
+++ b/cue/resolve_test.go
@@ -549,8 +549,9 @@
 
 func TestResolve(t *testing.T) {
 	testCases := []testCase{{
-		in:  `a: { <_>: _ }`,
-		out: `<0>{a: <1>{<>: <2>(_: string)->_, }}`,
+		desc: "convert _ to top",
+		in:   `a: { <_>: _ }`,
+		out:  `<0>{a: <1>{...}}`,
 	}, {
 		in: `
 			a: b.c.d
@@ -611,7 +612,7 @@
 			`c: <3>{foo: 1 @bar() @baz(1) @foo()}, ` +
 			`e: _|_((<4>.a & <5>{foo: 1 @foo(other)}):conflicting attributes for key "foo")}`,
 	}, {
-		desc: "optional fields",
+		desc: "optional field unification",
 		in: `
 			a: { foo?: string }
 			b: { foo: "foo" }
@@ -629,6 +630,16 @@
 			`g1: 1, ` +
 			`g2?: 2}`,
 	}, {
+		desc: "optional field resolves to incomplete",
+		in: `
+		r: {
+			a?: 3
+			b: a
+			c: r["a"]
+		}
+	`,
+		out: `<0>{r: <1>{a?: 3, b: <2>.a, c: <2>["a"]}}`,
+	}, {
 		desc: "bounds",
 		in: `
 			i1: >1 & 5
@@ -1069,6 +1080,188 @@
 			`,
 		out: `<0>{a: <1>{c: 5, d: 15}, t: <2>{c: number, d: (<3>.c * 3)}, b: <4>{c: 7, d: 21}, ti: <5>{c: int, d: (<6>.c * 3)}}`,
 	}, {
+		desc: "definitions",
+		in: `
+			Foo :: {
+				field: int
+				recursive: {
+					field: string
+				}
+			}
+
+			Foo1 :: { field: int }
+			Foo1 :: { field2: string }
+
+			foo: Foo
+			foo: { feild: 2 }
+
+			foo1: Foo
+			foo1: {
+				field: 2
+				recursive: {
+					feild: 2 // Not caught as per spec. TODO: change?
+				}
+			}
+
+			Bar :: {
+				field: int
+				<A>:   int
+			}
+			bar: Bar
+			bar: { feild: 2 }
+
+			Mixed :: string
+			Mixed: string
+
+			mixedRec: { Mixed :: string }
+			mixedRec: { Mixed: string }
+			`,
+		out: `<0>{` +
+			`Foo :: <1>C{field: int, recursive: <2>C{field: string}}, ` +
+			`Foo1 :: _|_((<3>C{field: int} & <4>C{field2: string}):field "field" not allowed in closed struct), ` +
+			`foo: _|_(2:field "feild" not allowed in closed struct), ` +
+			`foo1: <5>C{field: 2, recursive: _|_(2:field "feild" not allowed in closed struct)}, ` +
+			`Bar :: <6>{<>: <7>(A: string)->int, field: int}, ` +
+			`bar: <8>{<>: <9>(A: string)->int, field: int, feild: 2}, ` +
+			`Mixed: _|_(field "Mixed" declared as definition and regular field), ` +
+			`mixedRec: _|_(field "Mixed" declared as definition and regular field)}`,
+	}, {
+		desc: "definitions with oneofs",
+		in: `
+			Foo :: {
+				field: int
+
+				{ a: 1 } |
+				{ b: 2 }
+			}
+
+			foo: Foo
+			foo: { a: 2 }
+
+			bar: Foo
+			bar: { c: 2 }
+
+			baz: Foo
+			baz: { b: 2 }
+			`,
+		out: `<0>{` +
+			`Foo :: (<1>C{field: int, a: 1} | <2>C{field: int, b: 2}), ` +
+			`foo: _|_((<3>.Foo & <4>{a: 2}):empty disjunction: C{field: int, a: (1 & 2)}), ` +
+			`bar: _|_((<3>.Foo & <5>{c: 2}):empty disjunction: field "c" not allowed in closed struct), ` +
+			`baz: <6>C{field: int, b: 2}}`,
+	}, {
+		desc: "definitions with embedding",
+		in: `
+		E :: {
+			a: { b: int }
+		}
+
+		S :: {
+			E
+			a: { c: int }
+			b: 3
+		}
+
+		// error: literal struct is closed before unify
+		e1 :: S & { a c: 4 }
+		// no such issue here
+		v1: S & { a c: 4 }
+
+		// adding a field to a nested struct that is closed.
+		e2: S & { a d: 4 }
+		`,
+		out: `<0>{` +
+			`E :: <1>C{a: <2>C{b: int}}, ` +
+			`S :: <3>C{a: _|_((<4>C{b: int} & <5>C{c: int}):field "b" not allowed in closed struct), b: 3}, ` +
+			`e1 :: _|_((<6>.S & <7>C{a: <8>C{c: 4}}):field "b" not allowed in closed struct), ` +
+			`v1: <9>C{a: _|_((<10>C{b: int} & <11>C{c: int}):field "b" not allowed in closed struct), b: 3}, ` +
+			`e2: <12>C{a: _|_((<13>C{b: int} & <14>C{c: int}):field "b" not allowed in closed struct), b: 3}}`,
+	}, {
+		desc: "closing structs",
+		in: `
+		op: {x: int}             // {x: int}
+		ot: {x: int, ...}        // {x: int, ...}
+		cp: close({x: int})      // closed({x: int})
+		ct: close({x: int, ...}) // {x: int, ...}
+
+		opot: op & ot  // {x: int, ...}
+		otop: ot & op  // {x: int, ...}
+		opcp: op & cp  // closed({x: int})
+		cpop: cp & op  // closed({x: int})
+		opct: op & ct  // {x: int, ...}
+		ctop: ct & op  // {x: int, ...}
+		otcp: ot & cp  // closed({x: int})
+		cpot: cp & ot  // closed({x: int})
+		otct: ot & ct  // {x: int, ...}
+		ctot: ct & ot  // {x: int, ...}
+		cpct: cp & ct  // closed({x: int})
+		ctcp: ct & cp  // closed({x: int})
+		ctct: ct & ct  // {x: int, ...}
+		`,
+		out: `<0>{` +
+			`op: <1>{x: int}, ` +
+			`ot: <2>{x: int, ...}, ` +
+			`cp: <3>C{x: int}, ` +
+			`ct: <4>{x: int, ...}, ` +
+			`opot: <5>{x: int, ...}, ` +
+			`otop: <6>{x: int, ...}, ` +
+			`opcp: <7>C{x: int}, ` +
+			`cpop: <8>C{x: int}, ` +
+			`opct: <9>{x: int, ...}, ` +
+			`ctop: <10>{x: int, ...}, ` +
+			`otcp: <11>C{x: int}, ` +
+			`cpot: <12>C{x: int}, ` +
+			`otct: <13>{x: int, ...}, ` +
+			`ctot: <14>{x: int, ...}, ` +
+			`cpct: <15>C{x: int}, ` +
+			`ctcp: <16>C{x: int}, ` +
+			`ctct: <17>{x: int, ...}}`,
+	}, {
+		desc: "closing with failed optional",
+		in: `
+		k1 :: {a: int, b?: int} & {a: int} // closed({a: int})
+		k2 :: {a: int} & {a: int, b?: int} // closed({a: int})
+
+		o1: {a?: 3} & {a?: 4} // {a?: _|_}
+
+		// Optional fields with error values can be elimintated when closing
+		o2 :: {a?: 3} & {a?: 4} // close({})
+
+		d1 :: {a?: 2, b: 4} | {a?: 3, c: 5}
+		v1: d1 & {a?: 3, b: 4}  // close({b: 4})
+		`,
+		out: `<0>{` +
+			`k1 :: <1>C{a: int}, ` +
+			`k2 :: <2>C{a: int}, ` +
+			`o1: <3>{a?: _|_((3 & 4):conflicting values 3 and 4)}, ` +
+			`o2 :: <4>C{a?: _|_((3 & 4):conflicting values 3 and 4)}, ` +
+			`d1 :: (<5>C{a?: 2, b: 4} | <6>C{a?: 3, c: 5}), ` +
+			`v1: <7>C{a?: _|_((2 & 3):conflicting values 2 and 3), b: 4}}`,
+	}, {
+		desc: "closing with comprehensions",
+		in: `
+		A :: {f1: int, f2: int}
+
+		// Comprehension fields cannot be added like any other.
+		a: A & { "\(k)": v for k, v in {f3 : int}}
+
+		// A closed struct may not generate comprehension values it does not
+		// define explicitly.
+		B :: {"\(k)": v for k, v in {f1: int}}
+
+		// To fix this, add all allowed fields.
+		C :: {f1: _, "\(k)": v for k, v in {f1: int}}
+
+		// Or like this.
+		D :: {"\(k)": v for k, v in {f1: int}, ...}
+		`,
+		out: `<0>{` +
+			`A :: <1>C{f1: int, f2: int}, ` +
+			`a: _|_(int:field "f3" not allowed in closed struct), ` +
+			`B :: _|_(int:field "f1" not allowed in closed struct), ` +
+			`C :: <2>C{f1: int}, ` +
+			`D :: <3>{f1: int, ...}}`,
+	}, {
 		desc: "reference to root",
 		in: `
 			a: { b: int }
@@ -1564,6 +1757,15 @@
 				a: 7080 | int`,
 		out: `<0>{a: _|_((8000.9 & (int | int)):conflicting values 8000.9 and int (mismatched types float and int))}`, // TODO: fix repetition
 	}, {
+		desc: "conflicts in optional fields are okay ",
+		in: `
+			d: {a: 1, b?: 3} | {a: 2}
+
+			// the following conjunction should not eliminate any disjuncts
+			c: d & {b?:4}
+		`,
+		out: `<0>{d: (<1>{a: 1, b?: 3} | <2>{a: 2}), c: (<3>{a: 1, b?: (3 & 4)} | <4>{a: 2, b?: 4})}`,
+	}, {
 		desc: "resolve all disjunctions",
 		in: `
 			service <Name>: {
@@ -1622,8 +1824,12 @@
 				a: 3
 				a: 3 if a > 1
 			}
+			d: {
+				a: int
+				a: 3 if a > 1
+			}
 		`,
-		out: `<0>{b: true, c: <1>{a: 3}, a: "foo"}`,
+		out: `<0>{b: true, c: <1>{a: 3}, a: "foo", d: <2>{a: int if (<2>.a > 1) yield ("a"): 3}}`,
 	}, {
 		desc: "referencing field in field comprehension",
 		in: `
diff --git a/cue/rewrite.go b/cue/rewrite.go
index c135a15..06171e0 100644
--- a/cue/rewrite.go
+++ b/cue/rewrite.go
@@ -237,7 +237,7 @@
 	if key == x.key && value == x.value {
 		return x
 	}
-	return &yield{x.baseValue, x.opt, key, value}
+	return &yield{x.baseValue, x.opt, x.def, key, value}
 }
 
 func (x *guard) rewrite(ctx *context, fn rewriteFunc) value {
diff --git a/cue/rewrite_test.go b/cue/rewrite_test.go
index 4a6acc5..b9738c1 100644
--- a/cue/rewrite_test.go
+++ b/cue/rewrite_test.go
@@ -75,7 +75,7 @@
 			t = v
 		}
 		emit := testResolve(ctx, x.emit, m)
-		obj := &structLit{x.baseValue, emit, t, nil, arcs, nil}
+		obj := &structLit{x.baseValue, emit, t, x.isClosed, nil, arcs, nil}
 		return obj
 	case *list:
 		elm := rewriteRec(ctx, x.elem, x.elem, m).(*structLit)
diff --git a/cue/types.go b/cue/types.go
index c95af87..dddef8e 100644
--- a/cue/types.go
+++ b/cue/types.go
@@ -1078,12 +1078,13 @@
 		}
 		arcs = arcs[:k]
 		obj = &structLit{
-			obj.baseValue,
-			obj.emit,
-			obj.template,
-			nil,
-			arcs,
-			nil,
+			obj.baseValue, // baseValue
+			obj.emit,      // emit
+			obj.template,  // template
+			obj.isClosed,  // isClosed
+			nil,           // comprehensions
+			arcs,          // arcs
+			nil,           // attributes
 		}
 	}
 	return structValue{ctx, v.path, obj}, nil
diff --git a/cue/value.go b/cue/value.go
index 8d58770..ed49e71 100644
--- a/cue/value.go
+++ b/cue/value.go
@@ -624,8 +624,24 @@
 	baseValue
 
 	// TODO(perf): separate out these infrequent values to save space.
-	emit           value // currently only supported at top level.
-	template       value
+	emit value // currently only supported at top level.
+	// TODO: make this a list of templates and don't unify until templates are
+	// applied. This allows generalization of having different constraints
+	// for different field sets. This could also be used to mark closedness:
+	// use [string]: _ for fully open. This could be a sentinel value.
+	// For now we use a boolean for closedness.
+
+	// NOTE: must be conjunction of lists.
+	// For lists originating from closed structs,
+	// there must be at least one match.
+	// templates [][]value
+	// catch_all: value
+
+	// template must evaluated to a lambda and is applied to all concrete
+	// values in the struct, whether it be open or closed.
+	template value
+	isClosed bool
+
 	comprehensions []*fieldComprehension
 
 	// TODO: consider hoisting the template arc to its own value.
@@ -633,6 +649,18 @@
 	expanded evaluated
 }
 
+func (x *structLit) addTemplate(ctx *context, pos token.Pos, t value) {
+	if x.template == nil {
+		x.template = t
+	} else {
+		x.template = mkBin(ctx, pos, opUnify, x.template, t)
+	}
+}
+
+func (x *structLit) allows(f label) bool {
+	return !x.isClosed
+}
+
 func newStruct(src source) *structLit {
 	return &structLit{baseValue: src.base()}
 }
@@ -645,6 +673,16 @@
 func (x *structLit) Less(i, j int) bool { return x.arcs[i].feature < x.arcs[j].feature }
 func (x *structLit) Swap(i, j int)      { x.arcs[i], x.arcs[j] = x.arcs[j], x.arcs[i] }
 
+func (x *structLit) close() *structLit {
+	if x.template != nil {
+		return x // there is nothing to close as it is already fully defined.
+	}
+
+	newS := *x
+	newS.isClosed = true
+	return &newS
+}
+
 // lookup returns the node for the given label f, if present, or nil otherwise.
 func (x *structLit) lookup(ctx *context, f label) arc {
 	x, err := x.expandFields(ctx)
@@ -674,11 +712,22 @@
 }
 
 func (x *structLit) at(ctx *context, i int) evaluated {
+	// TODO: limit visibility of definitions:
+	// Approach:
+	// - add package identifier to arc (label)
+	// - assume ctx is unique for a package
+	// - record package identifier in context
+	// - if arc is a definition, check IsExported and verify the package if not.
+	//
+	// The same approach could be valid for looking up package-level identifiers.
+	// - detect somehow aht root nodes are.
+	//
+	// Allow import of CUE files. These cannot have a package clause.
+
 	x, err := x.expandFields(ctx)
 	if err != nil {
 		return err
 	}
-
 	// if x.emit != nil && isBottom(x.emit) {
 	// 	return x.emit.(evaluated)
 	// }
@@ -755,7 +804,7 @@
 	newArcs := []arc{}
 
 	for _, c := range comprehensions {
-		result := c.clauses.yield(ctx, func(k, v evaluated, opt bool) *bottom {
+		result := c.clauses.yield(ctx, func(k, v evaluated, opt, def bool) *bottom {
 			if !k.kind().isAnyOf(stringKind) {
 				return ctx.mkErr(k, "key must be of type string")
 			}
@@ -777,9 +826,10 @@
 				}
 			}
 			newArcs = append(newArcs, arc{
-				feature:  f,
-				optional: opt,
-				v:        v,
+				feature:    f,
+				optional:   opt,
+				definition: def,
+				v:          v,
 			})
 			return nil
 		})
@@ -803,6 +853,7 @@
 		x.baseValue, // baseValue
 		emit,        // emit
 		template,    // template
+		false,       // isClosed
 		nil,         // comprehensions
 		newArcs,     // arcs
 		nil,         // attributes
@@ -843,8 +894,10 @@
 // however, may have both. In this case, the value must ultimately evaluate
 // to a node, which will then be merged with the existing one.
 type arc struct {
-	feature  label
-	optional bool
+	feature    label
+	optional   bool
+	definition bool // field is a definition
+
 	// TODO: add index to preserve approximate order within a struct and use
 	// topological sort to compute new struct order when unifying. This could
 	// also be achieved by not sorting labels on features and doing
@@ -905,19 +958,27 @@
 }
 
 // insertValue is used during initialization but never during evaluation.
-func (x *structLit) insertValue(ctx *context, f label, optional bool, value value, a *attributes, docs *docNode) {
+func (x *structLit) insertValue(ctx *context, f label, optional, isDef bool, value value, a *attributes, docs *docNode) {
 	for i, p := range x.arcs {
 		if f != p.feature {
 			continue
 		}
-		x.arcs[i].v = mkBin(ctx, token.NoPos, opUnify, p.v, value)
-		// TODO: should we warn if there is a mixed mode of optional and non
-		// optional fields at this point?
 		x.arcs[i].optional = x.arcs[i].optional && optional
 		x.arcs[i].docs = mergeDocs(x.arcs[i].docs, docs)
+		x.arcs[i].v = mkBin(ctx, token.NoPos, opUnify, p.v, value)
+		if isDef != p.definition {
+			src := binSrc(token.NoPos, opUnify, p.v, value)
+			x.arcs[i].v = ctx.mkErr(src,
+				"field %q declared as definition and regular field",
+				ctx.labelStr(f))
+			isDef = false
+		}
+		x.arcs[i].definition = isDef
+		// TODO: should we warn if there is a mixed mode of optional and non
+		// optional fields at this point?
 		return
 	}
-	x.arcs = append(x.arcs, arc{f, optional, value, nil, a, docs})
+	x.arcs = append(x.arcs, arc{f, optional, isDef, value, nil, a, docs})
 	sort.Stable(x)
 }
 
@@ -1322,7 +1383,7 @@
 	return topKind | nonGround
 }
 
-type yieldFunc func(k, v evaluated, optional bool) *bottom
+type yieldFunc func(k, v evaluated, optional, definition bool) *bottom
 
 type yielder interface {
 	value
@@ -1332,6 +1393,7 @@
 type yield struct {
 	baseValue
 	opt   bool
+	def   bool
 	key   value
 	value value
 }
@@ -1352,7 +1414,7 @@
 	if isBottom(v) {
 		return v
 	}
-	if err := fn(k, v, x.opt); err != nil {
+	if err := fn(k, v, x.opt, x.def); err != nil {
 		return err
 	}
 	return nil
diff --git a/doc/ref/spec.md b/doc/ref/spec.md
index eb53b34..48393ff 100644
--- a/doc/ref/spec.md
+++ b/doc/ref/spec.md
@@ -976,6 +976,22 @@
 in their respective field values need to be replaced with references to `c`.
 The result of a unification is bottom (`_|_`) if any of its required
 fields evaluates to bottom, recursively.
+<!--NOTE: About bottom values for optional fields being okay.
+
+The proposition ¬P is a close cousin of P → ⊥ and is often used
+as an approximation to avoid the issues of using not.
+Bottom (⊥) is also frequently used to mean undefined. This makes sense.
+Consider `{a?: 2} & {a?: 3}`.
+Both structs say `a` is optional; in other words, it may be omitted.
+So we can still get a valid result by omitting `a`, even in
+case of a conflict.
+
+Granted, this definition may lead to confusing results, especially in
+definitions, when tightening an optional field leads to unintentionally
+discarding it.
+It could be a role of vet checkers to identify such cases (and suggest users
+to explicitly use `_|_` to discard a field, for instance).
+-->
 
 Syntactically, the labels of optional fields are followed by a
 question mark `?`.
@@ -998,6 +1014,8 @@
 labels match the expression.
 -->
 A Bind label binds an identifier to the label name scoped to the field value.
+It also makes all possible labels an optional field set to the
+associated field value.
 The token `...` is a shorthand for `<_>: _`.
 <!-- NOTE: if we allow ...Expr, as in list, it would mean something different. -->
 
@@ -1103,12 +1121,11 @@
 #### Closed structs
 
 By default, structs are open to adding fields.
-One could say that an optional field `f` with value top (`_`) is defined for any
-unspecified field.
+Instances of an open struct `p` may contain fields not defined in `p`.
 A _closed struct_ `c` is a struct whose instances may not have fields
 not defined in `c`.
 Closing a struct is equivalent to adding an optional field with value `_|_`
-for any undefined field.
+for all undefined fields.
 
 Note that fields created with field comprehensions are not considered
 defined fields.
@@ -1150,9 +1167,19 @@
 #### Embedding
 
 A struct may contain an _embedded value_, an Operand used
-as a field declaration.
+as a declaration, which must evaluate to a struct.
+An embedded value of type struct is unified with the struct in which it is
+embedded, but disregarding the restrictions imposed by closed structs
+for its top-level fields.
+<!--TODO: consider relaxing it to the below.
 An embedded value of type struct is unified with the struct in which it is
 embedded, but disregarding the restrictions imposed by closed structs.
+
+Note that in the above definition we cannot say that the fields of the
+embedded struct are added: references within these fields referring to
+the embedded struct should be rewired to reference the new struct.
+This would not be the case with  per-field definition.
+-->
 A struct resulting from such a unification is closed if either of the involved
 structs were closed.
 
@@ -1166,7 +1193,8 @@
 It is illegal to have a normal field and a definition with the same name
 within the same struct.
 Literal structs that are part of a definition's value are implicitly closed.
-An ellipsis `...` in such literal structs keeps them open.
+An ellipsis `...` in such literal structs keeps them open,
+as it defines `_` for all labels.
 
 
 ```