diff --git a/internal/core/adt/composite.go b/internal/core/adt/composite.go
index 3246c5d..d7c51ca 100644
--- a/internal/core/adt/composite.go
+++ b/internal/core/adt/composite.go
@@ -74,6 +74,11 @@
 	// status indicates the evaluation progress of this vertex.
 	status VertexStatus
 
+	// isData indicates that this Vertex is to be interepreted as data: pattern
+	// and additional constraints, as well as optional fields, should be
+	// ignored.
+	isData bool
+
 	// Value is the value associated with this vertex. For lists and structs
 	// this is a sentinel value indicating its kind.
 	Value Value
@@ -148,6 +153,39 @@
 	v.status = s
 }
 
+// IsData reports whether v should be interpreted in data mode. In other words,
+// it tells whether optional field matching and non-regular fields, like
+// definitions and hidden fields, should be ignored.
+func (v *Vertex) IsData() bool {
+	return v.isData || len(v.Conjuncts) == 0
+}
+
+// ToDataSingle creates a new Vertex that represents just the regular fields
+// of this vertex. Arcs are left untouched.
+// It is used by cue.Eval to convert nodes to data on per-node basis.
+func (v *Vertex) ToDataSingle() *Vertex {
+	w := *v
+	w.isData = true
+	return &w
+}
+
+// ToDataAll returns a new v where v and all its descendents contain only
+// the regular fields.
+func (v *Vertex) ToDataAll() *Vertex {
+	arcs := make([]*Vertex, len(v.Arcs))
+	for i, a := range v.Arcs {
+		arcs[i] = a.ToDataAll()
+	}
+	w := *v
+	w.Arcs = arcs
+	w.isData = true
+	return &w
+}
+
+// func (v *Vertex) IsEvaluating() bool {
+// 	return v.Value == cycle
+// }
+
 func (v *Vertex) IsErr() bool {
 	// if v.Status() > Evaluating {
 	if _, ok := v.Value.(*Bottom); ok {
@@ -228,8 +266,23 @@
 	// constraints, and additional constraints that match f and inserts them in
 	// arc. Use f is 0 to match all additional constraints only.
 	MatchAndInsert(c *OpContext, arc *Vertex)
+
+	// OptionalTypes returns a bit field with the type of optional constraints
+	// that are represented by this Acceptor.
+	OptionalTypes() OptionalType
 }
 
+// OptionalType is a bit field of the type of optional constraints in use by an
+// Acceptor.
+type OptionalType int
+
+const (
+	HasField OptionalType = 1 << iota
+	HasPattern
+	HasAdditional
+	IsOpen
+)
+
 func (v *Vertex) Kind() Kind {
 	// This is possible when evaluating comprehensions. It is potentially
 	// not known at this time what the type is.
@@ -239,6 +292,17 @@
 	return v.Value.Kind()
 }
 
+func (v *Vertex) OptionalTypes() OptionalType {
+	switch {
+	case v.Closed != nil:
+		return v.Closed.OptionalTypes()
+	case v.IsList():
+		return 0
+	default:
+		return IsOpen
+	}
+}
+
 func (v *Vertex) IsClosed(ctx *OpContext) bool {
 	switch x := v.Value.(type) {
 	case *ListMarker:
diff --git a/internal/core/debug/compact.go b/internal/core/debug/compact.go
index 722a480..b40ada5 100644
--- a/internal/core/debug/compact.go
+++ b/internal/core/debug/compact.go
@@ -34,7 +34,7 @@
 func (w *compactPrinter) node(n adt.Node) {
 	switch x := n.(type) {
 	case *adt.Vertex:
-		if x.Value == nil || (w.cfg.Raw && len(x.Conjuncts) > 0) {
+		if x.Value == nil || (w.cfg.Raw && !x.IsData()) {
 			for i, c := range x.Conjuncts {
 				if i > 0 {
 					w.string(" & ")
diff --git a/internal/core/eval/closed.go b/internal/core/eval/closed.go
index 10cee11..c909b43 100644
--- a/internal/core/eval/closed.go
+++ b/internal/core/eval/closed.go
@@ -97,6 +97,13 @@
 	}
 }
 
+func (a *acceptor) OptionalTypes() (mask adt.OptionalType) {
+	for _, f := range a.fields {
+		mask |= f.OptionalTypes()
+	}
+	return mask
+}
+
 // CloseDef defines how individual FieldSets (corresponding to conjuncts)
 // combine to determine whether a field is contained in a closed set.
 //
diff --git a/internal/core/eval/optionals.go b/internal/core/eval/optionals.go
index 1dbd376..8d77a57 100644
--- a/internal/core/eval/optionals.go
+++ b/internal/core/eval/optionals.go
@@ -37,6 +37,25 @@
 	isOpen     bool // has a ...
 }
 
+func (o *fieldSet) OptionalTypes() (mask adt.OptionalType) {
+	for _, f := range o.fields {
+		if len(f.optional) > 0 {
+			mask = adt.HasField
+			break
+		}
+	}
+	if o.bulk != nil {
+		mask |= adt.HasPattern
+	}
+	if o.additional != nil {
+		mask |= adt.HasAdditional
+	}
+	if o.isOpen {
+		mask |= adt.IsOpen
+	}
+	return mask
+}
+
 type field struct {
 	label    adt.Feature
 	optional []adt.Node
diff --git a/internal/core/subsume/structural.go b/internal/core/subsume/structural.go
new file mode 100644
index 0000000..16e7a0e
--- /dev/null
+++ b/internal/core/subsume/structural.go
@@ -0,0 +1,281 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+// TODO: structural subsumption has not yet been implemented.
+
+import "cuelang.org/go/internal/core/adt"
+
+func (s *subsumer) subsumes(gt, lt adt.Conjunct) bool {
+	if gt == lt {
+		return true
+	}
+
+	// First try evaluating at the value level.
+	x, _ := gt.Expr().(adt.Value)
+	y, _ := lt.Expr().(adt.Value)
+	if x == nil {
+		// Fall back to structural.
+		return s.structural(gt, lt)
+	}
+	if y == nil {
+		return false
+	}
+
+	return s.values(x, y)
+}
+
+func (s *subsumer) conjunct(gt, lt adt.Conjunct) bool {
+	return false
+}
+
+func (s *subsumer) c(env *adt.Environment, x adt.Expr) adt.Conjunct {
+	return adt.MakeConjunct(env, x)
+}
+
+func isBottomConjunct(c adt.Conjunct) bool {
+	b, _ := c.Expr().(*adt.Bottom)
+	return b != nil
+}
+
+func (s *subsumer) node(env *adt.Environment, up int32) *adt.Vertex {
+	for ; up != 0; up-- {
+		env = env.Up
+	}
+	return env.Vertex
+}
+
+func (s *subsumer) structural(a, b adt.Conjunct) bool {
+	if y, ok := b.Expr().(*adt.LetReference); ok {
+		return s.conjunct(a, s.c(b.Env, y.X))
+	}
+	if isBottomConjunct(b) {
+		return true
+	}
+
+	switch x := a.Expr().(type) {
+	case *adt.DisjunctionExpr:
+
+	case *adt.StructLit:
+	case *adt.ListLit:
+
+	case *adt.FieldReference:
+		if y, ok := b.Expr().(*adt.FieldReference); ok && x.Label == y.Label {
+			if s.node(a.Env, x.UpCount) == s.node(b.Env, y.UpCount) {
+				return true
+			}
+		}
+
+	case *adt.LabelReference:
+		if y, ok := b.Expr().(*adt.LabelReference); ok {
+			if s.node(a.Env, x.UpCount) == s.node(b.Env, y.UpCount) {
+				return true
+			}
+		}
+
+	case *adt.DynamicReference:
+		if y, ok := b.Expr().(*adt.FieldReference); ok {
+			if s.node(a.Env, x.UpCount) == s.node(b.Env, y.UpCount) {
+				return true
+			}
+		}
+
+	case *adt.ImportReference:
+		if y, ok := b.Expr().(*adt.ImportReference); ok &&
+			x.ImportPath == y.ImportPath {
+			return true
+		}
+
+	case *adt.LetReference:
+		return s.conjunct(s.c(a.Env, x.X), b)
+
+	case *adt.SelectorExpr:
+		if y, ok := a.Expr().(*adt.SelectorExpr); ok &&
+			x.Sel == y.Sel &&
+			s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X)) {
+			return true
+		}
+
+	case *adt.IndexExpr:
+		if y, ok := b.Expr().(*adt.IndexExpr); ok &&
+			s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X)) &&
+			s.conjunct(s.c(a.Env, x.Index), s.c(b.Env, y.Index)) {
+			return true
+		}
+
+	case *adt.SliceExpr:
+		if r, ok := b.Expr().(*adt.SliceExpr); ok &&
+			s.conjunct(s.c(a.Env, x.X), s.c(b.Env, r.X)) &&
+			s.conjunct(s.c(a.Env, x.Lo), s.c(b.Env, r.Lo)) &&
+			s.conjunct(s.c(a.Env, x.Hi), s.c(b.Env, r.Hi)) {
+			return true
+		}
+
+	case *adt.Interpolation:
+		switch y := b.Expr().(type) {
+		case *adt.String:
+			// Be conservative if not ground.
+			s.inexact = true
+
+		case *adt.Interpolation:
+			// structural equivalence
+			if len(x.Parts) != len(y.Parts) {
+				return false
+			}
+			for i, p := range x.Parts {
+				if !s.conjunct(s.c(a.Env, p), s.c(b.Env, y.Parts[i])) {
+					return false
+				}
+			}
+			return true
+		}
+
+	case *adt.BoundExpr:
+		if y, ok := b.Expr().(*adt.BoundExpr); ok && x.Op == y.Op {
+			return s.conjunct(s.c(a.Env, x.Expr), s.c(b.Env, y.Expr))
+		}
+
+	case *adt.UnaryExpr:
+		if y, ok := b.Expr().(*adt.UnaryExpr); ok && x.Op == y.Op {
+			return s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X))
+		}
+
+	case *adt.BinaryExpr:
+		if y, ok := b.Expr().(*adt.BinaryExpr); ok && x.Op == y.Op {
+			return s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X)) &&
+				s.conjunct(s.c(a.Env, x.Y), s.c(b.Env, y.Y))
+		}
+
+	case *adt.CallExpr:
+		if y, ok := b.Expr().(*adt.CallExpr); ok {
+			if len(x.Args) != len(y.Args) {
+				return false
+			}
+			for i, arg := range x.Args {
+				if !s.conjunct(s.c(a.Env, arg), s.c(b.Env, y.Args[i])) {
+					return false
+				}
+			}
+			return s.conjunct(s.c(a.Env, x.Fun), s.c(b.Env, y.Fun))
+		}
+	}
+	return false
+}
+
+func (s *subsumer) structLit(
+	ea *adt.Environment, sa *adt.StructLit,
+	eb *adt.Environment, sb *adt.StructLit) bool {
+
+	// Create index of instance fields.
+	ca := newCollatedDecls()
+	ca.collate(ea, sa)
+
+	if ca.yielders != nil || ca.dynamic != nil {
+		// TODO: we could do structural comparison of comprehensions
+		// in many cases. For instance, an if clause would subsume
+		// structurally if it subsumes any of the if clauses in sb.
+		s.inexact = true
+		return false
+	}
+
+	cb := newCollatedDecls()
+	cb.collate(eb, sb)
+
+	if ca.hasOptional && !s.IgnoreOptional {
+		// TODO: same argument here as for comprehensions. This could
+		// be made to work.
+		if ca.pattern != nil || ca.dynamic != nil {
+			s.inexact = true
+			return false
+		}
+
+		// for f, b := range cb.fields {
+		// 	if !b.required || f.IsDef() {
+		// 		continue
+		// 	}
+		// 	name := ctx.LabelStr(b.Label)
+		// 	arg := &stringLit{x.baseValue, name, nil}
+		// 	u, _ := x.optionals.constraint(ctx, arg)
+		// 	if u != nil && !s.subsumes(u, b.v) {
+		// 		return false
+		// 	}
+		// }
+
+	}
+
+	return false
+
+}
+
+// collatedDecls is used to compute the structural subsumption of two
+// struct literals.
+type collatedDecls struct {
+	fields      map[adt.Feature]field
+	yielders    []adt.Yielder
+	pattern     []*adt.BulkOptionalField
+	dynamic     []*adt.DynamicField
+	values      []adt.Expr
+	additional  []*adt.Ellipsis
+	isOpen      bool
+	hasOptional bool
+}
+
+func newCollatedDecls() *collatedDecls {
+	return &collatedDecls{fields: map[adt.Feature]field{}}
+}
+
+type field struct {
+	required  bool
+	conjuncts []adt.Conjunct
+}
+
+func (c *collatedDecls) collate(env *adt.Environment, s *adt.StructLit) {
+	for _, d := range s.Decls {
+		switch x := d.(type) {
+		case *adt.Field:
+			e := c.fields[x.Label]
+			e.required = true
+			e.conjuncts = append(e.conjuncts, adt.MakeConjunct(env, x))
+			c.fields[x.Label] = e
+
+		case *adt.OptionalField:
+			e := c.fields[x.Label]
+			e.conjuncts = append(e.conjuncts, adt.MakeConjunct(env, x))
+			c.fields[x.Label] = e
+			c.hasOptional = true
+
+		case *adt.BulkOptionalField:
+			c.pattern = append(c.pattern, x)
+			c.hasOptional = true
+
+		case *adt.DynamicField:
+			c.dynamic = append(c.dynamic, x)
+			c.hasOptional = true
+
+		case *adt.Ellipsis:
+			c.isOpen = true
+			c.additional = append(c.additional, x)
+
+		case *adt.ForClause:
+			c.yielders = append(c.yielders, x)
+
+		case *adt.IfClause:
+			c.yielders = append(c.yielders, x)
+
+		case *adt.LetClause:
+		case *adt.ValueClause:
+		}
+	}
+}
diff --git a/internal/core/subsume/structural_test.go b/internal/core/subsume/structural_test.go
new file mode 100644
index 0000000..b22ded7
--- /dev/null
+++ b/internal/core/subsume/structural_test.go
@@ -0,0 +1,495 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+	"regexp"
+	"strconv"
+	"strings"
+	"testing"
+
+	"cuelang.org/go/cue/parser"
+	"cuelang.org/go/internal/core/adt"
+	"cuelang.org/go/internal/core/compile"
+	"cuelang.org/go/internal/core/eval"
+	"cuelang.org/go/internal/core/runtime"
+)
+
+func TestStructural(t *testing.T) {
+	// TODO: all these tests should pass for structural subsumption.
+	t.Skip()
+
+	// Do not inline: the named struct is used as a marker in
+	// testdata/gen.go.
+	type subsumeTest struct {
+		// the result of b ⊑ a, where a and b are defined in "in"
+		subsumes bool
+		in       string
+		// mode     subsumeMode
+	}
+	testCases := []subsumeTest{
+		// Top subsumes everything
+		0: {subsumes: true, in: `a: _, b: _ `},
+		1: {subsumes: true, in: `a: _, b: null `},
+		2: {subsumes: true, in: `a: _, b: int `},
+		3: {subsumes: true, in: `a: _, b: 1 `},
+		4: {subsumes: true, in: `a: _, b: float `},
+		5: {subsumes: true, in: `a: _, b: "s" `},
+		6: {subsumes: true, in: `a: _, b: {} `},
+		7: {subsumes: true, in: `a: _, b: []`},
+		8: {subsumes: true, in: `a: _, b: _|_ `},
+
+		// Nothing besides top subsumed top
+		9:  {subsumes: false, in: `a: null,    b: _`},
+		10: {subsumes: false, in: `a: int, b: _`},
+		11: {subsumes: false, in: `a: 1,       b: _`},
+		12: {subsumes: false, in: `a: float, b: _`},
+		13: {subsumes: false, in: `a: "s",     b: _`},
+		14: {subsumes: false, in: `a: {},      b: _`},
+		15: {subsumes: false, in: `a: [],      b: _`},
+		16: {subsumes: false, in: `a: _|_ ,      b: _`},
+
+		// Bottom subsumes nothing except bottom itself.
+		17: {subsumes: false, in: `a: _|_, b: null `},
+		18: {subsumes: false, in: `a: _|_, b: int `},
+		19: {subsumes: false, in: `a: _|_, b: 1 `},
+		20: {subsumes: false, in: `a: _|_, b: float `},
+		21: {subsumes: false, in: `a: _|_, b: "s" `},
+		22: {subsumes: false, in: `a: _|_, b: {} `},
+		23: {subsumes: false, in: `a: _|_, b: [] `},
+		24: {subsumes: true, in: ` a: _|_, b: _|_ `},
+
+		// All values subsume bottom
+		25: {subsumes: true, in: `a: null,    b: _|_`},
+		26: {subsumes: true, in: `a: int, b: _|_`},
+		27: {subsumes: true, in: `a: 1,       b: _|_`},
+		28: {subsumes: true, in: `a: float, b: _|_`},
+		29: {subsumes: true, in: `a: "s",     b: _|_`},
+		30: {subsumes: true, in: `a: {},      b: _|_`},
+		31: {subsumes: true, in: `a: [],      b: _|_`},
+		32: {subsumes: true, in: `a: true,    b: _|_`},
+		33: {subsumes: true, in: `a: _|_,       b: _|_`},
+
+		// null subsumes only null
+		34: {subsumes: true, in: ` a: null, b: null `},
+		35: {subsumes: false, in: `a: null, b: 1 `},
+		36: {subsumes: false, in: `a: 1,    b: null `},
+
+		37: {subsumes: true, in: ` a: true, b: true `},
+		38: {subsumes: false, in: `a: true, b: false `},
+
+		39: {subsumes: true, in: ` a: "a",    b: "a" `},
+		40: {subsumes: false, in: `a: "a",    b: "b" `},
+		41: {subsumes: true, in: ` a: string, b: "a" `},
+		42: {subsumes: false, in: `a: "a",    b: string `},
+
+		// Number typing (TODO)
+		//
+		// In principle, an "int" cannot assume an untyped "1", as "1" may
+		// still by typed as a float. They are two different type aspects. When
+		// considering, keep in mind that:
+		//   Key requirement: if A subsumes B, it must not be possible to
+		//   specialize B further such that A does not subsume B. HOWEVER,
+		//   The type conversion rules for conversion are INDEPENDENT of the
+		//   rules for subsumption!
+		// Consider:
+		// - only having number, but allowing user-defined types.
+		//   Subsumption would still work the same, but it may be somewhat
+		//   less weird.
+		// - making 1 always an int and 1.0 always a float.
+		//   - the int type would subsume any derived type from int.
+		//   - arithmetic would allow implicit conversions, but maybe not for
+		//     types.
+		//
+		// TODO: irrational numbers: allow untyped, but require explicit
+		//       trunking when assigning to float.
+		//
+		// a: number; cue.IsInteger(a) && a > 0
+		// t: (x) -> number; cue.IsInteger(a) && a > 0
+		// type x number: cue.IsInteger(x) && x > 0
+		// x: typeOf(number); cue.IsInteger(x) && x > 0
+		43: {subsumes: true, in: `a: 1, b: 1 `},
+		44: {subsumes: true, in: `a: 1.0, b: 1.0 `},
+		45: {subsumes: true, in: `a: 3.0, b: 3.0 `},
+		46: {subsumes: false, in: `a: 1.0, b: 1 `},
+		47: {subsumes: false, in: `a: 1, b: 1.0 `},
+		48: {subsumes: false, in: `a: 3, b: 3.0`},
+		49: {subsumes: true, in: `a: int, b: 1`},
+		50: {subsumes: true, in: `a: int, b: int & 1`},
+		51: {subsumes: true, in: `a: float, b: 1.0`},
+		52: {subsumes: false, in: `a: float, b: 1`},
+		53: {subsumes: false, in: `a: int, b: 1.0`},
+		54: {subsumes: true, in: `a: int, b: int`},
+		55: {subsumes: true, in: `a: number, b: int`},
+
+		// Structs
+		64: {subsumes: true, in: `a: {}, b: {}`},
+		65: {subsumes: true, in: `a: {}, b: {a: 1}`},
+		66: {subsumes: true, in: `a: {a:1}, b: {a:1, b:1}`},
+		67: {subsumes: true, in: `a: {s: { a:1} }, b: { s: { a:1, b:2 }}`},
+		68: {subsumes: true, in: `a: {}, b: {}`},
+		// TODO: allow subsumption of unevaluated values?
+		// ref not yet evaluated and not structurally equivalent
+		69: {subsumes: true, in: `a: {}, b: {} & c, c: {}`},
+
+		70: {subsumes: false, in: `a: {a:1}, b: {}`},
+		71: {subsumes: false, in: `a: {a:1, b:1}, b: {a:1}`},
+		72: {subsumes: false, in: `a: {s: { a:1} }, b: { s: {}}`},
+
+		84: {subsumes: true, in: `a: 1 | 2, b: 2 | 1`},
+		85: {subsumes: true, in: `a: 1 | 2, b: 1 | 2`},
+
+		86: {subsumes: true, in: `a: number, b: 2 | 1`},
+		87: {subsumes: true, in: `a: number, b: 2 | 1`},
+		88: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+
+		89: {subsumes: true, in: `a: float | number, b: 1 | 2 | 3.1`},
+
+		90: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+		91: {subsumes: true, in: `a: 1 | 2, b: 1`},
+		92: {subsumes: true, in: `a: 1 | 2, b: 2`},
+		93: {subsumes: false, in: `a: 1 | 2, b: 3`},
+
+		// Structural
+		94: {subsumes: false, in: `a: int + int, b: int`},
+		95: {subsumes: true, in: `a: int + int, b: int + int`},
+		96: {subsumes: true, in: `a: int + number, b: int + int`},
+		97: {subsumes: true, in: `a: number + number, b: int + int`},
+		// TODO: allow subsumption of unevaluated values?
+		// TODO: may be false if we allow arithmetic on incomplete values.
+		98: {subsumes: false, in: `a: int + int, b: int * int`},
+
+		// TODO: allow subsumption of unevaluated values?
+		// true because both evaluate to bottom
+		99:  {subsumes: true, in: `a: !int, b: !int`},
+		100: {subsumes: true, in: `a: !number, b: !int`},
+		101: {subsumes: true, in: `a: !int, b: !number`},
+
+		// TODO: allow subsumption of unevaluated values?
+		102: {subsumes: false, in: `a: int + int, b: !number`},
+		// TODO: allow subsumption of unevaluated values?
+		103: {subsumes: false, in: `a: !bool, b: bool`},
+		104: {subsumes: true, in: `a: !bool, b: !bool`},
+
+		// Call
+		113: {subsumes: true, in: `
+			a: fn()
+			b: fn()
+			fn: _`,
+		},
+		114: {subsumes: false, in: `
+			a: fn(),
+			b: fn(1)
+			fn: _`,
+		},
+		115: {subsumes: true, in: `
+			a: fn(2)
+			b: fn(2)
+			fn: _`,
+		},
+		116: {subsumes: true, in: `
+			a: fn(number)
+			b: fn(2)
+			fn: _`,
+		},
+		117: {subsumes: false, in: `
+			a: fn(2)
+			b: fn(number)
+			fn: _`,
+		},
+
+		// TODO: allow subsumption of unevaluated values?
+		// TODO: okay, but why false?
+		121: {subsumes: false, in: `a: c + d, b: int, c: int, d: int`},
+		// TODO: allow subsumption of unevaluated values?
+		122: {subsumes: true, in: `a: {}, b: c & {}, c: {}`},
+
+		// references
+		123: {subsumes: true, in: `a: c, b: c, c: {}`},
+		// TODO: allow subsumption of unevaluated values?
+		124: {subsumes: true, in: `a: c, b: d, c: {}, d: {}`},
+		125: {subsumes: false, in: `a: c, b: d, c: {a:1}, d: {}`},
+		// TODO: allow subsumption of unevaluated values?
+		126: {subsumes: true, in: `a: c, b: d, c: {a:1}, d: c & {b:1}`},
+		127: {subsumes: false, in: `a: d, b: c, c: {a:1}, d: c & {b:1}`},
+		128: {subsumes: false, in: `a: c.c, b: c, c: { d: number}`},
+
+		// type unification catches a reference error.
+		129: {subsumes: false, in: `a: c, b: d, c: 1, d: 2`},
+
+		130: {subsumes: true, in: ` a: [1][1], b: [1][1]`},
+		131: {subsumes: true, in: ` a: [1][number], b: [1][1]`},
+		132: {subsumes: true, in: ` a: [number][1], b: [1][1]`},
+		133: {subsumes: true, in: ` a: [number][number], b: [1][1]`},
+		134: {subsumes: false, in: ` a: [1][0], b: [1][number]`},
+		135: {subsumes: false, in: ` a: [1][0], b: [number][0]`},
+		136: {subsumes: true, in: ` a: [number][number], b: [1][number]`},
+		137: {subsumes: true, in: ` a: [number][number], b: [number][1]`},
+		// purely structural:
+		138: {subsumes: false, in: ` a: [number][number], b: number`},
+
+		// interpolations
+		139: {subsumes: true, in: ` a: "\(d)", b: "\(d)", d: _`},
+		// TODO: allow subsumption of unevaluated values?
+		140: {subsumes: true, in: ` a: "\(d)", b: "\(e)", d: _, e: _`},
+
+		141: {subsumes: true, in: ` a: "\(string)", b: "\("foo")"`},
+		// TODO: allow subsumption of unevaluated values?
+		142: {subsumes: true, in: ` a: "\(string)", b: "\(d)", d: "foo"`},
+		143: {subsumes: true, in: ` a: "\("foo")", b: "\("foo")"`},
+		144: {subsumes: false, in: ` a: "\("foo")", b: "\(1) \(2)"`},
+
+		145: {subsumes: false, in: ` a: "s \(d) e", b: "s a e", d: _`},
+		146: {subsumes: false, in: ` a: "s \(d)m\(d) e", b: "s a e", d: _`},
+
+		// 147: {subsumes: true, in: ` a: 7080, b: *7080 | int`, mode: subChoose},
+
+		// Defaults
+		150: {subsumes: false, in: `a: number | *1, b: number | *2`},
+		151: {subsumes: true, in: `a: number | *2, b: number | *2`},
+		152: {subsumes: true, in: `a: int | *float, b: int | *2.0`},
+		153: {subsumes: false, in: `a: int | *2, b: int | *2.0`},
+		154: {subsumes: true, in: `a: number | *2 | *3, b: number | *2`},
+		155: {subsumes: true, in: `a: number, b: number | *2`},
+
+		// Bounds
+		170: {subsumes: true, in: `a: >=2, b: >=2`},
+		171: {subsumes: true, in: `a: >=1, b: >=2`},
+		172: {subsumes: true, in: `a: >0, b: >=2`},
+		173: {subsumes: true, in: `a: >1, b: >1`},
+		174: {subsumes: true, in: `a: >=1, b: >1`},
+		175: {subsumes: false, in: `a: >1, b: >=1`},
+		176: {subsumes: true, in: `a: >=1, b: >=1`},
+		177: {subsumes: true, in: `a: <1, b: <1`},
+		178: {subsumes: true, in: `a: <=1, b: <1`},
+		179: {subsumes: false, in: `a: <1, b: <=1`},
+		180: {subsumes: true, in: `a: <=1, b: <=1`},
+
+		181: {subsumes: true, in: `a: !=1, b: !=1`},
+		182: {subsumes: false, in: `a: !=1, b: !=2`},
+
+		183: {subsumes: false, in: `a: !=1, b: <=1`},
+		184: {subsumes: true, in: `a: !=1, b: <1`},
+		185: {subsumes: false, in: `a: !=1, b: >=1`},
+		186: {subsumes: true, in: `a: !=1, b: <1`},
+
+		187: {subsumes: true, in: `a: !=1, b: <=0`},
+		188: {subsumes: true, in: `a: !=1, b: >=2`},
+		189: {subsumes: true, in: `a: !=1, b: >1`},
+
+		195: {subsumes: false, in: `a: >=2, b: !=2`},
+		196: {subsumes: false, in: `a: >2, b: !=2`},
+		197: {subsumes: false, in: `a: <2, b: !=2`},
+		198: {subsumes: false, in: `a: <=2, b: !=2`},
+
+		200: {subsumes: true, in: `a: =~"foo", b: =~"foo"`},
+		201: {subsumes: false, in: `a: =~"foo", b: =~"bar"`},
+		202: {subsumes: false, in: `a: =~"foo1", b: =~"foo"`},
+
+		203: {subsumes: true, in: `a: !~"foo", b: !~"foo"`},
+		204: {subsumes: false, in: `a: !~"foo", b: !~"bar"`},
+		205: {subsumes: false, in: `a: !~"foo", b: !~"foo1"`},
+
+		// The following is could be true, but we will not go down the rabbit
+		// hold of trying to prove subsumption of regular expressions.
+		210: {subsumes: false, in: `a: =~"foo", b: =~"foo1"`},
+		211: {subsumes: false, in: `a: !~"foo1", b: !~"foo"`},
+
+		220: {subsumes: true, in: `a: <5, b: 4`},
+		221: {subsumes: false, in: `a: <5, b: 5`},
+		222: {subsumes: true, in: `a: <=5, b: 5`},
+		223: {subsumes: false, in: `a: <=5.0, b: 5.00000001`},
+		224: {subsumes: true, in: `a: >5, b: 6`},
+		225: {subsumes: false, in: `a: >5, b: 5`},
+		226: {subsumes: true, in: `a: >=5, b: 5`},
+		227: {subsumes: false, in: `a: >=5, b: 4`},
+		228: {subsumes: true, in: `a: !=5, b: 6`},
+		229: {subsumes: false, in: `a: !=5, b: 5`},
+		230: {subsumes: false, in: `a: !=5.0, b: 5.0`},
+		231: {subsumes: false, in: `a: !=5.0, b: 5`},
+
+		250: {subsumes: true, in: `a: =~ #"^\d{3}$"#, b: "123"`},
+		251: {subsumes: false, in: `a: =~ #"^\d{3}$"#, b: "1234"`},
+		252: {subsumes: true, in: `a: !~ #"^\d{3}$"#, b: "1234"`},
+		253: {subsumes: false, in: `a: !~ #"^\d{3}$"#, b: "123"`},
+
+		// Conjunctions
+		300: {subsumes: true, in: `a: >0, b: >=2 & <=100`},
+		301: {subsumes: false, in: `a: >0, b: >=0 & <=100`},
+
+		310: {subsumes: true, in: `a: >=0 & <=100, b: 10`},
+		311: {subsumes: true, in: `a: >=0 & <=100, b: >=0 & <=100`},
+		312: {subsumes: false, in: `a: !=2 & !=4, b: >3`},
+		313: {subsumes: true, in: `a: !=2 & !=4, b: >5`},
+
+		314: {subsumes: false, in: `a: >=0 & <=100, b: >=0 & <=150`},
+		315: {subsumes: true, in: `a: >=0 & <=150, b: >=0 & <=100`},
+
+		// Disjunctions
+		330: {subsumes: true, in: `a: >5, b: >10 | 8`},
+		331: {subsumes: false, in: `a: >8, b: >10 | 8`},
+
+		// Optional fields
+		// Optional fields defined constraints on fields that are not yet
+		// defined. So even if such a field is not part of the output, it
+		// influences the lattice structure.
+		// For a given A and B, where A and B unify and where A has an optional
+		// field that is not defined in B, the addition of an incompatible
+		// value of that field in B can cause A and B to no longer unify.
+		//
+		400: {subsumes: false, in: `a: {foo: 1}, b: {}`},
+		401: {subsumes: false, in: `a: {foo?: 1}, b: {}`},
+		402: {subsumes: true, in: `a: {}, b: {foo: 1}`},
+		403: {subsumes: true, in: `a: {}, b: {foo?: 1}`},
+
+		404: {subsumes: true, in: `a: {foo: 1}, b: {foo: 1}`},
+		405: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`},
+		406: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`},
+		407: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`},
+
+		408: {subsumes: false, in: `a: {foo: 1}, b: {foo: 2}`},
+		409: {subsumes: false, in: `a: {foo?: 1}, b: {foo: 2}`},
+		410: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: 2}`},
+		411: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 2}`},
+
+		412: {subsumes: true, in: `a: {foo: number}, b: {foo: 2}`},
+		413: {subsumes: true, in: `a: {foo?: number}, b: {foo: 2}`},
+		414: {subsumes: true, in: `a: {foo?: number}, b: {foo?: 2}`},
+		415: {subsumes: false, in: `a: {foo: number}, b: {foo?: 2}`},
+
+		416: {subsumes: false, in: `a: {foo: 1}, b: {foo: number}`},
+		417: {subsumes: false, in: `a: {foo?: 1}, b: {foo: number}`},
+		418: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: number}`},
+		419: {subsumes: false, in: `a: {foo: 1}, b: {foo?: number}`},
+
+		// The one exception of the rule: there is no value of foo that can be
+		// added to b which would cause the unification of a and b to fail.
+		// So an optional field with a value of top is equivalent to not
+		// defining one at all.
+		420: {subsumes: true, in: `a: {foo?: _}, b: {}`},
+
+		430: {subsumes: false, in: `a: {[_]: 4}, b: {[_]: int}`},
+		// TODO: handle optionals.
+		431: {subsumes: false, in: `a: {[_]: int}, b: {[_]: 2}`},
+
+		// 440: {subsumes: true, in: `a: {foo?: 1}, b: {}`, mode: subNoOptional},
+		// 441: {subsumes: true, in: `a: {}, b: {foo?: 1}`, mode: subNoOptional},
+		// 442: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`, mode: subNoOptional},
+		// 443: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`, mode: subNoOptional},
+		// 444: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subNoOptional},
+		// 445: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subNoOptional},
+		// 446: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subNoOptional},
+		// 447: {subsumes: true, in: `a: {}, b: close({})`, mode: subNoOptional},
+		// 448: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subNoOptional},
+
+		// Lists
+		506: {subsumes: true, in: `a: [], b: [] `},
+		507: {subsumes: true, in: `a: [1], b: [1] `},
+		508: {subsumes: false, in: `a: [1], b: [2] `},
+		509: {subsumes: false, in: `a: [1], b: [2, 3] `},
+		510: {subsumes: true, in: `a: [{b: string}], b: [{b: "foo"}] `},
+		511: {subsumes: true, in: `a: [...{b: string}], b: [{b: "foo"}] `},
+		512: {subsumes: false, in: `a: [{b: "foo"}], b: [{b: string}] `},
+		513: {subsumes: false, in: `a: [{b: string}], b: [{b: "foo"}, ...{b: "foo"}] `},
+		520: {subsumes: false, in: `a: [_, int, ...], b: [int, string, ...string] `},
+
+		// Closed structs.
+		600: {subsumes: false, in: `a: close({}), b: {a: 1}`},
+		601: {subsumes: false, in: `a: close({a: 1}), b: {a: 1}`},
+		602: {subsumes: false, in: `a: close({a: 1, b: 1}), b: {a: 1}`},
+		603: {subsumes: false, in: `a: {a: 1}, b: close({})`},
+		604: {subsumes: true, in: `a: {a: 1}, b: close({a: 1})`},
+		605: {subsumes: true, in: `a: {a: 1}, b: close({a: 1, b: 1})`},
+		606: {subsumes: true, in: `a: close({b?: 1}), b: close({b: 1})`},
+		607: {subsumes: false, in: `a: close({b: 1}), b: close({b?: 1})`},
+		608: {subsumes: true, in: `a: {}, b: close({})`},
+		609: {subsumes: true, in: `a: {}, b: close({foo?: 1})`},
+		610: {subsumes: true, in: `a: {foo?:1}, b: close({})`},
+
+		// Definitions are not regular fields.
+		630: {subsumes: false, in: `a: {#a: 1}, b: {a: 1}`},
+		631: {subsumes: false, in: `a: {a: 1}, b: {#a: 1}`},
+
+		// // Subsuming final values.
+		// 700: {subsumes: true, in: `a: {[string]: 1}, b: {foo: 1}`, mode: subFinal},
+		// 701: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subFinal},
+		// 702: {subsumes: true, in: `a: {["foo"]: int}, b: {foo: 1}`, mode: subFinal},
+		// 703: {subsumes: false, in: `a: close({["foo"]: 1}), b: {bar: 1}`, mode: subFinal},
+		// 704: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subFinal},
+		// 705: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subFinal},
+		// 706: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subFinal},
+		// 707: {subsumes: true, in: `a: {}, b: close({})`, mode: subFinal},
+		// 708: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subFinal},
+		// 709: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subFinal},
+		// 710: {subsumes: false, in: `a: {foo: [...string]}, b: {}`, mode: subFinal},
+
+		// // Schema values
+		// 800: {subsumes: true, in: `a: close({}), b: {foo: 1}`, mode: subSchema},
+		// // TODO(eval): FIX
+		// // 801: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subSchema},
+		// 804: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subSchema},
+		// 805: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subSchema},
+		// 806: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subSchema},
+		// 807: {subsumes: true, in: `a: {}, b: close({})`, mode: subSchema},
+		// 808: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subSchema},
+		// 809: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subSchema},
+	}
+
+	re := regexp.MustCompile(`a: (.*).*b: ([^\n]*)`)
+	for i, tc := range testCases {
+		if tc.in == "" {
+			continue
+		}
+		m := re.FindStringSubmatch(strings.Join(strings.Split(tc.in, "\n"), ""))
+		const cutset = "\n ,"
+		key := strings.Trim(m[1], cutset) + " ⊑ " + strings.Trim(m[2], cutset)
+
+		r := runtime.New()
+
+		t.Run(strconv.Itoa(i)+"/"+key, func(t *testing.T) {
+
+			file, err := parser.ParseFile("subsume", tc.in)
+			if err != nil {
+				t.Fatal(err)
+			}
+
+			root, errs := compile.Files(nil, r, file)
+			if errs != nil {
+				t.Fatal(errs)
+			}
+
+			ctx := eval.NewContext(r, root)
+			root.Finalize(ctx)
+
+			// Use low-level lookup to avoid evaluation.
+			var a, b adt.Value
+			for _, arc := range root.Arcs {
+				switch arc.Label {
+				case ctx.StringLabel("a"):
+					a = arc
+				case ctx.StringLabel("b"):
+					b = arc
+				}
+			}
+
+			err = Value(ctx, a, b)
+			got := err == nil
+
+			if got != tc.subsumes {
+				t.Errorf("got %v; want %v (%v vs %v)", got, tc.subsumes, a.Kind(), b.Kind())
+			}
+		})
+	}
+}
diff --git a/internal/core/subsume/subsume.go b/internal/core/subsume/subsume.go
new file mode 100644
index 0000000..9ce210a
--- /dev/null
+++ b/internal/core/subsume/subsume.go
@@ -0,0 +1,127 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// Package subsume defines various subsumption relations.
+package subsume
+
+import (
+	"cuelang.org/go/cue/errors"
+	"cuelang.org/go/internal"
+	"cuelang.org/go/internal/core/adt"
+)
+
+// Profile configures the type of subsumption. One should typically use one
+// of the preconfigured profiles.
+type Profile struct {
+	// Final indicates subsumption should only consider fields that are relevant
+	// to data mode, and ignore definitions, hidden fields, pattern constraints
+	// and additional constraints.
+	Final bool
+
+	// Defaults indicate that default values should be used for the subsumed
+	// value.
+	Defaults bool
+
+	// Ignore optional fields.
+	IgnoreOptional bool
+
+	// IgnoreClosedness ignores closedness of structs and is used for comparing
+	// APIs.
+	IgnoreClosedness bool
+}
+
+var CUE = Profile{}
+
+// Final checks subsumption interpreting the subsumed value as data.
+var Final = Profile{
+	Final:    true,
+	Defaults: true,
+}
+
+// FinalOpen exists as an artifact of the old API. One should probably not use
+// this.
+var FinalOpen = Profile{
+	Final:            true,
+	Defaults:         true,
+	IgnoreClosedness: true,
+}
+
+// API is subsumption used for APIs.
+var API = Profile{
+	IgnoreClosedness: true,
+}
+
+// Value subsumes two values based on their logical (evaluated) values.
+func Value(ctx *adt.OpContext, a, b adt.Value) errors.Error {
+	return CUE.Value(ctx, a, b)
+}
+
+func (p *Profile) Value(ctx *adt.OpContext, a, b adt.Value) errors.Error {
+	s := subsumer{ctx: ctx, Profile: *p}
+	if !s.values(a, b) {
+		return s.getError()
+	}
+	return s.errs
+}
+
+// Check reports whether b is an instance of a.
+func (p *Profile) Check(ctx *adt.OpContext, a, b adt.Value) bool {
+	s := subsumer{ctx: ctx, Profile: *p}
+	return s.values(a, b)
+}
+
+func isBottom(x adt.Node) bool {
+	b, _ := x.(*adt.Bottom)
+	return b != nil
+}
+
+type subsumer struct {
+	ctx  *adt.OpContext
+	errs errors.Error
+
+	Profile
+
+	inexact bool // If true, the result could be a false negative.
+	missing adt.Feature
+	gt      adt.Value
+	lt      adt.Value
+}
+
+func (s *subsumer) errf(msg string, args ...interface{}) {
+	b := s.ctx.NewErrf(msg, args...)
+	s.errs = errors.Append(s.errs, b.Err)
+}
+
+func (s *subsumer) getError() (err errors.Error) {
+	c := s.ctx
+	// src := binSrc(token.NoPos, opUnify, gt, lt)
+	if s.gt != nil && s.lt != nil {
+		// src := binSrc(token.NoPos, opUnify, s.gt, s.lt)
+		if s.missing != 0 {
+			s.errf("missing field %q", s.missing.SelectorString(c))
+		} else if b, ok := adt.BinOp(c, adt.AndOp, s.gt, s.lt).(*adt.Bottom); !ok {
+			s.errf("value not an instance")
+		} else {
+			s.errs = errors.Append(s.errs, b.Err)
+		}
+	}
+	if s.errs == nil {
+		s.errf("value not an instance")
+	}
+	err = s.errs
+	if s.inexact {
+		err = internal.DecorateError(internal.ErrInexact, err)
+	}
+	return err
+}
diff --git a/internal/core/subsume/subsume_test.go b/internal/core/subsume/subsume_test.go
new file mode 100644
index 0000000..757c901
--- /dev/null
+++ b/internal/core/subsume/subsume_test.go
@@ -0,0 +1,61 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+	"testing"
+
+	"cuelang.org/go/cue/parser"
+	"cuelang.org/go/internal/core/adt"
+	"cuelang.org/go/internal/core/compile"
+	"cuelang.org/go/internal/core/eval"
+	"cuelang.org/go/internal/core/runtime"
+)
+
+// For debugging purposes, do not remove.
+func TestX(t *testing.T) {
+	t.Skip()
+
+	r := runtime.New()
+	ctx := eval.NewContext(r, nil)
+
+	const gt = `a: *1 | int`
+	const lt = `a: (*1 | int) & 1`
+
+	a := parse(t, ctx, gt)
+	b := parse(t, ctx, lt)
+
+	p := Profile{Defaults: true}
+	err := p.Check(ctx, a, b)
+	t.Error(err)
+}
+
+func parse(t *testing.T, ctx *adt.OpContext, str string) *adt.Vertex {
+	t.Helper()
+
+	file, err := parser.ParseFile("subsume", str)
+	if err != nil {
+		t.Fatal(err)
+	}
+
+	root, errs := compile.Files(nil, ctx, file)
+	if errs != nil {
+		t.Fatal(errs)
+	}
+
+	root.Finalize(ctx)
+
+	return root
+}
diff --git a/internal/core/subsume/value.go b/internal/core/subsume/value.go
new file mode 100644
index 0000000..c6e691f
--- /dev/null
+++ b/internal/core/subsume/value.go
@@ -0,0 +1,298 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+	"bytes"
+
+	"cuelang.org/go/cue/errors"
+	"cuelang.org/go/internal/core/adt"
+)
+
+func (s *subsumer) values(a, b adt.Value) (result bool) {
+	defer func() {
+		if !result && s.gt == nil && s.lt == nil {
+			s.gt = a
+			s.lt = b
+		}
+	}()
+
+	if a == b {
+		return true
+	}
+
+	if s.Defaults {
+		a = adt.Default(a)
+		b = adt.Default(b)
+	}
+
+	switch b := b.(type) {
+	case *adt.Bottom:
+		// If the value is incomplete, the error is not final. So either check
+		// structural equivalence or return an error.
+		return !b.IsIncomplete()
+
+	case *adt.Vertex:
+		if a, ok := a.(*adt.Vertex); ok {
+			return s.vertices(a, b)
+		}
+		// Safe to ignore arcs of w.
+		return s.values(a, b.Value)
+
+	case *adt.Conjunction:
+		if _, ok := a.(*adt.Conjunction); ok {
+			break
+		}
+		for _, y := range b.Values {
+			if s.values(a, y) {
+				return true
+			}
+		}
+		return false
+
+	case *adt.Disjunction:
+		if _, ok := a.(*adt.Disjunction); ok {
+			break
+		}
+
+		for _, y := range b.Values {
+			if !s.values(a, y) {
+				return false
+			}
+		}
+		return true
+
+	case *adt.NodeLink:
+		// Do not descend into NodeLinks to avoid processing cycles.
+		// TODO: this would work better if all equal nodes shared the same
+		// node link.
+		return deref(a) == deref(b)
+	}
+
+	switch x := a.(type) {
+	case *adt.Top:
+		return true
+
+	case *adt.Bottom:
+		// isBottom(b) was already tested above.
+		return false
+
+	case *adt.BasicType:
+		k := b.Kind()
+		return x.K&k == k
+
+	case *adt.BoundValue:
+		return s.bound(x, b)
+
+	case *adt.Builtin:
+		return x == b
+
+	case *adt.BuiltinValidator:
+		if y := s.ctx.Validate(x, b); y != nil {
+			s.errs = errors.Append(s.errs, y.Err)
+			return false
+		}
+		return true
+
+	case *adt.Null:
+		return b.Kind() == adt.NullKind
+
+	case *adt.Bool:
+		y, ok := b.(*adt.Bool)
+		return ok && x.B == y.B
+
+	case *adt.Num:
+		y, ok := b.(*adt.Num)
+		return ok && x.K&y.K == y.K && test(s.ctx, x, adt.EqualOp, x, y)
+
+	case *adt.String:
+		y, ok := b.(*adt.String)
+		return ok && x.Str == y.Str
+
+	case *adt.Bytes:
+		y, ok := b.(*adt.Bytes)
+		return ok && bytes.Equal(x.B, y.B)
+
+	case *adt.Vertex:
+		y, ok := b.(*adt.Vertex)
+		if !ok {
+			// 	// Under what conditions can we cast to the value?
+			if len(x.Arcs) == 0 && x.Value != nil {
+				return s.values(x.Value, b)
+			}
+			return false
+		}
+		return s.vertices(x, y)
+
+	case *adt.Conjunction:
+		if y, ok := b.(*adt.Conjunction); ok {
+			// A Conjunction subsumes another Conjunction if for all values a in
+			// x there is a value b in y such that a subsumes b.
+			//
+			// This assumes overlapping ranges in disjunctions are merged.If
+			// this is not the case, subsumes will return a false negative,
+			// which is allowed.
+		outerC:
+			for _, a := range x.Values {
+				for _, b := range y.Values {
+					if s.values(a, b) {
+						continue outerC
+					}
+				}
+				// TODO: should this be marked as inexact?
+				return false
+			}
+			return true
+		}
+		subsumed := true
+		for _, a := range x.Values {
+			subsumed = subsumed && s.values(a, b)
+		}
+		return subsumed
+
+	case *adt.Disjunction:
+		// A Disjunction subsumes another Disjunction if all values of y are
+		// subsumed by any of the values of x, and default values in y are
+		// subsumed by the default values of x.
+		//
+		// This assumes that overlapping ranges in x are merged. If this is not
+		// the case, subsumes will return a false negative, which is allowed.
+		if y, ok := b.(*adt.Disjunction); ok {
+			// at least one value in x should subsume each value in d.
+		outerD:
+			for i, b := range y.Values {
+				bDefault := i < y.NumDefaults
+				// v is subsumed if any value in x subsumes v.
+				for j, a := range x.Values {
+					aDefault := j < x.NumDefaults
+					if (aDefault || !bDefault) && s.values(a, b) {
+						continue outerD
+					}
+				}
+				return false
+			}
+			return true
+		}
+		// b is subsumed if any value in x subsumes b.
+		for _, a := range x.Values {
+			if s.values(a, b) {
+				return true
+			}
+		}
+		// TODO: should this be marked as inexact?
+		return false
+
+	case *adt.NodeLink:
+		return deref(x) == deref(b)
+	}
+	return false
+}
+
+func deref(v adt.Expr) *adt.Vertex {
+	switch x := v.(type) {
+	case *adt.Vertex:
+		return x
+	case *adt.NodeLink:
+		return x.Node
+	}
+	return nil
+}
+
+func (s *subsumer) bound(x *adt.BoundValue, v adt.Value) bool {
+	ctx := s.ctx
+	if isBottom(v) {
+		return true
+	}
+
+	switch y := v.(type) {
+	case *adt.BoundValue:
+		if !adt.IsConcrete(y.Value) {
+			return false
+		}
+
+		kx := x.Kind()
+		ky := y.Kind()
+		if (kx&ky)&^kx != 0 {
+			return false
+		}
+		// x subsumes y if
+		// x: >= a, y: >= b ==> a <= b
+		// x: >= a, y: >  b ==> a <= b
+		// x: >  a, y: >  b ==> a <= b
+		// x: >  a, y: >= b ==> a < b
+		//
+		// x: <= a, y: <= b ==> a >= b
+		//
+		// x: != a, y: != b ==> a != b
+		//
+		// false if types or op direction doesn't match
+
+		xv := x.Value
+		yv := y.Value
+		switch x.Op {
+		case adt.GreaterThanOp:
+			if y.Op == adt.GreaterEqualOp {
+				return test(ctx, x, adt.LessThanOp, xv, yv)
+			}
+			fallthrough
+		case adt.GreaterEqualOp:
+			if y.Op == adt.GreaterThanOp || y.Op == adt.GreaterEqualOp {
+				return test(ctx, x, adt.LessEqualOp, xv, yv)
+			}
+		case adt.LessThanOp:
+			if y.Op == adt.LessEqualOp {
+				return test(ctx, x, adt.GreaterThanOp, xv, yv)
+			}
+			fallthrough
+		case adt.LessEqualOp:
+			if y.Op == adt.LessThanOp || y.Op == adt.LessEqualOp {
+				return test(ctx, x, adt.GreaterEqualOp, xv, yv)
+			}
+		case adt.NotEqualOp:
+			switch y.Op {
+			case adt.NotEqualOp:
+				return test(ctx, x, adt.EqualOp, xv, yv)
+			case adt.GreaterEqualOp:
+				return test(ctx, x, adt.LessThanOp, xv, yv)
+			case adt.GreaterThanOp:
+				return test(ctx, x, adt.LessEqualOp, xv, yv)
+			case adt.LessThanOp:
+				return test(ctx, x, adt.GreaterEqualOp, xv, yv)
+			case adt.LessEqualOp:
+				return test(ctx, x, adt.GreaterThanOp, xv, yv)
+			}
+
+		case adt.MatchOp, adt.NotMatchOp:
+			// these are just approximations
+			if y.Op == x.Op {
+				return test(ctx, x, adt.EqualOp, xv, yv)
+			}
+
+		default:
+			// adt.NotEqualOp already handled above.
+			panic("cue: undefined bound mode")
+		}
+
+	case *adt.Num, *adt.String, *adt.Bool:
+		return test(ctx, x, x.Op, y, x.Value)
+	}
+	return false
+}
+
+func test(ctx *adt.OpContext, src adt.Node, op adt.Op, gt, lt adt.Value) bool {
+	x := adt.BinOp(ctx, op, gt, lt)
+	b, ok := x.(*adt.Bool)
+	return ok && b.B
+}
diff --git a/internal/core/subsume/value_test.go b/internal/core/subsume/value_test.go
new file mode 100644
index 0000000..80869c4
--- /dev/null
+++ b/internal/core/subsume/value_test.go
@@ -0,0 +1,427 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+	"regexp"
+	"strconv"
+	"strings"
+	"testing"
+
+	"cuelang.org/go/cue/parser"
+	"cuelang.org/go/internal/core/adt"
+	"cuelang.org/go/internal/core/compile"
+	"cuelang.org/go/internal/core/eval"
+	"cuelang.org/go/internal/core/runtime"
+)
+
+const (
+	subNone = iota
+	subFinal
+	subNoOptional
+	subSchema
+)
+
+func TestValues(t *testing.T) {
+	// Do not inline: the named struct is used as a marker in
+	// testdata/gen.go.
+	type subsumeTest struct {
+		// the result of b ⊑ a, where a and b are defined in "in"
+		subsumes bool
+		in       string
+		mode     int
+	}
+	testCases := []subsumeTest{
+		// Top subsumes everything
+		0: {subsumes: true, in: `a: _, b: _ `},
+		1: {subsumes: true, in: `a: _, b: null `},
+		2: {subsumes: true, in: `a: _, b: int `},
+		3: {subsumes: true, in: `a: _, b: 1 `},
+		4: {subsumes: true, in: `a: _, b: float `},
+		5: {subsumes: true, in: `a: _, b: "s" `},
+		6: {subsumes: true, in: `a: _, b: {} `},
+		7: {subsumes: true, in: `a: _, b: []`},
+		8: {subsumes: true, in: `a: _, b: _|_ `},
+
+		// Nothing besides top subsumed top
+		9:  {subsumes: false, in: `a: null,    b: _`},
+		10: {subsumes: false, in: `a: int, b: _`},
+		11: {subsumes: false, in: `a: 1,       b: _`},
+		12: {subsumes: false, in: `a: float, b: _`},
+		13: {subsumes: false, in: `a: "s",     b: _`},
+		14: {subsumes: false, in: `a: {},      b: _`},
+		15: {subsumes: false, in: `a: [],      b: _`},
+		16: {subsumes: false, in: `a: _|_ ,      b: _`},
+
+		// Bottom subsumes nothing except bottom itself.
+		17: {subsumes: false, in: `a: _|_, b: null `},
+		18: {subsumes: false, in: `a: _|_, b: int `},
+		19: {subsumes: false, in: `a: _|_, b: 1 `},
+		20: {subsumes: false, in: `a: _|_, b: float `},
+		21: {subsumes: false, in: `a: _|_, b: "s" `},
+		22: {subsumes: false, in: `a: _|_, b: {} `},
+		23: {subsumes: false, in: `a: _|_, b: [] `},
+		24: {subsumes: true, in: ` a: _|_, b: _|_ `},
+
+		// All values subsume bottom
+		25: {subsumes: true, in: `a: null,    b: _|_`},
+		26: {subsumes: true, in: `a: int, b: _|_`},
+		27: {subsumes: true, in: `a: 1,       b: _|_`},
+		28: {subsumes: true, in: `a: float, b: _|_`},
+		29: {subsumes: true, in: `a: "s",     b: _|_`},
+		30: {subsumes: true, in: `a: {},      b: _|_`},
+		31: {subsumes: true, in: `a: [],      b: _|_`},
+		32: {subsumes: true, in: `a: true,    b: _|_`},
+		33: {subsumes: true, in: `a: _|_,       b: _|_`},
+
+		// null subsumes only null
+		34: {subsumes: true, in: ` a: null, b: null `},
+		35: {subsumes: false, in: `a: null, b: 1 `},
+		36: {subsumes: false, in: `a: 1,    b: null `},
+
+		37: {subsumes: true, in: ` a: true, b: true `},
+		38: {subsumes: false, in: `a: true, b: false `},
+
+		39: {subsumes: true, in: ` a: "a",    b: "a" `},
+		40: {subsumes: false, in: `a: "a",    b: "b" `},
+		41: {subsumes: true, in: ` a: string, b: "a" `},
+		42: {subsumes: false, in: `a: "a",    b: string `},
+
+		// Number typing (TODO)
+		//
+		// In principle, an "int" cannot assume an untyped "1", as "1" may
+		// still by typed as a float. They are two different type aspects. When
+		// considering, keep in mind that:
+		//   Key requirement: if A subsumes B, it must not be possible to
+		//   specialize B further such that A does not subsume B. HOWEVER,
+		//   The type conversion rules for conversion are INDEPENDENT of the
+		//   rules for subsumption!
+		// Consider:
+		// - only having number, but allowing user-defined types.
+		//   Subsumption would still work the same, but it may be somewhat
+		//   less weird.
+		// - making 1 always an int and 1.0 always a float.
+		//   - the int type would subsume any derived type from int.
+		//   - arithmetic would allow implicit conversions, but maybe not for
+		//     types.
+		//
+		// TODO: irrational numbers: allow untyped, but require explicit
+		//       trunking when assigning to float.
+		//
+		// a: number; cue.IsInteger(a) && a > 0
+		// t: (x) -> number; cue.IsInteger(a) && a > 0
+		// type x number: cue.IsInteger(x) && x > 0
+		// x: typeOf(number); cue.IsInteger(x) && x > 0
+		43: {subsumes: true, in: `a: 1, b: 1 `},
+		44: {subsumes: true, in: `a: 1.0, b: 1.0 `},
+		45: {subsumes: true, in: `a: 3.0, b: 3.0 `},
+		46: {subsumes: false, in: `a: 1.0, b: 1 `},
+		47: {subsumes: false, in: `a: 1, b: 1.0 `},
+		48: {subsumes: false, in: `a: 3, b: 3.0`},
+		49: {subsumes: true, in: `a: int, b: 1`},
+		50: {subsumes: true, in: `a: int, b: int & 1`},
+		51: {subsumes: true, in: `a: float, b: 1.0`},
+		52: {subsumes: false, in: `a: float, b: 1`},
+		53: {subsumes: false, in: `a: int, b: 1.0`},
+		54: {subsumes: true, in: `a: int, b: int`},
+		55: {subsumes: true, in: `a: number, b: int`},
+
+		// Structs
+		64: {subsumes: true, in: `a: {}, b: {}`},
+		65: {subsumes: true, in: `a: {}, b: {a: 1}`},
+		66: {subsumes: true, in: `a: {a:1}, b: {a:1, b:1}`},
+		67: {subsumes: true, in: `a: {s: { a:1} }, b: { s: { a:1, b:2 }}`},
+		68: {subsumes: true, in: `a: {}, b: {}`},
+		// TODO: allow subsumption of unevaluated values?
+		// ref not yet evaluated and not structurally equivalent
+		69: {subsumes: true, in: `a: {}, b: {} & c, c: {}`},
+
+		70: {subsumes: false, in: `a: {a:1}, b: {}`},
+		71: {subsumes: false, in: `a: {a:1, b:1}, b: {a:1}`},
+		72: {subsumes: false, in: `a: {s: { a:1} }, b: { s: {}}`},
+
+		84: {subsumes: true, in: `a: 1 | 2, b: 2 | 1`},
+		85: {subsumes: true, in: `a: 1 | 2, b: 1 | 2`},
+
+		86: {subsumes: true, in: `a: number, b: 2 | 1`},
+		87: {subsumes: true, in: `a: number, b: 2 | 1`},
+		88: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+
+		89: {subsumes: true, in: `a: float | number, b: 1 | 2 | 3.1`},
+
+		90: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+		91: {subsumes: true, in: `a: 1 | 2, b: 1`},
+		92: {subsumes: true, in: `a: 1 | 2, b: 2`},
+		93: {subsumes: false, in: `a: 1 | 2, b: 3`},
+
+		// 147: {subsumes: true, in: ` a: 7080, b: *7080 | int`, mode: subChoose},
+
+		// Defaults
+		150: {subsumes: false, in: `a: number | *1, b: number | *2`},
+		151: {subsumes: true, in: `a: number | *2, b: number | *2`},
+		152: {subsumes: true, in: `a: int | *float, b: int | *2.0`},
+		153: {subsumes: false, in: `a: int | *2, b: int | *2.0`},
+		154: {subsumes: true, in: `a: number | *2 | *3, b: number | *2`},
+		155: {subsumes: true, in: `a: number, b: number | *2`},
+
+		// Bounds
+		170: {subsumes: true, in: `a: >=2, b: >=2`},
+		171: {subsumes: true, in: `a: >=1, b: >=2`},
+		172: {subsumes: true, in: `a: >0, b: >=2`},
+		173: {subsumes: true, in: `a: >1, b: >1`},
+		174: {subsumes: true, in: `a: >=1, b: >1`},
+		175: {subsumes: false, in: `a: >1, b: >=1`},
+		176: {subsumes: true, in: `a: >=1, b: >=1`},
+		177: {subsumes: true, in: `a: <1, b: <1`},
+		178: {subsumes: true, in: `a: <=1, b: <1`},
+		179: {subsumes: false, in: `a: <1, b: <=1`},
+		180: {subsumes: true, in: `a: <=1, b: <=1`},
+
+		181: {subsumes: true, in: `a: !=1, b: !=1`},
+		182: {subsumes: false, in: `a: !=1, b: !=2`},
+
+		183: {subsumes: false, in: `a: !=1, b: <=1`},
+		184: {subsumes: true, in: `a: !=1, b: <1`},
+		185: {subsumes: false, in: `a: !=1, b: >=1`},
+		186: {subsumes: true, in: `a: !=1, b: <1`},
+
+		187: {subsumes: true, in: `a: !=1, b: <=0`},
+		188: {subsumes: true, in: `a: !=1, b: >=2`},
+		189: {subsumes: true, in: `a: !=1, b: >1`},
+
+		195: {subsumes: false, in: `a: >=2, b: !=2`},
+		196: {subsumes: false, in: `a: >2, b: !=2`},
+		197: {subsumes: false, in: `a: <2, b: !=2`},
+		198: {subsumes: false, in: `a: <=2, b: !=2`},
+
+		200: {subsumes: true, in: `a: =~"foo", b: =~"foo"`},
+		201: {subsumes: false, in: `a: =~"foo", b: =~"bar"`},
+		202: {subsumes: false, in: `a: =~"foo1", b: =~"foo"`},
+
+		203: {subsumes: true, in: `a: !~"foo", b: !~"foo"`},
+		204: {subsumes: false, in: `a: !~"foo", b: !~"bar"`},
+		205: {subsumes: false, in: `a: !~"foo", b: !~"foo1"`},
+
+		// The following is could be true, but we will not go down the rabbit
+		// hold of trying to prove subsumption of regular expressions.
+		210: {subsumes: false, in: `a: =~"foo", b: =~"foo1"`},
+		211: {subsumes: false, in: `a: !~"foo1", b: !~"foo"`},
+
+		220: {subsumes: true, in: `a: <5, b: 4`},
+		221: {subsumes: false, in: `a: <5, b: 5`},
+		222: {subsumes: true, in: `a: <=5, b: 5`},
+		223: {subsumes: false, in: `a: <=5.0, b: 5.00000001`},
+		224: {subsumes: true, in: `a: >5, b: 6`},
+		225: {subsumes: false, in: `a: >5, b: 5`},
+		226: {subsumes: true, in: `a: >=5, b: 5`},
+		227: {subsumes: false, in: `a: >=5, b: 4`},
+		228: {subsumes: true, in: `a: !=5, b: 6`},
+		229: {subsumes: false, in: `a: !=5, b: 5`},
+		230: {subsumes: false, in: `a: !=5.0, b: 5.0`},
+		231: {subsumes: false, in: `a: !=5.0, b: 5`},
+
+		250: {subsumes: true, in: `a: =~ #"^\d{3}$"#, b: "123"`},
+		251: {subsumes: false, in: `a: =~ #"^\d{3}$"#, b: "1234"`},
+		252: {subsumes: true, in: `a: !~ #"^\d{3}$"#, b: "1234"`},
+		253: {subsumes: false, in: `a: !~ #"^\d{3}$"#, b: "123"`},
+
+		// Conjunctions
+		300: {subsumes: true, in: `a: >0, b: >=2 & <=100`},
+		301: {subsumes: false, in: `a: >0, b: >=0 & <=100`},
+
+		310: {subsumes: true, in: `a: >=0 & <=100, b: 10`},
+		311: {subsumes: true, in: `a: >=0 & <=100, b: >=0 & <=100`},
+		312: {subsumes: false, in: `a: !=2 & !=4, b: >3`},
+		313: {subsumes: true, in: `a: !=2 & !=4, b: >5`},
+
+		314: {subsumes: false, in: `a: >=0 & <=100, b: >=0 & <=150`},
+		315: {subsumes: true, in: `a: >=0 & <=150, b: >=0 & <=100`},
+
+		// Disjunctions
+		330: {subsumes: true, in: `a: >5, b: >10 | 8`},
+		331: {subsumes: false, in: `a: >8, b: >10 | 8`},
+
+		// Optional fields
+		// Optional fields defined constraints on fields that are not yet
+		// defined. So even if such a field is not part of the output, it
+		// influences the lattice structure.
+		// For a given A and B, where A and B unify and where A has an optional
+		// field that is not defined in B, the addition of an incompatible
+		// value of that field in B can cause A and B to no longer unify.
+		//
+		400: {subsumes: false, in: `a: {foo: 1}, b: {}`},
+		401: {subsumes: false, in: `a: {foo?: 1}, b: {}`},
+		402: {subsumes: true, in: `a: {}, b: {foo: 1}`},
+		403: {subsumes: true, in: `a: {}, b: {foo?: 1}`},
+
+		404: {subsumes: true, in: `a: {foo: 1}, b: {foo: 1}`},
+		405: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`},
+		406: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`},
+		407: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`},
+
+		408: {subsumes: false, in: `a: {foo: 1}, b: {foo: 2}`},
+		409: {subsumes: false, in: `a: {foo?: 1}, b: {foo: 2}`},
+		410: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: 2}`},
+		411: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 2}`},
+
+		412: {subsumes: true, in: `a: {foo: number}, b: {foo: 2}`},
+		413: {subsumes: true, in: `a: {foo?: number}, b: {foo: 2}`},
+		414: {subsumes: true, in: `a: {foo?: number}, b: {foo?: 2}`},
+		415: {subsumes: false, in: `a: {foo: number}, b: {foo?: 2}`},
+
+		416: {subsumes: false, in: `a: {foo: 1}, b: {foo: number}`},
+		417: {subsumes: false, in: `a: {foo?: 1}, b: {foo: number}`},
+		418: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: number}`},
+		419: {subsumes: false, in: `a: {foo: 1}, b: {foo?: number}`},
+
+		// The one exception of the rule: there is no value of foo that can be
+		// added to b which would cause the unification of a and b to fail.
+		// So an optional field with a value of top is equivalent to not
+		// defining one at all.
+		420: {subsumes: true, in: `a: {foo?: _}, b: {}`},
+
+		430: {subsumes: false, in: `a: {[_]: 4}, b: {[_]: int}`},
+		// TODO: handle optionals.
+		431: {subsumes: false, in: `a: {[_]: int}, b: {[_]: 2}`},
+
+		// TODO: the subNoOptional mode used to be used by the equality check.
+		// Now this has its own implementation it is no longer necessary. Keep
+		// around for now in case we still need the more permissive equality
+		// check that can be created by using subsumption.
+		//
+		// 440: {subsumes: true, in: `a: {foo?: 1}, b: {}`, mode: subNoOptional},
+		// 441: {subsumes: true, in: `a: {}, b: {foo?: 1}`, mode: subNoOptional},
+		// 442: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`, mode: subNoOptional},
+		// 443: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`, mode: subNoOptional},
+		// 444: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subNoOptional},
+		// 445: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subNoOptional},
+		// 446: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subNoOptional},
+		// 447: {subsumes: true, in: `a: {}, b: close({})`, mode: subNoOptional},
+		// 448: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subNoOptional},
+
+		// Lists
+		506: {subsumes: true, in: `a: [], b: [] `},
+		507: {subsumes: true, in: `a: [1], b: [1] `},
+		508: {subsumes: false, in: `a: [1], b: [2] `},
+		509: {subsumes: false, in: `a: [1], b: [2, 3] `},
+		510: {subsumes: true, in: `a: [{b: string}], b: [{b: "foo"}] `},
+		511: {subsumes: true, in: `a: [...{b: string}], b: [{b: "foo"}] `},
+		512: {subsumes: false, in: `a: [{b: "foo"}], b: [{b: string}] `},
+		513: {subsumes: false, in: `a: [{b: string}], b: [{b: "foo"}, ...{b: "foo"}] `},
+		520: {subsumes: false, in: `a: [_, int, ...], b: [int, string, ...string] `},
+
+		// Closed structs.
+		600: {subsumes: false, in: `a: close({}), b: {a: 1}`},
+		601: {subsumes: false, in: `a: close({a: 1}), b: {a: 1}`},
+		602: {subsumes: false, in: `a: close({a: 1, b: 1}), b: {a: 1}`},
+		603: {subsumes: false, in: `a: {a: 1}, b: close({})`},
+		604: {subsumes: true, in: `a: {a: 1}, b: close({a: 1})`},
+		605: {subsumes: true, in: `a: {a: 1}, b: close({a: 1, b: 1})`},
+		606: {subsumes: true, in: `a: close({b?: 1}), b: close({b: 1})`},
+		607: {subsumes: false, in: `a: close({b: 1}), b: close({b?: 1})`},
+		608: {subsumes: true, in: `a: {}, b: close({})`},
+		609: {subsumes: true, in: `a: {}, b: close({foo?: 1})`},
+		610: {subsumes: true, in: `a: {foo?:1}, b: close({})`},
+
+		// New in new evaluator.
+		611: {subsumes: false, in: `a: close({foo?:1}), b: close({bar?: 1})`},
+		612: {subsumes: true, in: `a: {foo?:1}, b: close({bar?: 1})`},
+		613: {subsumes: true, in: `a: {foo?:1}, b: close({bar: 1})`},
+
+		// Definitions are not regular fields.
+		630: {subsumes: false, in: `a: {#a: 1}, b: {a: 1}`},
+		631: {subsumes: false, in: `a: {a: 1}, b: {#a: 1}`},
+
+		// Subsuming final values.
+		700: {subsumes: true, in: `a: {[string]: 1}, b: {foo: 1}`, mode: subFinal},
+		701: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subFinal},
+		702: {subsumes: true, in: `a: {["foo"]: int}, b: {foo: 1}`, mode: subFinal},
+		703: {subsumes: false, in: `a: close({["foo"]: 1}), b: {bar: 1}`, mode: subFinal},
+		704: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subFinal},
+		705: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subFinal},
+		706: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subFinal},
+		707: {subsumes: true, in: `a: {}, b: close({})`, mode: subFinal},
+		708: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subFinal},
+		709: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subFinal},
+		710: {subsumes: false, in: `a: {foo: [...string]}, b: {}`, mode: subFinal},
+
+		// Schema values
+		800: {subsumes: true, in: `a: close({}), b: {foo: 1}`, mode: subSchema},
+		// TODO(eval): FIX
+		// 801: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subSchema},
+		804: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subSchema},
+		805: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subSchema},
+		806: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subSchema},
+		807: {subsumes: true, in: `a: {}, b: close({})`, mode: subSchema},
+		808: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subSchema},
+		809: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subSchema},
+	}
+
+	re := regexp.MustCompile(`a: (.*).*b: ([^\n]*)`)
+	for i, tc := range testCases {
+		if tc.in == "" {
+			continue
+		}
+		m := re.FindStringSubmatch(strings.Join(strings.Split(tc.in, "\n"), ""))
+		const cutset = "\n ,"
+		key := strings.Trim(m[1], cutset) + " ⊑ " + strings.Trim(m[2], cutset)
+
+		r := runtime.New()
+
+		t.Run(strconv.Itoa(i)+"/"+key, func(t *testing.T) {
+
+			file, err := parser.ParseFile("subsume", tc.in)
+			if err != nil {
+				t.Fatal(err)
+			}
+
+			root, errs := compile.Files(nil, r, file)
+			if errs != nil {
+				t.Fatal(errs)
+			}
+
+			ctx := eval.NewContext(r, root)
+			root.Finalize(ctx)
+
+			// Use low-level lookup to avoid evaluation.
+			var a, b adt.Value
+			for _, arc := range root.Arcs {
+				switch arc.Label {
+				case ctx.StringLabel("a"):
+					a = arc
+				case ctx.StringLabel("b"):
+					b = arc
+				}
+			}
+
+			switch tc.mode {
+			case subNone:
+				err = Value(ctx, a, b)
+			case subSchema:
+				err = API.Value(ctx, a, b)
+			// TODO: see comments above.
+			// case subNoOptional:
+			// 	err = IgnoreOptional.Value(ctx, a, b)
+			case subFinal:
+				err = Final.Value(ctx, a, b)
+			}
+			got := err == nil
+
+			if got != tc.subsumes {
+				t.Errorf("got %v; want %v (%v vs %v)", got, tc.subsumes, a.Kind(), b.Kind())
+			}
+		})
+	}
+}
diff --git a/internal/core/subsume/vertex.go b/internal/core/subsume/vertex.go
new file mode 100644
index 0000000..6ece49e
--- /dev/null
+++ b/internal/core/subsume/vertex.go
@@ -0,0 +1,256 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+	"cuelang.org/go/internal/core/adt"
+	"cuelang.org/go/internal/core/export"
+)
+
+// Notes:
+// - Can optional fields of y can always be ignored here? Maybe not in the
+//   schema case.
+// - Definitions of y can be ignored in data mode.
+//
+// TODO(perf): use merge sort where possible.
+func (s *subsumer) vertices(x, y *adt.Vertex) bool {
+	if x == y {
+		return true
+	}
+
+	if s.Defaults {
+		x = x.Default()
+		y = y.Default()
+	}
+
+	if b, _ := y.Value.(*adt.Bottom); b != nil {
+		// If the value is incomplete, the error is not final. So either check
+		// structural equivalence or return an error.
+		return !b.IsIncomplete()
+	}
+
+	ctx := s.ctx
+
+	final := y.IsData() || s.Final
+
+	switch v := x.Value.(type) {
+	case *adt.Bottom:
+		return false
+
+	case *adt.ListMarker:
+		if !y.IsList() {
+			s.errf("list does not subsume %s (type %s)", ctx.Str(y), y.Kind())
+			return false
+		}
+		if !s.listVertices(x, y) {
+			return false
+		}
+		// TODO: allow other arcs alongside list arc.
+		return true
+
+	case *adt.StructMarker:
+		_, ok := y.Value.(*adt.StructMarker)
+		if !ok {
+			return false
+		}
+
+	default:
+		if !s.values(v, y.Value) {
+			return false
+		}
+
+		// Embedded scalars could still have arcs.
+		if final {
+			return true
+		}
+	}
+
+	xClosed := x.IsClosed(ctx) && !s.IgnoreClosedness
+	yClosed := y.IsClosed(ctx) && !s.IgnoreClosedness
+
+	if xClosed && !yClosed && !final {
+		return false
+	}
+
+	types := x.OptionalTypes()
+	if !final && !s.IgnoreOptional && types&(adt.HasPattern|adt.HasAdditional) != 0 {
+		// TODO: there are many cases where pattern constraints can be checked.
+		s.inexact = true
+		return false
+	}
+
+	// All arcs in x must exist in y and its values must subsume.
+	xFeatures := export.VertexFeatures(x)
+	for _, f := range xFeatures {
+		if s.Final && !f.IsRegular() {
+			continue
+		}
+
+		a := x.Lookup(f)
+		aOpt := false
+		if a == nil {
+			// x.f is optional
+			if s.IgnoreOptional {
+				continue
+			}
+
+			a = &adt.Vertex{Label: f}
+			x.MatchAndInsert(ctx, a)
+			a.Finalize(ctx)
+
+			// If field a is optional and has value top, neither the
+			// omission of the field nor the field defined with any value
+			// may cause unification to fail.
+			if a.Kind() == adt.TopKind {
+				continue
+			}
+
+			aOpt = true
+		}
+
+		b := y.Lookup(f)
+		if b == nil {
+			// y.f is optional
+			if !aOpt {
+				s.errf("required field %s is optional in subsumed value",
+					f.SelectorString(ctx))
+				return false
+			}
+
+			// If f is undefined for y and if y is closed, the field is
+			// implicitly defined as _|_ and thus subsumed. Technically, this is
+			// even true if a is not optional, but in that case it means that y
+			// is invalid, so return false regardless
+			if !y.Accept(ctx, f) || y.IsData() || s.Final {
+				continue
+			}
+
+			b = &adt.Vertex{Label: f}
+			y.MatchAndInsert(ctx, b)
+			b.Finalize(ctx)
+		}
+
+		if s.values(a, b) {
+			continue
+		}
+
+		s.missing = f
+		s.gt = a
+		s.lt = y
+
+		s.errf("field %s not not present in %s",
+			f.SelectorString(ctx), ctx.Str(y))
+		return false
+	}
+
+	if xClosed && !yClosed && !s.Final {
+		s.errf("closed struct does not subsume open struct")
+		return false
+	}
+
+	yFeatures := export.VertexFeatures(y)
+outer:
+	for _, f := range yFeatures {
+		if s.Final && !f.IsRegular() {
+			continue
+		}
+
+		for _, g := range xFeatures {
+			if g == f {
+				// already validated
+				continue outer
+			}
+		}
+
+		b := y.Lookup(f)
+		if b == nil {
+			if s.IgnoreOptional || s.Final {
+				continue
+			}
+
+			b = &adt.Vertex{Label: f}
+			y.MatchAndInsert(ctx, b)
+		}
+
+		if !x.Accept(ctx, f) {
+			if s.Profile.IgnoreClosedness {
+				continue
+			}
+			s.errf("field %s not allowed in closed struct",
+				f.SelectorString(ctx))
+			return false
+		}
+
+		a := &adt.Vertex{Label: f}
+		x.MatchAndInsert(ctx, a)
+		if len(a.Conjuncts) == 0 {
+			// It is accepted and has no further constraints, so all good.
+			continue
+		}
+
+		a.Finalize(ctx)
+		b.Finalize(ctx)
+
+		if !s.vertices(a, b) {
+			return false
+		}
+	}
+
+	return true
+}
+
+func (s *subsumer) listVertices(x, y *adt.Vertex) bool {
+	ctx := s.ctx
+
+	if !y.IsData() && x.IsClosed(ctx) && !y.IsClosed(ctx) {
+		return false
+	}
+
+	xElems := x.Elems()
+	yElems := y.Elems()
+
+	switch {
+	case len(xElems) == len(yElems):
+	case len(xElems) > len(yElems):
+		return false
+	case x.IsClosed(ctx):
+		return false
+	default:
+		a := &adt.Vertex{Label: adt.InvalidLabel}
+		x.MatchAndInsert(ctx, a)
+		a.Finalize(ctx)
+
+		// x must be open
+		for _, b := range yElems[len(xElems):] {
+			if !s.vertices(a, b) {
+				return false
+			}
+		}
+
+		if !y.IsClosed(ctx) {
+			b := &adt.Vertex{Label: adt.InvalidLabel}
+			y.MatchAndInsert(ctx, b)
+			b.Finalize(ctx)
+		}
+	}
+
+	for i, a := range xElems {
+		if !s.vertices(a, yElems[i]) {
+			return false
+		}
+	}
+
+	return true
+}