diff --git a/Sources/CodeGen/LLVM/TypeLowering.swift b/Sources/CodeGen/LLVM/TypeLowering.swift
index cd780af0d..2af3bacf4 100644
--- a/Sources/CodeGen/LLVM/TypeLowering.swift
+++ b/Sources/CodeGen/LLVM/TypeLowering.swift
@@ -39,7 +39,7 @@ extension IR.Program {
   ///
   /// - Requires: `t` is representable in LLVM.
   func llvm(arrowType t: ArrowType, in module: inout SwiftyLLVM.Module) -> SwiftyLLVM.IRType {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
     let e = llvm(t.environment, in: &module)
     return SwiftyLLVM.StructType([module.ptr, e], in: &module)
   }
@@ -49,7 +49,7 @@ extension IR.Program {
   /// - Requires: `t` is representable in LLVM.
   func llvm(bufferType t: BufferType, in module: inout SwiftyLLVM.Module) -> SwiftyLLVM.IRType {
     let e = llvm(t.element, in: &module)
-    guard let n = t.count.asCompilerKnown(Int.self) else {
+    guard let n = ConcreteTerm(t.count)?.value as? Int else {
       notLLVMRepresentable(t)
     }
     return SwiftyLLVM.ArrayType(n, e, in: &module)
@@ -85,7 +85,7 @@ extension IR.Program {
   func llvm(
     boundGenericType t: BoundGenericType, in module: inout SwiftyLLVM.Module
   ) -> SwiftyLLVM.IRType {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
     precondition(t.base.base is ProductType)
     return demandStruct(named: base.mangled(t), in: &module) { (m) in
       llvm(fields: base.storage(of: t), in: &m)
@@ -96,7 +96,7 @@ extension IR.Program {
   ///
   /// - Requires: `t` is representable in LLVM.
   func llvm(productType t: ProductType, in module: inout SwiftyLLVM.Module) -> SwiftyLLVM.IRType {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
     return demandStruct(named: base.mangled(t), in: &module) { (m) in
       llvm(fields: AbstractTypeLayout(of: t, definedIn: base).properties, in: &m)
     }
@@ -106,7 +106,7 @@ extension IR.Program {
   ///
   /// - Requires: `t` is representable in LLVM.
   func llvm(tupleType t: TupleType, in module: inout SwiftyLLVM.Module) -> SwiftyLLVM.IRType {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
     let fs = llvm(fields: t.elements, in: &module)
     return SwiftyLLVM.StructType(fs, in: &module)
   }
@@ -122,7 +122,7 @@ extension IR.Program {
   ///
   /// - Requires: `t` is representable in LLVM.
   func llvm(unionType t: UnionType, in module: inout SwiftyLLVM.Module) -> SwiftyLLVM.IRType {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
 
     var payload: SwiftyLLVM.IRType = SwiftyLLVM.StructType([], in: &module)
     if t.isNever {
diff --git a/Sources/FrontEnd/AST/AST.swift b/Sources/FrontEnd/AST/AST.swift
index 9eafe3c5a..8cb8c80bd 100644
--- a/Sources/FrontEnd/AST/AST.swift
+++ b/Sources/FrontEnd/AST/AST.swift
@@ -199,6 +199,15 @@ public struct AST {
     return UnionType([t, ^u])
   }
 
+  /// Returns the Hylo type of an array of `t`.
+  ///
+  /// - Requires: The Core library must have been loaded.
+  public func array(_ t: AnyType) -> BoundGenericType {
+    let b = coreType("Array")!
+    let e = self[b.decl].genericParameters[0]
+    return BoundGenericType(b, arguments: [e: .type(t)])
+  }
+
   /// Returns the type named `name` defined in the core library or `nil` it does not exist.
   ///
   /// - Requires: The Core library must have been loaded.
diff --git a/Sources/FrontEnd/AST/Decl/SynthesizedFunctionDecl.swift b/Sources/FrontEnd/AST/Decl/SynthesizedFunctionDecl.swift
index d28721a5e..5987d4c53 100644
--- a/Sources/FrontEnd/AST/Decl/SynthesizedFunctionDecl.swift
+++ b/Sources/FrontEnd/AST/Decl/SynthesizedFunctionDecl.swift
@@ -50,7 +50,7 @@ public struct SynthesizedFunctionDecl: Hashable {
     parameterizedBy genericParameters: [GenericParameterDecl.ID],
     in scope: AnyScopeID
   ) {
-    precondition(type[.isCanonical])
+    precondition(type.isCanonical)
     precondition(type.environment.base is TupleType)
     self.type = type
     self.genericParameters = genericParameters
diff --git a/Sources/FrontEnd/CompileTimeValues/CompileTimeValue.swift b/Sources/FrontEnd/CompileTimeValues/CompileTimeValue.swift
index e7a71ffa1..928aa8462 100644
--- a/Sources/FrontEnd/CompileTimeValues/CompileTimeValue.swift
+++ b/Sources/FrontEnd/CompileTimeValues/CompileTimeValue.swift
@@ -4,35 +4,40 @@ public enum CompileTimeValue: Hashable {
   /// A type.
   case type(AnyType)
 
-  /// An instance of a type known by the compiler (e.g. `Int`).
-  case compilerKnown(AnyHashable)
+  /// A term.
+  case term(AnyTerm)
+
+  /// Properties about the representation of self.
+  public var flags: ValueFlags {
+    switch self {
+    case .type(let t): return t.flags
+    case .term(let t): return t.flags
+    }
+  }
 
   /// The payload of `.type`.
   public var asType: AnyType? {
-    if case .type(let t) = self {
-      return t
-    } else {
-      return nil
-    }
+    if case .type(let v) = self { v } else { nil }
+  }
+
+  /// The payload of `.term`.
+  public var asTerm: AnyTerm? {
+    if case .term(let v) = self { v } else { nil }
   }
 
   /// `true` iff self is in canonical form.
   public var isCanonical: Bool {
-    if let t = asType { t[.isCanonical] } else { true }
+    if let t = asType { t.isCanonical } else { true }
   }
 
   /// `true` if `self` is a `TypeVariable`.
   public var isTypeVariable: Bool {
-    asType?.base is TypeVariable
+    self.asType?.base is TypeVariable
   }
 
   /// The payload of `.compilerKnown` as an instance of `T`.
   public func asCompilerKnown<T>(_: T.Type) -> T? {
-    if case .compilerKnown(let v) = self {
-      return v as? T
-    } else {
-      return nil
-    }
+    ConcreteTerm(self.asTerm)?.value as? T
   }
 
 }
@@ -43,7 +48,7 @@ extension CompileTimeValue: CustomStringConvertible {
     switch self {
     case .type(let v):
       return "\(v)"
-    case .compilerKnown(let v):
+    case .term(let v):
       return "\(v)"
     }
   }
diff --git a/Sources/FrontEnd/CompileTimeValues/ValueFlags.swift b/Sources/FrontEnd/CompileTimeValues/ValueFlags.swift
new file mode 100644
index 000000000..051a1e15a
--- /dev/null
+++ b/Sources/FrontEnd/CompileTimeValues/ValueFlags.swift
@@ -0,0 +1,29 @@
+/// Properties about the representation of a type or term.
+public struct ValueFlags: Hashable, OptionSet {
+
+  public typealias RawValue = UInt8
+
+  public let rawValue: UInt8
+
+  public init(rawValue: UInt8) {
+    self.rawValue = rawValue
+  }
+
+  /// Returns the union of `l` with `r`.
+  public static func | (l: Self, r: Self) -> Self {
+    l.union(r)
+  }
+
+  /// The type contains one or more error types.
+  public static let hasError = ValueFlags(rawValue: 1 << 0)
+
+  /// The type contains open type variables.
+  public static let hasVariable = ValueFlags(rawValue: 1 << 1)
+
+  /// The type contains skolemized variables.
+  public static let hasSkolem = ValueFlags(rawValue: 1 << 2)
+
+  /// The type is not canonical.
+  public static let hasNonCanonical = ValueFlags(rawValue: 1 << 3)
+
+}
diff --git a/Sources/FrontEnd/Terms/AnyTerm.swift b/Sources/FrontEnd/Terms/AnyTerm.swift
new file mode 100644
index 000000000..f040896d1
--- /dev/null
+++ b/Sources/FrontEnd/Terms/AnyTerm.swift
@@ -0,0 +1,107 @@
+import Utils
+
+/// A box wrapping a term.
+private protocol TermBox {
+
+  /// Hashes the salient parts of the wrapped value into `hasher`.
+  func hash(into hasher: inout Hasher)
+
+  /// Returns whether the value wrapped inside `self` is equal to that wrapped inside `other`.
+  func equals<Other: TermBox>(_ other: Other) -> Bool
+
+  /// Returns the value wrapped inside `self` with its type erased.
+  func unwrap() -> any TermProtocol
+
+  /// Returns the value wrapped inside `self` as an instance of `T` or `nil` if that value has a
+  /// different type.
+  func unwrap<T: TermProtocol>(as: T.Type) -> T?
+
+}
+
+/// A box wrapping an instance of `Base`.
+private struct ConcreteTermBox<Base: TermProtocol>: TermBox {
+
+  /// The value wrapped by this instance.
+  let base: Base
+
+  func hash(into hasher: inout Hasher) {
+    base.hash(into: &hasher)
+  }
+
+  func equals<Other: TermBox>(_ other: Other) -> Bool {
+    base == other.unwrap(as: Base.self)
+  }
+
+  func unwrap() -> any TermProtocol {
+    base
+  }
+
+  func unwrap<T: TermProtocol>(as: T.Type) -> T? {
+    base as? T
+  }
+
+}
+
+/// The compile-time representation of the value of an expression.
+public struct AnyTerm {
+
+  /// A shorthand for `^ErrorTerm()`.
+  public static let error = ^ErrorTerm()
+
+  /// The value wrapped by this instance.
+  private var wrapped: TermBox
+
+  /// Creates a type-erased container wrapping the given instance.
+  ///
+  /// - Parameter base: A type to wrap.
+  public init<T: TermProtocol>(_ base: T) {
+    if let t = base as? AnyTerm {
+      self.wrapped = t.wrapped
+    } else {
+      self.wrapped = ConcreteTermBox(base: base)
+    }
+  }
+
+  /// Accesses value wrapped by this instance.
+  ///
+  /// The `base` property can be cast back to its original type using one of the type casting
+  /// operators (`as?`, `as!`, or `as`).
+  public var base: any TermProtocol {
+    wrapped.unwrap()
+  }
+
+}
+
+extension AnyTerm: TermProtocol {
+
+  public var flags: ValueFlags { base.flags }
+
+}
+
+extension AnyTerm: Equatable {
+
+  /// Returns whether `l` is syntactically equal to `r`.
+  public static func == (l: Self, r: Self) -> Bool {
+    l.wrapped.equals(r.wrapped)
+  }
+
+}
+
+extension AnyTerm: Hashable {
+
+  public func hash(into hasher: inout Hasher) {
+    wrapped.hash(into: &hasher)
+  }
+
+}
+
+extension AnyTerm: CustomStringConvertible {
+
+  public var description: String { String(describing: base) }
+
+}
+
+/// Creates a type-erased container wrapping the given instance.
+public prefix func ^ <T: TermProtocol>(_ base: T) -> AnyTerm {
+  AnyTerm(base)
+}
diff --git a/Sources/FrontEnd/Terms/ConcreteTerm.swift b/Sources/FrontEnd/Terms/ConcreteTerm.swift
new file mode 100644
index 000000000..3b0e49629
--- /dev/null
+++ b/Sources/FrontEnd/Terms/ConcreteTerm.swift
@@ -0,0 +1,20 @@
+/// A box wrapping a concrete compile-time value.
+public struct ConcreteTerm: TermProtocol {
+
+  /// The value of the term.
+  public let value: AnyHashable
+
+  /// Creates an instance with the given value.
+  public init(wrapping value: AnyHashable) {
+    self.value = value
+  }
+
+  public var flags: ValueFlags { .init() }
+
+}
+
+extension ConcreteTerm: CustomStringConvertible {
+
+  public var description: String { "\(value)" }
+
+}
diff --git a/Sources/FrontEnd/Terms/ErrorTerm.swift b/Sources/FrontEnd/Terms/ErrorTerm.swift
new file mode 100644
index 000000000..cc2d86340
--- /dev/null
+++ b/Sources/FrontEnd/Terms/ErrorTerm.swift
@@ -0,0 +1,12 @@
+/// A term denoting a type checking error.
+public struct ErrorTerm: TermProtocol {
+
+  public var flags: ValueFlags { .hasError }
+
+}
+
+extension ErrorTerm: CustomStringConvertible {
+
+  public var description: String { "_" }
+
+}
diff --git a/Sources/FrontEnd/Terms/GenericTermParameter.swift b/Sources/FrontEnd/Terms/GenericTermParameter.swift
new file mode 100644
index 000000000..8bd521a79
--- /dev/null
+++ b/Sources/FrontEnd/Terms/GenericTermParameter.swift
@@ -0,0 +1,26 @@
+import Utils
+
+/// A generic type parameter.
+public struct GenericTermParameter: TermProtocol {
+
+  /// The declaration that introduces the parameter.
+  public let decl: GenericParameterDecl.ID
+
+  /// The name of the parameter.
+  public let name: Incidental<String>
+
+  /// Creates an instance denoting the generic type parameter declared by `decl`.
+  public init(_ decl: GenericParameterDecl.ID, ast: AST) {
+    self.decl = decl
+    self.name = Incidental(ast[decl].baseName)
+  }
+
+  public var flags: ValueFlags { .hasSkolem }
+
+}
+
+extension GenericTermParameter: CustomStringConvertible {
+
+  public var description: String { name.value }
+
+}
diff --git a/Sources/FrontEnd/Terms/TermProtocol.swift b/Sources/FrontEnd/Terms/TermProtocol.swift
new file mode 100644
index 000000000..036e34b07
--- /dev/null
+++ b/Sources/FrontEnd/Terms/TermProtocol.swift
@@ -0,0 +1,34 @@
+/// A protocol describing the API of a Hylo term.
+public protocol TermProtocol: Hashable {
+
+  /// Properties about the representation of `self`.
+  var flags: ValueFlags { get }
+
+}
+
+extension TermProtocol {
+
+  /// Creates an instance with the value of `container.base` or returns `nil` if that value has
+  /// a different type.
+  public init?(_ container: AnyTerm) {
+    if let t = container.base as? Self {
+      self = t
+    } else {
+      return nil
+    }
+  }
+
+  /// Creates an instance with the value of `container.base` or returns `nil` if either that value
+  /// has a different type or `container` is `nil`.
+  public init?(_ container: AnyTerm?) {
+    if let t = container.flatMap(Self.init(_:)) {
+      self = t
+    } else {
+      return nil
+    }
+  }
+
+  /// Returns whether the specified flags are raised on this term.
+  public subscript(fs: ValueFlags) -> Bool { flags.contains(fs) }
+
+}
diff --git a/Sources/FrontEnd/Terms/TermVariable.swift b/Sources/FrontEnd/Terms/TermVariable.swift
new file mode 100644
index 000000000..206786855
--- /dev/null
+++ b/Sources/FrontEnd/Terms/TermVariable.swift
@@ -0,0 +1,28 @@
+import Utils
+
+/// A term variable.
+public struct TermVariable: TermProtocol {
+
+  /// The identifier of the variable.
+  public let rawValue: UInt64
+
+  /// Creates an instance with given `rawValue`.
+  public init(_ rawValue: UInt64) {
+    self.rawValue = rawValue
+  }
+
+  public var flags: ValueFlags { .hasVariable }
+
+  /// The context in which this instance was created.
+  var context: UInt8 { UInt8(rawValue >> 56) }
+
+  /// The identifier of this instance.
+  var identifier: UInt64 { ~(255 << 56) & rawValue }
+
+}
+
+extension TermVariable: CustomStringConvertible {
+
+  public var description: String { "%\(context).\(identifier)*" }
+
+}
diff --git a/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift b/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift
index 3bb9fb15b..3e1079d8a 100644
--- a/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift
+++ b/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift
@@ -27,19 +27,19 @@ struct ConstraintSystem {
   /// The root goals that could not be solved.
   private var failureRoots: [GoalIdentity] = []
 
-  /// A map from open type variable to its assignment.
+  /// A map from open type or term variable to its assignment.
   ///
-  /// This map is monotonically extended during constraint solving to assign a type to each open
-  /// variable in the constraint system. A system is complete if it can be used to derive a
-  /// complete substitution map w.r.t. its open type variables.
-  private var typeAssumptions = SubstitutionMap()
+  /// This map is monotonically extended during constraint solving to assign a type or term to each
+  /// open variable in the constraint system. A system is complete if it can be used to derive a
+  /// complete substitution map w.r.t. its open variables.
+  private var substitutions = SubstitutionMap()
 
   /// A map from name expression to its referred declaration.
   ///
   /// This map is monotonically extended during constraint solving to assign a declaration to each
   /// unresolved name expression in the constraint system. A system is complete if it can be used
   /// to derive a complete name binding map w.r.t. its unresolved name expressions.
-  private var bindingAssumptions: [NameExpr.ID: DeclReference]
+  private var bindings: [NameExpr.ID: DeclReference]
 
   /// A map from call expression to its operands after desugaring and implicit resolution.
   private var callOperands: [CallID: [ArgumentResolutionResult]] = [:]
@@ -60,7 +60,7 @@ struct ConstraintSystem {
   /// deduction process if `loggingIsEnabled` is `true`.
   init(_ obligations: ProofObligations, logging loggingIsEnabled: Bool) {
     self.scope = obligations.scope
-    self.bindingAssumptions = obligations.referredDecl
+    self.bindings = obligations.referredDecl
     self.loggingIsEnabled = loggingIsEnabled
     _ = insert(fresh: obligations.constraints)
   }
@@ -73,8 +73,8 @@ struct ConstraintSystem {
     self.fresh = other.fresh
     self.stale = other.stale
     self.failureRoots = other.failureRoots
-    self.typeAssumptions = other.typeAssumptions
-    self.bindingAssumptions = other.bindingAssumptions
+    self.substitutions = other.substitutions
+    self.bindings = other.bindings
     self.callOperands = other.callOperands
     self.penalties = other.penalties
     self.loggingIsEnabled = other.loggingIsEnabled
@@ -107,7 +107,7 @@ struct ConstraintSystem {
       }
 
       goals[g].modifyTypes { (t) in
-        typeAssumptions.reify(t, withVariables: .kept)
+        substitutions.reify(t, withVariables: .kept)
       }
 
       log("- solve: \"\(goals[g])\"")
@@ -184,14 +184,14 @@ struct ConstraintSystem {
       setOutcome(.failure({ (_, _, _) in () }), for: g)
     }
 
-    let m = typeAssumptions.optimized()
+    let m = substitutions.optimized()
     var d = DiagnosticSet()
     for (k, v) in zip(goals.indices, outcomes) where isFailureRoot(k) {
       v!.diagnoseFailure!(&d, m, outcomes)
     }
 
     return Solution(
-      substitutions: m, bindings: bindingAssumptions, callOperands: callOperands,
+      substitutions: m, bindings: bindings, callOperands: callOperands,
       penalties: penalties, diagnostics: d, stale: stale.map({ goals[$0] }))
   }
 
@@ -241,7 +241,7 @@ struct ConstraintSystem {
   /// Returns eiteher `.success` if `g.left` is unifiable with `g.right` or `.failure` otherwise.
   private mutating func solve(equality g: GoalIdentity) -> Outcome {
     let goal = goals[g] as! EqualityConstraint
-    if unify(goal.left, goal.right) {
+    if solve(goal.left, equals: goal.right) {
       return .success
     } else {
       return .failure(failureToSolve(goal))
@@ -267,6 +267,7 @@ struct ConstraintSystem {
   /// If the constraint is strict, then `g.left` must be different than `g.right`.
   private mutating func solve(subtyping g: GoalIdentity) -> Outcome? {
     let goal = goals[g] as! SubtypingConstraint
+    lazy var o = goal.origin.subordinate()
 
     // Note: we're not using canonical equality here since we'll be dealing with aliases and
     // structural equivalences during unification anyway.
@@ -293,11 +294,10 @@ struct ConstraintSystem {
     case (_, let r as UnionType):
       // If `R` is an empty union, so must be `L`.
       if r.elements.isEmpty {
-        return unify(goal.left, goal.right) ? .success : .failure(failureToSolve(goal))
+        return solve(goal.left, equals: goal.right) ? .success : .failure(failureToSolve(goal))
       }
 
       // If `R` has a single element, it must be above (the canonical form of) `L`.
-      let o = goal.origin.subordinate()
       if let e = r.elements.uniqueElement {
         let s = schedule(SubtypingConstraint(goal.left, e, origin: o))
         return delegate(to: [s])
@@ -335,7 +335,6 @@ struct ConstraintSystem {
         postpone(g)
         return nil
       } else {
-        let o = goal.origin.subordinate()
         let s = schedule(inferenceConstraint(goal.left, isSubtypeOf: goal.right, origin: o))
         return delegate(to: [s])
       }
@@ -345,18 +344,16 @@ struct ConstraintSystem {
       // coercible to `R` and that are above `L`, but that set is unbounded unless `R` is a leaf.
       // If it isn't, we have no choice but to postpone the goal.
       if goal.right.isLeaf {
-        return unify(goal.left, goal.right) ? .success : .failure(failureToSolve(goal))
+        return solve(goal.left, equals: goal.right) ? .success : .failure(failureToSolve(goal))
       } else if goal.isStrict {
         postpone(g)
         return nil
       } else {
-        let o = goal.origin.subordinate()
         let s = schedule(inferenceConstraint(goal.left, isSubtypeOf: goal.right, origin: o))
         return delegate(to: [s])
       }
 
     case (let l as RemoteType, _):
-      let o = goal.origin.subordinate()
       let s = schedule(
         SubtypingConstraint(l.bareType, goal.right, strictly: goal.isStrict, origin: o))
       return delegate(to: [s])
@@ -374,7 +371,6 @@ struct ConstraintSystem {
           return .success
         } else {
           var subordinates: [GoalIdentity] = []
-          let o = goal.origin.subordinate()
           for t in traits {
             subordinates.append(
               schedule(ConformanceConstraint(goal.left, conformsTo: t, origin: o)))
@@ -394,12 +390,12 @@ struct ConstraintSystem {
         }
 
         let r = checker.openForUnification(d)
-        let s = schedule(EqualityConstraint(goal.left, ^r, origin: goal.origin.subordinate()))
+        let s = schedule(EqualityConstraint(goal.left, ^r, origin: o))
         return delegate(to: [s])
 
       case .metatype:
         let r = MetatypeType(of: checker.freshVariable())
-        let s = schedule(EqualityConstraint(goal.left, ^r, origin: goal.origin.subordinate()))
+        let s = schedule(EqualityConstraint(goal.left, ^r, origin: o))
         return delegate(to: [s])
       }
 
@@ -412,20 +408,15 @@ struct ConstraintSystem {
       return nil
 
     default:
-      if !goal.left[.isCanonical] || !goal.right[.isCanonical] {
+      if !goal.left.isCanonical || !goal.right.isCanonical {
         let l = checker.canonical(goal.left, in: scope)
         let r = checker.canonical(goal.right, in: scope)
-        assert(l[.isCanonical] && r[.isCanonical])
-
-        let s = schedule(
-          SubtypingConstraint(l, r, strictly: goal.isStrict, origin: goal.origin.subordinate()))
+        let s = schedule(SubtypingConstraint(l, r, strictly: goal.isStrict, origin: o))
         return delegate(to: [s])
-      }
-
-      if goal.isStrict {
+      } else if goal.isStrict {
         return .failure(failureToSolve(goal))
       } else {
-        return unify(goal.left, goal.right) ? .success : .failure(failureToSolve(goal))
+        return solve(goal.left, equals: goal.right) ? .success : .failure(failureToSolve(goal))
       }
     }
   }
@@ -585,7 +576,7 @@ struct ConstraintSystem {
 
     if let i = candidates.viable.uniqueElement {
       let c = candidates.elements[i]
-      bindingAssumptions[goal.memberExpr] = c.reference
+      bindings[goal.memberExpr] = c.reference
 
       var subordinates = insert(fresh: c.constraints)
       subordinates.append(
@@ -777,7 +768,7 @@ struct ConstraintSystem {
 
     let results: Explorations<OverloadConstraint> = explore(g) { (solver, choice) in
       solver.penalties += choice.penalties
-      solver.bindingAssumptions[goal.overloadedExpr] = choice.reference
+      solver.bindings[goal.overloadedExpr] = choice.reference
       return solver.insert(fresh: choice.constraints)
     }
 
@@ -886,21 +877,19 @@ struct ConstraintSystem {
     stale.append(g)
   }
 
-  /// Returns `true` iff `lhs` and `rhs` can be unified, updating the type substitution table.
+  /// Returns `true` iff `lhs` and `rhs` can be unified, updating the substitution table.
   ///
   /// Type unification consists of finding substitutions that makes `lhs` and `rhs` equal. Both
-  /// types are visited in lockstep, updating `self.typeAssumptions` every time either side is a
-  /// type variable for which no substitution has been made yet.
-  private mutating func unify(_ lhs: AnyType, _ rhs: AnyType) -> Bool {
-    lhs.matches(rhs, mutating: &self) { (this, a, b) in
-      this.unifySyntacticallyInequal(a, b)
-    }
+  /// types are visited in lockstep, updating `self.subscritutions` every time either side is a
+  /// variable for which no substitution has been made yet.
+  private mutating func solve(_ lhs: AnyType, equals rhs: AnyType) -> Bool {
+    matches(lhs, rhs)
   }
 
   /// Returns `true` iff `lhs` and `rhs` can be unified.
-  private mutating func unifySyntacticallyInequal(_ lhs: AnyType, _ rhs: AnyType) -> Bool {
-    let t = typeAssumptions[lhs]
-    let u = typeAssumptions[rhs]
+  private mutating func unify(_ lhs: AnyType, _ rhs: AnyType) -> Bool {
+    let t = substitutions[lhs]
+    let u = substitutions[rhs]
 
     switch (t.base, u.base) {
     case (let l as TypeVariable, _):
@@ -912,10 +901,10 @@ struct ConstraintSystem {
       return true
 
     case (let l as UnionType, let r as UnionType):
-      return unifySyntacticallyInequal(l, r)
+      return unify(l, r)
 
-    case _ where !t[.isCanonical] || !u[.isCanonical]:
-      return unify(checker.canonical(t, in: scope), checker.canonical(u, in: scope))
+    case _ where !t.isCanonical || !u.isCanonical:
+      return solve(checker.canonical(t, in: scope), equals: checker.canonical(u, in: scope))
 
     default:
       return checker.areEquivalent(t, u, in: scope)
@@ -923,12 +912,12 @@ struct ConstraintSystem {
   }
 
   /// Returns `true` iff `lhs` and `rhs` can be unified.
-  private mutating func unifySyntacticallyInequal(
+  private mutating func unify(
     _ lhs: UnionType, _ rhs: UnionType
   ) -> Bool {
     for a in lhs.elements {
       var success = false
-      for b in rhs.elements where unify(a, b) {
+      for b in rhs.elements where solve(a, equals: b) {
         success = true
       }
       if !success { return false }
@@ -936,19 +925,132 @@ struct ConstraintSystem {
     return true
   }
 
+  /// Returns `true` iff `lhs` and `rhs` can be unified.
+  private mutating func unify(_ lhs: AnyTerm, _ rhs: AnyTerm) -> Bool {
+    let t = substitutions[lhs]
+    let u = substitutions[rhs]
+
+    switch (t.base, u.base) {
+    case (let l as TermVariable, _):
+      assume(l, equals: u)
+      return true
+
+    case (_, let r as TermVariable):
+      assume(r, equals: t)
+      return true
+
+    default:
+      return t == u
+    }
+  }
+
+  /// Returns `true` iff `t` and `u` are equal under some substitution of their variables.
+  private mutating func matches(_ t: AnyType, _ u: AnyType) -> Bool {
+    switch (t.base, u.base) {
+    case (let lhs as BoundGenericType, let rhs as BoundGenericType):
+      if lhs.arguments.count != rhs.arguments.count { return false }
+      var result = matches(lhs.base, rhs.base)
+      for (a, b) in zip(lhs.arguments, rhs.arguments) {
+        result = matches(a.value, b.value) && result
+      }
+      return result
+
+    case (let lhs as MetatypeType, let rhs as MetatypeType):
+      return matches(lhs.instance, rhs.instance)
+
+    case (let lhs as TupleType, let rhs as TupleType):
+      if !lhs.labels.elementsEqual(rhs.labels) { return false }
+      return matches(lhs.elements, rhs.elements, at: \.type)
+
+    case (let lhs as ArrowType, let rhs as ArrowType):
+      if !lhs.labels.elementsEqual(rhs.labels) { return false }
+      var result = matches(lhs.inputs, rhs.inputs, at: \.type)
+      result = matches(lhs.output, rhs.output) && result
+      result = matches(lhs.environment, rhs.environment) && result
+      return result
+
+    case (let lhs as BufferType, let rhs as BufferType):
+      return matches(lhs.element, rhs.element) && matches(lhs.count, rhs.count)
+
+    case (let lhs as MethodType, let rhs as MethodType):
+      if !lhs.labels.elementsEqual(rhs.labels) || (lhs.capabilities != rhs.capabilities) {
+        return false
+      }
+
+      var result = matches(lhs.inputs, rhs.inputs, at: \.type)
+      result = matches(lhs.output, rhs.output) && result
+      result = matches(lhs.receiver, rhs.receiver) && result
+      return result
+
+    case (let lhs as ParameterType, let rhs as ParameterType):
+      if lhs.access != rhs.access { return false }
+      return matches(lhs.bareType, rhs.bareType)
+
+    case (let lhs as RemoteType, let rhs as RemoteType):
+      if lhs.access != rhs.access { return false }
+      return matches(lhs.bareType, rhs.bareType)
+
+    default:
+      return (t == u) || unify(t, u)
+    }
+  }
+
+  /// Returns `true` iff the result of `matches(_:_:)` applied on all elements from `ts` and `us`
+  /// pairwise is `true`.
+  private mutating func matches<T: Sequence>(
+    _ ts: T, _ us: T, at p: KeyPath<T.Element, AnyType>
+  ) -> Bool {
+    var result = true
+    for (a, b) in zip(ts, us) {
+      result = matches(a[keyPath: p], b[keyPath: p]) && result
+    }
+    return result
+  }
+
+  /// Returns `true` iff `t` and `u` are equal under some substitution of their variables.
+  private mutating func matches(_ t: AnyTerm, _ u: AnyTerm) -> Bool {
+    (t == u) || unify(t, u)
+  }
+
+  /// Returns `true` iff `t` and `u` are equal under some substitution of their variables.
+  private mutating func matches(_ t: CompileTimeValue, _ u: CompileTimeValue) -> Bool {
+    switch (t, u) {
+    case (.type(let lhs), .type(let rhs)):
+      return matches(lhs, rhs)
+    case (.term(let lhs), .term(let rhs)):
+      return matches(lhs, rhs)
+    default:
+      return false
+    }
+  }
+
   /// Extends the type substution table to map `tau` to `substitute`.
   private mutating func assume(_ tau: TypeVariable, equals substitute: AnyType) {
     log("- assume: \"\(tau) = \(substitute)\"")
-    typeAssumptions.assign(substitute, to: tau)
+    substitutions.assign(substitute, to: tau)
+    refresh()
+  }
+
+  /// Extends the term substution table to map `tau` to `substitute`.
+  private mutating func assume(_ tau: TermVariable, equals substitute: AnyTerm) {
+    log("- assume: \"\(tau) = \(substitute)\"")
+    substitutions.assign(substitute, to: tau)
+    refresh()
+  }
 
-    // Refresh stale constraints.
+  /// Refresh stale constraints containing variables that have been assigned.
+  private mutating func refresh() {
     for i in (0 ..< stale.count).reversed() {
       var changed = false
-      goals[stale[i]].modifyTypes({ (type) in
-        let u = typeAssumptions.reify(type, withVariables: .kept)
-        changed = changed || (type != u)
-        return u
-      })
+      goals[stale[i]].modifyTypes { (t) in
+        if t[.hasVariable] {
+          let u = substitutions.reify(t, withVariables: .kept)
+          changed = changed || (t != u)
+          return u
+        } else {
+          return t
+        }
+      }
 
       if changed {
         log("- refresh \(goals[stale[i]])")
diff --git a/Sources/FrontEnd/TypeChecking/Solution.swift b/Sources/FrontEnd/TypeChecking/Solution.swift
index 970c6a173..52eac38b1 100644
--- a/Sources/FrontEnd/TypeChecking/Solution.swift
+++ b/Sources/FrontEnd/TypeChecking/Solution.swift
@@ -21,11 +21,11 @@ struct Solution {
 
   }
 
-  /// The type assumptions made by the solver.
-  private(set) var typeAssumptions: SubstitutionMap
+  /// The type and term substitutions made by the solver.
+  private(set) var substitutions: SubstitutionMap
 
   /// The name binding assumptions made by the solver.
-  private(set) var bindingAssumptions: BindingMap
+  private(set) var bindings: BindingMap
 
   /// A map from call expression to its operands after desugaring and implicit resolution.
   private(set) var callOperands: [CallID: [ArgumentResolutionResult]]
@@ -42,21 +42,21 @@ struct Solution {
   /// Creates an empty solution.
   init() {
     self.init(
-      substitutions: [:], bindings: [:], callOperands: [:],
+      substitutions: .init(), bindings: [:], callOperands: [:],
       penalties: 0, diagnostics: [], stale: [])
   }
 
   /// Creates an instance with the given properties.
   init(
-    substitutions typeAssumptions: SubstitutionMap,
-    bindings bindingAssumptions: [NameExpr.ID: DeclReference],
+    substitutions: SubstitutionMap,
+    bindings: [NameExpr.ID: DeclReference],
     callOperands: [CallID: [ArgumentResolutionResult]],
     penalties: Int,
     diagnostics: DiagnosticSet,
     stale: [Constraint]
   ) {
-    self.typeAssumptions = typeAssumptions
-    self.bindingAssumptions = bindingAssumptions
+    self.substitutions = substitutions
+    self.bindings = bindings
     self.callOperands = callOperands
     self.penalties = penalties
     self.diagnostics = diagnostics
@@ -81,8 +81,8 @@ struct Solution {
   /// Removes the type and binding assumptions that aren't in `other` and incorporate the
   /// penalties and diagnostics of `other` into `self`.
   mutating func formIntersection(_ other: Self) {
-    typeAssumptions.formIntersection(other.typeAssumptions)
-    bindingAssumptions.formIntersection(other.bindingAssumptions)
+    substitutions.formIntersection(other.substitutions)
+    bindings.formIntersection(other.bindings)
     diagnostics.formIntersection(other.diagnostics)
     penalties = max(penalties, other.penalties)
   }
@@ -94,13 +94,13 @@ extension Solution: CustomStringConvertible {
   public var description: String {
     var result = ""
 
-    result.append("typeAssumptions:\n")
-    for (k, v) in typeAssumptions.storage {
+    result.append("substitutions:\n")
+    for (k, v) in substitutions.types {
       result.append("  \(k) : \(v)\n")
     }
 
-    result.append("bindingAssumptions:\n")
-    for (k, v) in bindingAssumptions {
+    result.append("bindings:\n")
+    for (k, v) in bindings {
       result.append("  \(k) : \(v)\n")
     }
 
diff --git a/Sources/FrontEnd/TypeChecking/SubstitutionMap.swift b/Sources/FrontEnd/TypeChecking/SubstitutionMap.swift
index 627fed6b5..ed55329ee 100644
--- a/Sources/FrontEnd/TypeChecking/SubstitutionMap.swift
+++ b/Sources/FrontEnd/TypeChecking/SubstitutionMap.swift
@@ -1,7 +1,7 @@
-/// A substitution table mapping type variables to assumptions during type inference.
+/// A substitution table mapping type and term variables to assumptions during inference.
 struct SubstitutionMap {
 
-  /// A policy for substituting type variales during reification.
+  /// A policy for substituting variables during reification.
   enum SubstitutionPolicy {
 
     /// Free variables are substituted by errors.
@@ -10,35 +10,80 @@ struct SubstitutionMap {
     /// Free variables are kept.
     case kept
 
+    /// Returns the application of this policy to `t`.
+    fileprivate func callAsFunction(_ t: TypeVariable) -> AnyType {
+      switch self {
+      case .substitutedByError:
+        return .error
+      case .kept:
+        return ^t
+      }
+    }
+
+    /// Returns the application of this policy to `t`.
+    fileprivate func callAsFunction(_ t: TermVariable) -> AnyTerm {
+      switch self {
+      case .substitutedByError:
+        return .error
+      case .kept:
+        return ^t
+      }
+    }
+
   }
 
-  /// The internal storage of a substitution table.
-  typealias Storage = [TypeVariable: AnyType]
+  /// A map from type variable to its assignment.
+  private(set) var types: [TypeVariable: AnyType]
 
-  /// The internal storage of the map.
-  private(set) var storage: Storage = [:]
+  /// A map from term variable to its assignment.
+  private(set) var terms: [TermVariable: AnyTerm]
 
   /// Creates an empty substitution map.
-  init() {}
+  init() {
+    self.init(types: [:], terms: [:])
+  }
+
+  /// Creates an instance with the given properties.
+  private init(types: [TypeVariable: AnyType], terms: [TermVariable: AnyTerm]) {
+    self.types = types
+    self.terms = terms
+  }
 
   /// Returns a copy of this instance with its internal representation optimized.
   func optimized() -> Self {
-    var result = SubstitutionMap()
-    result.storage = storage.mapValues({ self[$0] })
-    return result
+    .init(
+      types: types.mapValues({ self[$0] }),
+      terms: terms.mapValues({ self[$0] }))
   }
 
-  /// Returns the substitution for `variable`, if any.
-  subscript(variable: TypeVariable) -> AnyType? {
-    storage[walk(variable)]
+  /// Returns the substitution for `v`, if any.
+  subscript(v: TypeVariable) -> AnyType? {
+    types[walk(v)]
   }
 
-  /// Returns the substitution for `type` if it is a variable to which a type is assigned in this
-  /// map; returns `type` otherwise.
-  subscript(type: AnyType) -> AnyType {
-    var walked = type
+  /// Returns the substitution of `t` in this map or `t` is no such substitution exists.
+  subscript(t: AnyType) -> AnyType {
+    var walked = t
     while let a = TypeVariable(walked) {
-      if let b = storage[a] {
+      if let b = types[a] {
+        walked = b
+      } else {
+        break
+      }
+    }
+    return walked
+  }
+
+  /// Returns the substitution for `v`, if any.
+  subscript(v: TermVariable) -> AnyTerm? {
+    terms[walk(v)]
+  }
+
+  /// Returns the substitution of `t` in this map or `t` is no such substitution exists.
+  subscript(t: AnyTerm) -> AnyTerm {
+    var walked = t
+    while let a = TermVariable(walked) {
+      if let b = terms[a] {
         walked = b
       } else {
         break
@@ -50,7 +95,7 @@ struct SubstitutionMap {
   /// Assigns `substitution` to `variable`.
   mutating func assign(_ substitution: AnyType, to variable: TypeVariable) {
     var walked = variable
-    while let a = storage[walked] {
+    while let a = types[walked] {
       guard let b = TypeVariable(a) else {
         precondition(a == substitution, "'\(variable)' already bound to '\(a)'")
         return
@@ -61,13 +106,33 @@ struct SubstitutionMap {
     precondition(
       !occurCheck(walked, substitution),
       "illegal substitution: '\(walked)' for '\(substitution)'")
-    storage[walked] = substitution
+    types[walked] = substitution
+  }
+
+  /// Assigns `substitution` to `variable`.
+  mutating func assign(_ substitution: AnyTerm, to variable: TermVariable) {
+    var walked = variable
+    while let a = terms[walked] {
+      guard let b = TermVariable(a) else {
+        precondition(a == substitution, "'\(variable)' already bound to '\(a)'")
+        return
+      }
+      walked = b
+    }
+    terms[walked] = substitution
   }
 
   /// Returns the type variable representing the equivalence class of `v` in `self`.
   private func walk(_ v: TypeVariable) -> TypeVariable {
     var w = v
-    while let a = TypeVariable(storage[w]) { w = a }
+    while let a = TypeVariable(types[w]) { w = a }
+    return w
+  }
+
+  /// Returns the term variable representing the equivalence class of `v` in `self`.
+  private func walk(_ v: TermVariable) -> TermVariable {
+    var w = v
+    while let a = TermVariable(terms[w]) { w = a }
     return w
   }
 
@@ -81,8 +146,8 @@ struct SubstitutionMap {
     return occurs
   }
 
-  /// Returns a copy of `type` where type variable occurring in is replaced by its corresponding
-  /// substitution in `self`, applying `substitutionPolicy` to deal with free variables.
+  /// Returns a copy of `type` where each variable is replaced by its substitution in `self` or the
+  /// application of `substitutionPolicy` is no such substitution exists.
   ///
   /// The default substitution policy is `substituteByError` because we typically use `reify` after
   /// having built a complete solution and therefore don't expect its result to still contain open
@@ -91,97 +156,100 @@ struct SubstitutionMap {
     _ type: AnyType, withVariables substitutionPolicy: SubstitutionPolicy = .substitutedByError
   ) -> AnyType {
     type.transform { (t: AnyType) -> TypeTransformAction in
-      if t.base is TypeVariable {
-        let walked = self[t]
+      switch t.base {
+      case let u as BufferType:
+        let n = reify(u.count, withVariables: substitutionPolicy)
+        return .stepInto(^BufferType(u.element, n))
 
-        // Substitute `walked` for `type`.
-        if walked.base is TypeVariable {
-          switch substitutionPolicy {
-          case .substitutedByError:
-            return .stepOver(.error)
-          case .kept:
-            return .stepOver(walked)
-          }
+      case _ where t[.hasVariable]:
+        let walked = self[t]
+        if let w = TypeVariable(walked) {
+          return .stepOver(substitutionPolicy(w))
         } else {
           return .stepInto(walked)
         }
-      } else if !t[.hasVariable] {
+
+      default:
         // Nothing to do if the type doesn't contain any variable.
         return .stepOver(t)
-      } else {
-        // Recursively visit other types.
-        return .stepInto(t)
       }
     }
   }
 
+  /// Returns a copy of `term` where each variable is replaced by its substitution in `self` or the
+  /// application of `substitutionPolicy` is no such substitution exists.
+  func reify(
+    _ term: AnyTerm, withVariables substitutionPolicy: SubstitutionPolicy
+  ) -> AnyTerm {
+    let walked = self[term]
+    return TermVariable(walked).map({ (w) in substitutionPolicy(w) }) ?? walked
+  }
+
   /// Returns a copy of `r` where each generic argument is replaced by the result of applying
   /// `reify(withVariables:)` on it.
   func reify(
-    _ r: DeclReference, withVariables substitutionPolicy: SubstitutionPolicy
+    reference r: DeclReference, withVariables substitutionPolicy: SubstitutionPolicy
   ) -> DeclReference {
     switch r {
     case .direct(let d, let a):
-      return .direct(d, reify(a, withVariables: substitutionPolicy))
+      return .direct(d, reify(argument: a, withVariables: substitutionPolicy))
     case .member(let d, let a, let r):
-      return .member(d, reify(a, withVariables: substitutionPolicy), r)
+      return .member(d, reify(argument: a, withVariables: substitutionPolicy), r)
     case .constructor(let d, let a):
-      return .constructor(d, reify(a, withVariables: substitutionPolicy))
+      return .constructor(d, reify(argument: a, withVariables: substitutionPolicy))
     case .builtinModule, .builtinType, .builtinFunction, .compilerKnownType:
       return r
     }
   }
 
-  /// Returns `a` with its type variables replaced by their their corresponding value in `self`,
-  /// applying `substitutionPolicy` to handle free variables.
+  /// Returns a copy of `a` where each variable is replaced by its substitution value in `self` or
+  /// the application `substitutionPolicy` is no such substitution exists.
   private func reify(
-    _ a: GenericArguments, withVariables substitutionPolicy: SubstitutionPolicy
+    argument a: GenericArguments, withVariables substitutionPolicy: SubstitutionPolicy
   ) -> GenericArguments {
     a.mapValues({ reify(value: $0, withVariables: substitutionPolicy) })
   }
 
-  /// Returns `v` with its type variables replaced by their their corresponding value in `self`,
-  /// applying `substitutionPolicy` to handle free variables.
+  /// Returns a copy of `v` where each variable is replaced by its substitution value in `self` or
+  /// the application `substitutionPolicy` is no such substitution exists.
   private func reify(
     value v: CompileTimeValue, withVariables substitutionPolicy: SubstitutionPolicy
   ) -> CompileTimeValue {
-    if case .type(let t) = v {
+    switch v {
+    case .type(let t):
       return .type(reify(t, withVariables: substitutionPolicy))
-    } else {
-      return v
+    case .term(let t):
+      return .term(reify(t, withVariables: substitutionPolicy))
     }
   }
 
   /// Removes the key/value pairs in `self` that are not also in `other`.
   mutating func formIntersection(_ other: Self) {
-    for (key, lhs) in storage {
-      storage[key] = (lhs == other[key]) ? lhs : nil
-    }
+    self = self.intersection(other)
   }
 
   /// Returns a new substitution map containing the key/value pairs common to `self` and `other`.
   func intersection(_ other: Self) -> Self {
     var result = SubstitutionMap()
-    for (key, lhs) in storage {
-      result.storage[key] = (lhs == other[key]) ? lhs : nil
+    result.types.reserveCapacity(types.capacity)
+    result.terms.reserveCapacity(terms.capacity)
+    for (key, lhs) in types {
+      result.types[key] = (lhs == other[key]) ? lhs : nil
     }
-    return result
-  }
-
-}
-
-extension SubstitutionMap: ExpressibleByDictionaryLiteral {
-
-  init(dictionaryLiteral elements: (TypeVariable, AnyType)...) {
-    for (k, v) in elements {
-      self.assign(v, to: k)
+    for (key, lhs) in terms {
+      result.terms[key] = (lhs == other[key]) ? lhs : nil
     }
+    return result
   }
 
 }
 
 extension SubstitutionMap: CustomStringConvertible {
 
-  var description: String { String(describing: storage) }
+  var description: String {
+    let ts = types.map({ "\($0.key): \($0.value)" })
+    let us = terms.map({ "\($0.key): \($0.value)" })
+    return "[\(list: ts + us)]"
+  }
 
 }
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift b/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
index 598e23bb9..202c60dbe 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
@@ -102,6 +102,12 @@ extension Diagnostic {
     .error("incompatible types '\(l)' and '\(r)'", at: site)
   }
 
+  static func error(
+    expected: AnyType, found: AnyType, at site: SourceRange
+  ) -> Diagnostic {
+    .error("expected type '\(expected)' but found '\(found)'", at: site)
+  }
+
   static func error(invalidDestructuringOfType type: AnyType, at site: SourceRange) -> Diagnostic {
     .error("invalid destructuring of type '\(type)'", at: site)
   }
@@ -242,10 +248,6 @@ extension Diagnostic {
     .error("non-generic type '\(type)' has no generic parameters", at: site)
   }
 
-  static func error(tooManyAnnotationsOnGenericValueParametersAt site: SourceRange) -> Diagnostic {
-    .error("only one annotation is allowed on generic value parameter declarations", at: site)
-  }
-
   static func error(
     invalidBufferTypeExprArgumentCount e: SubscriptCallExpr.ID, in ast: AST
   ) -> Diagnostic {
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker.swift b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
index 3b8d27bf8..5ba6af518 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
@@ -76,20 +76,24 @@ struct TypeChecker {
 
   /// Returns the canonical form of `t` in `scopeOfUse`.
   mutating func canonical(_ t: AnyType, in scopeOfUse: AnyScopeID) -> AnyType {
-    if t[.isCanonical] { return t }
+    if t.isCanonical { return t }
 
+    let r: AnyType
     switch t.base {
     case let u as AssociatedTypeType:
-      return canonical(u, in: scopeOfUse)
+      r = canonical(u, in: scopeOfUse)
     case let u as BoundGenericType:
-      return canonical(u, in: scopeOfUse)
+      r = canonical(u, in: scopeOfUse)
     case let u as TypeAliasType:
-      return canonical(u.aliasee.value, in: scopeOfUse)
+      r = canonical(u.aliasee.value, in: scopeOfUse)
     case let u as UnionType:
-      return canonical(u, in: scopeOfUse)
+      r = canonical(u, in: scopeOfUse)
     default:
-      return t.transformParts(mutating: &self, { .stepOver($0.canonical($1, in: scopeOfUse)) })
+      r = t.transformParts(mutating: &self, { .stepOver($0.canonical($1, in: scopeOfUse)) })
     }
+
+    assert(r.isCanonical)
+    return r
   }
 
   /// Returns the canonical form of `t` in `scopeOfUse`.
@@ -103,7 +107,7 @@ struct TypeChecker {
 
   /// Returns the canonical form of `t` in `scopeOfUse`.
   private mutating func canonical(_ t: BoundGenericType, in scopeOfUse: AnyScopeID) -> AnyType {
-    if t[.isCanonical] { return ^t }
+    if t.isCanonical { return ^t }
 
     let b = canonical(t.base, in: scopeOfUse)
     let a = canonical(GenericArguments(t), in: scopeOfUse)
@@ -113,7 +117,7 @@ struct TypeChecker {
 
   /// Returns the canonical form of `t` in `scopeOfUse`.
   private mutating func canonical(_ t: UnionType, in scopeOfUse: AnyScopeID) -> AnyType {
-    if t[.isCanonical] { return ^t }
+    if t.isCanonical { return ^t }
 
     var elements = Set<AnyType>()
     for e in t.elements {
@@ -499,7 +503,7 @@ struct TypeChecker {
   func cachedConformance(
     of model: AnyType, to trait: TraitType, exposedTo scopeOfUse: AnyScopeID
   ) -> Conformance? {
-    assert(model[.isCanonical])
+    assert(model.isCanonical)
 
     // `A<X>: T` iff `A: T`.
     if let t = BoundGenericType(model) {
@@ -1173,7 +1177,7 @@ struct TypeChecker {
     // Note: in theory, we should make sure this update is monotonic. In practice, such a test
     // would require prohibitively expensive structural comparisons.
     modify(&cache.uncheckedType[d]!) { (u) in
-      let v = solution.typeAssumptions.reify(u.computed!)
+      let v = solution.substitutions.reify(u.computed!)
       u = .computed(v)
       return v
     }
@@ -1785,7 +1789,7 @@ struct TypeChecker {
         return
       }
 
-      assert(expectedType[.isCanonical] && b.type[.isCanonical])
+      assert(expectedType.isCanonical && b.type.isCanonical)
       // TODO: Use semantic equality
       if program[d].isDefinition && (b.type == expectedType) {
         s.append(AnyDeclID(d))
@@ -1858,7 +1862,7 @@ struct TypeChecker {
     var obligations = ProofObligations(scope: program[d].scope)
     let t = inferredType(of: d, usedAs: purpose, updating: &obligations)
     let s = discharge(obligations, relatedTo: d)
-    let u = s.typeAssumptions.reify(t)
+    let u = s.substitutions.reify(t)
     cache.write(s.isSound ? u : .error, at: \.declType[d], ignoringSharedCache: ignoreSharedCache)
     return u
   }
@@ -1867,7 +1871,7 @@ struct TypeChecker {
   private mutating func checkedType(of e: AnyExprID, withHint hint: AnyType? = nil) -> AnyType {
     let (incompleteType, obligations) = partiallyCheckedType(of: e, withHint: hint)
     let s = discharge(obligations, relatedTo: e)
-    return s.typeAssumptions.reify(incompleteType)
+    return s.substitutions.reify(incompleteType)
   }
 
   /// Type checks `e` as an argument to `p` and returns its type.
@@ -1878,7 +1882,7 @@ struct TypeChecker {
     obligations.insert(
       ParameterConstraint(incompleteType, ^p, origin: .init(.argument, at: program[e].site)))
     let s = discharge(obligations, relatedTo: e)
-    return s.typeAssumptions.reify(incompleteType)
+    return s.substitutions.reify(incompleteType)
   }
 
   /// Returns the inferred type of `e`, along with a set of goals to solve to check that type.
@@ -2351,64 +2355,6 @@ struct TypeChecker {
     return i
   }
 
-  /// Returns `(trait, hasError)` where `trait` is the trait to which `bound` resolves or `nil` if
-  /// it resolves to another entity, and `hasError` is `true` iff name resolution failed.
-  ///
-  /// This method does not run standard name resolution on `bound`, as it may require information
-  /// in which `bound` occurs. Instead, it processes the components of `bound` one by one, bailing
-  /// out as soon as it find one that denotes a type or expression since trait declarations can
-  /// only occur at global scope.
-  ///
-  /// - Parameters:
-  ///   - bound: The expression of a bound on a generic parameter declaration or the RHS of a
-  ///     conformance constraint in a where clause.
-  ///   - scopeOfUse: The declaration defining the environment in which `bound` occurs.
-  private mutating func resolveTrait(
-    expressedBy bound: NameExpr.ID,
-    inEnvironmentOf scopeOfUse: AnyScopeID
-  ) -> (trait: TraitType?, hasError: Bool) {
-    let (n, d) = program.ast.splitNominalComponents(of: bound)
-
-    // `bound` can't denote a trait if it contains a non-nominal component.
-    if d != .none {
-      return (nil, false)
-    }
-
-    // `bound` can't denote a trait if it refers to a generic parameter.
-    if let ns = names(introducedIn: scopeOfUse)[program[n.last!].name.value.stem] {
-      if ns.contains(where: { $0.kind == GenericParameterDecl.self }) {
-        return (nil, false)
-      }
-    }
-
-    // We can apply name resolution on the components of `bound` as long as they don't have
-    // generic arguments. A name expression with arguments can't denote a trait.
-    var parent: NameResolutionContext? = nil
-    for c in n.reversed() {
-      if !program[c].arguments.isEmpty {
-        return (nil, false)
-      }
-
-      let candidates = resolve(c, in: parent, usedAs: .unapplied)
-      if candidates.isEmpty {
-        return (nil, true)
-      }
-
-      guard let pick = candidates.uniqueElement else {
-        return (nil, false)
-      }
-
-      switch pick.type.base {
-      case is ModuleType, is NamespaceType, is TraitType:
-        parent = .init(type: pick.type, arguments: .empty, receiver: .explicit(AnyExprID(c)))
-      default:
-        return (nil, false)
-      }
-    }
-
-    return (TraitType(parent?.type), false)
-  }
-
   /// Returns the type of `d`, computing it if necessary, without type checking `d`.
   ///
   /// This method returns the value for `d` in `cache[\.declType]` or `cache.uncheckedType` if
@@ -2564,32 +2510,11 @@ struct TypeChecker {
 
   /// Computes and returns the type of `d`.
   private mutating func _uncheckedType(of d: GenericParameterDecl.ID) -> AnyType {
-    // If `p` is introduced without any bounds, it is assumed to be type-kinded.
-    guard let bounds = program[d].conformances.headAndTail else {
-      return ^MetatypeType(of: GenericTypeParameterType(d, ast: program.ast))
-    }
-
-    // Otherwise, the first bound of `p` determines its kind.
-    let (firstBoundAsTrait, nameResolutionFailed) = resolveTrait(
-      expressedBy: bounds.head, inEnvironmentOf: program[d].scope)
-
-    // Register failures so we can fail fast.
-    if nameResolutionFailed {
+    if isTypeKinded(d) {
       return ^MetatypeType(of: GenericTypeParameterType(d, ast: program.ast))
-    }
-
-    // If the first bound is a trait, then `p` is type-kinded.
-    if firstBoundAsTrait != nil {
-      return ^MetatypeType(of: GenericTypeParameterType(d, ast: program.ast))
-    }
-
-    // Otherwise, `p` is value-kinded.
-    else {
-      let rhs = evalTypeAnnotation(AnyExprID(bounds.head))
-      if let n = bounds.tail.first {
-        report(.error(tooManyAnnotationsOnGenericValueParametersAt: program[n].site))
-      }
-      return rhs
+    } else {
+      let bound = program[d].conformances.uniqueElement!
+      return evalTypeAnnotation(AnyExprID(bound))
     }
   }
 
@@ -3044,6 +2969,25 @@ struct TypeChecker {
     }
   }
 
+  /// Evaluates `e` as a buffer type expression, having inferred that the type of the buffer's
+  /// elements is `t`.
+  private mutating func evalBufferTypeExpression(
+    _ e: SubscriptCallExpr.ID, havingInferredElementType t: AnyType
+  ) -> MetatypeType {
+    let n = program[e].arguments[0].value
+    let i = program.ast.coreType("Int")!
+    let j = checkedType(of: n, withHint: ^i)
+
+    // Bail out if the type of the argument isn't `Hylo.Int`.
+    if j != i {
+      report(.error(expected: ^i, found: j, at: program[n].site))
+      return MetatypeType(of: BufferType(t, ^ConcreteTerm(wrapping: 0)))
+    } else {
+      let v = denotation(of: n).asTerm!
+      return MetatypeType(of: BufferType(t, v))
+    }
+  }
+
   /// Ensures that `t` is a valid type for an annotation and returns its meaning iff it is;
   /// otherwise, returns `nil`.
   private mutating func ensureValidTypeAnnotation(
@@ -3084,7 +3028,7 @@ struct TypeChecker {
   /// Returns the value expressed by `e`
   private func denotation(of e: IntegerLiteralExpr.ID) -> CompileTimeValue {
     if cache.local.exprType[e]! == program.ast.coreType("Int")! {
-      return .compilerKnown(Int(program[e].value)!)
+      return .term(^ConcreteTerm(wrapping: Int(program[e].value)!))
     } else {
       UNIMPLEMENTED("arbitrary compile-time literals")
     }
@@ -3092,7 +3036,15 @@ struct TypeChecker {
 
   /// Returns the value expressed by `e`
   private func denotation(of e: NameExpr.ID) -> CompileTimeValue {
-    UNIMPLEMENTED()
+    guard let d = cache.local.referredDecl[e] else {
+      return .term(^ErrorTerm())
+    }
+
+    if let p = d.decl.flatMap(GenericParameterDecl.ID.init(_:)) {
+      return .term(^GenericTermParameter(p, ast: program.ast))
+    } else {
+      UNIMPLEMENTED("denotation of \(e.kind)")
+    }
   }
 
   /// Evaluates and returns the qualification of `e`, which is a type annotation.
@@ -4667,7 +4619,7 @@ struct TypeChecker {
 
   /// Returns the generic arguments passed to `d`, which has type `t` and is being referred to by
   /// `name`, reporting diagnostics to `log`.
-  private func genericArguments(
+  private mutating func genericArguments(
     passedTo d: AnyDeclID, typed t: AnyType,
     referredToBy name: SourceRepresentable<Name>, specializedBy arguments: [CompileTimeValue],
     reportingDiagnosticsTo log: inout DiagnosticSet
@@ -4700,10 +4652,10 @@ struct TypeChecker {
     }
   }
 
-  /// Associates `parameters`, which are introduced by `name`'s declaration, to corresponding
-  /// values in `arguments` if the two arrays have the same length; returns `nil` otherwise,
-  /// reporting diagnostics to `log`.
-  private func associateGenericParameters(
+  /// Returns a table mapping the elements of `parameters`, which are introduced by `name`'s
+  /// declaration, to their corresponding values in `arguments` if the two arrays have the same
+  /// length. Otherwise, returns `nil` and reports diagnostics to `log`.
+  private mutating func associateGenericParameters(
     _ parameters: [GenericParameterDecl.ID], of name: SourceRepresentable<Name>,
     to arguments: [CompileTimeValue],
     reportingDiagnosticsTo log: inout DiagnosticSet
@@ -4713,7 +4665,11 @@ struct TypeChecker {
       result[p] = a
     }
     for p in parameters.dropFirst(arguments.count) {
-      result[p] = .type(^GenericTypeParameterType(p, ast: program.ast))
+      if isTypeKinded(p) {
+        result[p] = .type(^GenericTypeParameterType(p, ast: program.ast))
+      } else {
+        result[p] = .term(^GenericTermParameter(p, ast: program.ast))
+      }
     }
 
     if !arguments.isEmpty && (parameters.count != arguments.count) {
@@ -4942,9 +4898,9 @@ struct TypeChecker {
   /// Replaces the generic parameters in `candidate` by fresh variables if their environments don't
   /// contain `scopeOfUse`, updating `substitutions` with opened generic parameters and anchoring
   /// instantiation constraints at `cause`.
-  mutating func instantiate(
+  private mutating func instantiate(
     _ candidate: NameResolutionResult.Candidate, in scopeOfUse: AnyScopeID,
-    updating substitutions: inout [GenericParameterDecl.ID: AnyType],
+    updating substitutions: inout GenericArguments,
     anchoringInstantiationConstraintsAt cause: ConstraintOrigin
   ) -> NameResolutionResult.Candidate {
     let ctx = instantiationContext(candidate.reference, in: scopeOfUse)
@@ -4959,8 +4915,8 @@ struct TypeChecker {
         cs.formUnion(x.constraints)
         return .type(x.shape)
 
-      case .compilerKnown:
-        return v
+      case .term(let w):
+        return .term(instantiate(w, in: ctx, updating: &s))
       }
     }
 
@@ -4977,7 +4933,7 @@ struct TypeChecker {
     _ subject: AnyType, in scopeOfUse: AnyScopeID, cause: ConstraintOrigin
   ) -> InstantiatedType {
     let ctx = instantiationContext(in: scopeOfUse)
-    var substitutions: [GenericParameterDecl.ID: AnyType] = [:]
+    var substitutions = GenericArguments()
     return instantiate(subject, in: ctx, cause: cause, updating: &substitutions)
   }
 
@@ -4985,22 +4941,24 @@ struct TypeChecker {
   /// contain `contextOfUse`, assigning `cause` to instantiation constraints.
   private mutating func instantiate(
     _ subject: AnyType, in contextOfUse: InstantiationContext, cause: ConstraintOrigin,
-    updating substitutions: inout [GenericParameterDecl.ID: AnyType]
+    updating substitutions: inout GenericArguments
   ) -> InstantiatedType {
     let shape = subject.transform(mutating: &self, transform)
     return InstantiatedType(shape: shape, constraints: [])
 
     func transform(mutating me: inout Self, _ t: AnyType) -> TypeTransformAction {
       // Nothing to do if `t` doesn't contain any generic parameter.
-      if !t[.hasGenericTypeParameter] && !t[.hasGenericValueParameter] {
+      if !t[.hasSkolem] {
         return .stepOver(t)
       }
 
       switch t.base {
       case let u as AssociatedTypeType:
         return transform(mutating: &me, u)
-      case let u as GenericTypeParameterType:
+      case let u as BufferType:
         return transform(mutating: &me, u)
+      case let u as GenericTypeParameterType:
+        return .stepInto(me.instantiate(u, in: contextOfUse, updating: &substitutions))
       default:
         return .stepInto(t)
       }
@@ -5014,16 +4972,51 @@ struct TypeChecker {
     }
 
     func transform(
-      mutating me: inout Self, _ t: GenericTypeParameterType
+      mutating me: inout Self, _ t: BufferType
     ) -> TypeTransformAction {
-      if let t = substitutions[t.decl] {
-        return .stepOver(t)
-      } else if me.shouldOpen(t, in: contextOfUse) {
-        // TODO: Collect constraints
-        return .stepOver(substitutions[t.decl].setIfNil(^me.freshVariable()))
-      } else {
-        return .stepOver(substitutions[t.decl].setIfNil(^t))
-      }
+      let n = me.instantiate(t.count, in: contextOfUse, updating: &substitutions)
+      return .stepInto(^BufferType(t.element, n))
+    }
+  }
+
+  /// Replaces the generic parameters in `subject` by fresh variables if their environments don't
+  /// contain `contextOfUse`.
+  private mutating func instantiate(
+    _ subject: AnyTerm, in contextOfUse: InstantiationContext,
+    updating substitutions: inout GenericArguments
+  ) -> AnyTerm {
+    if let p = GenericTermParameter(subject) {
+      return instantiate(p, in: contextOfUse, updating: &substitutions)
+    } else {
+      return subject
+    }
+  }
+
+  /// Returns a fresh variables if `p`' environment doesn't contain `contextOfUse`.
+  private mutating func instantiate(
+    _ p: GenericTypeParameterType, in contextOfUse: InstantiationContext,
+    updating substitutions: inout GenericArguments
+  ) -> AnyType {
+    if let v = substitutions[p.decl]?.asType {
+      return v
+    } else {
+      let v = shouldOpen(p.decl, in: contextOfUse) ? ^freshVariable() : ^p
+      substitutions[p.decl] = .type(v)
+      return v
+    }
+  }
+
+  /// Returns a fresh variables if `p`' environment doesn't contain `contextOfUse`.
+  private mutating func instantiate(
+    _ p: GenericTermParameter, in contextOfUse: InstantiationContext,
+    updating substitutions: inout GenericArguments
+  ) -> AnyTerm {
+    if let v = substitutions[p.decl]?.asTerm {
+      return v
+    } else {
+      let v = shouldOpen(p.decl, in: contextOfUse) ? ^freshTermVariable() : ^p
+      substitutions[p.decl] = .term(v)
+      return v
     }
   }
 
@@ -5031,7 +5024,7 @@ struct TypeChecker {
   /// opened generic parameters and anchoring instantiation constraints at `cause`.
   private mutating func instantiate(
     constraints: inout ConstraintSet, in contextOfUse: InstantiationContext,
-    updating substitutions: inout [GenericParameterDecl.ID: AnyType],
+    updating substitutions: inout GenericArguments,
     anchoringInstantiationConstraintsAt cause: ConstraintOrigin
   ) {
     var work = ConstraintSet()
@@ -5049,10 +5042,10 @@ struct TypeChecker {
 
   /// Returns `true` iff `contextOfUse` is not contained in `p`'s environment.
   private func shouldOpen(
-    _ p: GenericTypeParameterType, in contextOfUse: InstantiationContext
+    _ p: GenericParameterDecl.ID, in contextOfUse: InstantiationContext
   ) -> Bool {
     // Generic parameters introduced by a trait can't be referenced outside of their environment.
-    let introductionScope = program[p.decl].scope
+    let introductionScope = program[p].scope
     if introductionScope.kind == TraitDecl.self {
       return false
     }
@@ -5078,6 +5071,44 @@ struct TypeChecker {
     }
   }
 
+  /// Returns `true` iff `d` represents a variable ranging over types.
+  private mutating func isTypeKinded(_ d: GenericParameterDecl.ID) -> Bool {
+    // Only parameters with exactly one bound may be value-kinded.
+    guard let bound = program[d].conformances.uniqueElement else {
+      return true
+    }
+
+    // Traits can only be qualified by name expressions.
+    var (unresolved, domain) = program.ast.splitNominalComponents(of: bound)
+    if domain != .none {
+      return false
+    }
+
+    var p: AnyType? = nil
+    while let u = unresolved.popLast() {
+      // Traits have no arguments.
+      if !program[u].arguments.isEmpty {
+        return false
+      }
+
+      let candidates = lookup(program[u].name, memberOf: p, exposedTo: program[d].scope)
+      guard let pick = candidates.uniqueElement else {
+        return false
+      }
+
+      switch pick.kind {
+      case ModuleDecl.self, NamespaceDecl.self:
+        p = uncheckedType(of: pick)
+      case TraitDecl.self:
+        return unresolved.isEmpty
+      default:
+        return false
+      }
+    }
+
+    return false
+  }
+
   // MARK: Type inference
 
   /// Returns the inferred type of `d`, which is is used as `purpose`, inserting new proof
@@ -5278,10 +5309,11 @@ struct TypeChecker {
         }
       }
 
-      let n = program[e].elements.count
-      return constrain(e, to: ^BufferType(head, .compilerKnown(n)), in: &obligations)
+      let n = ConcreteTerm(wrapping: program[e].elements.count)
+      return constrain(e, to: ^BufferType(head, ^n), in: &obligations)
     } else {
-      return constrain(e, to: ^BufferType(elementHint, .compilerKnown(0)), in: &obligations)
+      let n = ConcreteTerm(wrapping: 0)
+      return constrain(e, to: ^BufferType(elementHint, ^n), in: &obligations)
     }
   }
 
@@ -5680,21 +5712,20 @@ struct TypeChecker {
     }
 
     // The callee has a metatype and is a name expression bound to a nominal type declaration,
-    // meaning that the call is actually a sugared buffer type expression.
+    // meaning that the call is actually a sugared array or buffer type expression.
     if isBoundToNominalTypeDecl(program[e].callee, in: obligations) {
-      let n = program[e].arguments.count
-      if n != 1 {
+      let t = MetatypeType(callee)!.instance
+      switch program[e].arguments.count {
+      case 0:
+        let u = MetatypeType(of: program.ast.array(t))
+        return constrain(e, to: ^u, in: &obligations)
+      case 1:
+        let u = evalBufferTypeExpression(e, havingInferredElementType: t)
+        return constrain(e, to: ^u, in: &obligations)
+      case let n:
         report(.error(invalidBufferTypeArgumentCount: n, at: program[e].callee.site))
         return constrain(e, to: .error, in: &obligations)
       }
-
-      if let a = IntegerLiteralExpr.ID(program[e].arguments[0].value) {
-        let t = MetatypeType(callee)!.instance
-        let r = BufferType(t, .compilerKnown(Int(program[a].value)!))
-        return constrain(e, to: ^MetatypeType(of: r), in: &obligations)
-      } else {
-        UNIMPLEMENTED("arbitrary buffer type argument expression")
-      }
     }
 
     // The callee has a callable type or we need inference to determine its type. Either way,
@@ -6095,7 +6126,7 @@ struct TypeChecker {
     _ components: [NameResolutionResult.ResolvedComponent], in obligations: inout ProofObligations
   ) -> AnyType {
     var last: AnyType?
-    var substitutions: [GenericParameterDecl.ID: AnyType] = [:]
+    var substitutions = GenericArguments()
     for p in components {
       last = constrain(p.component, to: p.candidates, in: &obligations, extending: &substitutions)
     }
@@ -6109,7 +6140,7 @@ struct TypeChecker {
   private mutating func constrain(
     _ name: NameExpr.ID, to candidates: [NameResolutionResult.Candidate],
     in obligations: inout ProofObligations,
-    extending substitutions: inout [GenericParameterDecl.ID: AnyType]
+    extending substitutions: inout GenericArguments
   ) -> AnyType {
     precondition(!candidates.isEmpty)
     let site = program[name].site
@@ -6192,13 +6223,13 @@ struct TypeChecker {
     _ solution: Solution, satisfying obligations: ProofObligations,
     ignoringSharedCache ignoreSharedCache: Bool
   ) {
-    for (n, r) in solution.bindingAssumptions {
-      var s = solution.typeAssumptions.reify(r, withVariables: .kept)
+    for (n, r) in solution.bindings {
+      var s = solution.substitutions.reify(reference: r, withVariables: .kept)
 
-      let t = solution.typeAssumptions.reify(obligations.exprType[n]!, withVariables: .kept)
+      let t = solution.substitutions.reify(obligations.exprType[n]!, withVariables: .kept)
       if t[.hasVariable] || s.arguments.values.contains(where: { $0.isTypeVariable }) {
         report(.error(notEnoughContextToInferArgumentsAt: program[n].site))
-        s = solution.typeAssumptions.reify(s, withVariables: .substitutedByError)
+        s = solution.substitutions.reify(reference: s, withVariables: .substitutedByError)
       }
 
       cache.write(s, at: \.referredDecl[n], ignoringSharedCache: ignoreSharedCache)
@@ -6209,7 +6240,7 @@ struct TypeChecker {
     }
 
     for (e, t) in obligations.exprType {
-      let u = solution.typeAssumptions.reify(t, withVariables: .substitutedByError)
+      let u = solution.substitutions.reify(t, withVariables: .substitutedByError)
       cache.write(u, at: \.exprType[e], ignoringSharedCache: ignoreSharedCache)
     }
 
@@ -6217,7 +6248,7 @@ struct TypeChecker {
 
     // Note: Post-inference checks run after other choices have been committed.
     for (d, t) in obligations.declType {
-      let u = solution.typeAssumptions.reify(t, withVariables: .substitutedByError)
+      let u = solution.substitutions.reify(t, withVariables: .substitutedByError)
       cache.uncheckedType[d].updateMonotonically(.computed(u))
       checkPostInference(d, solution: solution, ignoringSharedCache: ignoreSharedCache)
     }
@@ -6248,8 +6279,8 @@ struct TypeChecker {
     var ranking: StrictPartialOrdering = .equal
     var namesInCommon = 0
 
-    for (n, lhs) in lhs.bindingAssumptions {
-      guard let rhs = rhs.bindingAssumptions[n] else { continue }
+    for (n, lhs) in lhs.bindings {
+      guard let rhs = rhs.bindings[n] else { continue }
       namesInCommon += 1
 
       // Nothing to do if both functions have the same binding.
@@ -6269,23 +6300,23 @@ struct TypeChecker {
       }
     }
 
-    if lhs.bindingAssumptions.count < rhs.bindingAssumptions.count {
-      if namesInCommon == lhs.bindingAssumptions.count {
+    if lhs.bindings.count < rhs.bindings.count {
+      if namesInCommon == lhs.bindings.count {
         return ranking != .ascending ? .descending : nil
       } else {
         return nil
       }
     }
 
-    if lhs.bindingAssumptions.count > rhs.bindingAssumptions.count {
-      if namesInCommon == rhs.bindingAssumptions.count {
+    if lhs.bindings.count > rhs.bindings.count {
+      if namesInCommon == rhs.bindings.count {
         return ranking != .descending ? .ascending : nil
       } else {
         return nil
       }
     }
 
-    return namesInCommon == lhs.bindingAssumptions.count ? ranking : nil
+    return namesInCommon == lhs.bindings.count ? ranking : nil
   }
 
   /// Compares `lhs` and `rhs` in `scopeOfUse` and returns whether one has either shadows or is
@@ -6443,6 +6474,14 @@ struct TypeChecker {
     return .init(nextFreshVariableIdentifier)
   }
 
+  /// Creates a fresh term variable.
+  ///
+  /// The returned instance is unique access concurrent type checker instances.
+  mutating func freshTermVariable() -> TermVariable {
+    defer { nextFreshVariableIdentifier += 1 }
+    return .init(nextFreshVariableIdentifier)
+  }
+
   /// Returns `true` iff `t` is known as an arrow type.
   private func isArrow(_ t: AnyType) -> Bool {
     (t.base as? CallableType)?.isArrow ?? false
diff --git a/Sources/FrontEnd/TypedProgram.swift b/Sources/FrontEnd/TypedProgram.swift
index 1a51addf8..dc223bd91 100644
--- a/Sources/FrontEnd/TypedProgram.swift
+++ b/Sources/FrontEnd/TypedProgram.swift
@@ -174,7 +174,7 @@ public struct TypedProgram {
 
   /// Returns the canonical form of `t` in `scopeOfUse`.
   public func canonical(_ t: AnyType, in scopeOfUse: AnyScopeID) -> AnyType {
-    if t[.isCanonical] { return t }
+    if t.isCanonical { return t }
     var checker = TypeChecker(asContextFor: self)
     return checker.canonical(t, in: scopeOfUse)
   }
@@ -317,7 +317,7 @@ public struct TypedProgram {
 
   /// Returns the names and types of `t`'s stored properties.
   public func storage(of t: BufferType) -> [TupleType.Element] {
-    if let w = t.count.asCompilerKnown(Int.self) {
+    if let w = ConcreteTerm(t.count)?.value as? Int {
       return Array(repeating: .init(label: nil, type: t.element), count: w)
     } else {
       return []
@@ -444,7 +444,7 @@ public struct TypedProgram {
   private func structuralConformance(
     of model: AnyType, to concept: TraitType, exposedTo scopeOfUse: AnyScopeID
   ) -> Conformance? {
-    assert(model[.isCanonical])
+    assert(model.isCanonical)
 
     switch model.base {
     case let m as BufferType:
diff --git a/Sources/FrontEnd/Types/AnyType.swift b/Sources/FrontEnd/Types/AnyType.swift
index 334e6c230..85f47756a 100644
--- a/Sources/FrontEnd/Types/AnyType.swift
+++ b/Sources/FrontEnd/Types/AnyType.swift
@@ -92,8 +92,7 @@ public struct AnyType {
   /// The `base` property can be cast back to its original type using one of the type casting
   /// operators (`as?`, `as!`, or `as`).
   public var base: any TypeProtocol {
-    get { wrapped.unwrap() }
-    set { wrapped = AnyType(newValue).wrapped }
+    wrapped.unwrap()
   }
 
   /// `self` if `!self[.hasError]`; otherwise, `nil`.
@@ -146,7 +145,7 @@ public struct AnyType {
   ///
   /// - Requires: `self` is canonical.
   public var isBuiltin: Bool {
-    precondition(self[.isCanonical])
+    precondition(isCanonical)
     return base is BuiltinType
   }
 
@@ -154,7 +153,7 @@ public struct AnyType {
   ///
   /// - Requires: `self` is canonical.
   public var isBuiltinInteger: Bool {
-    precondition(self[.isCanonical])
+    precondition(isCanonical)
     if let b = BuiltinType(self) {
       return b.isInteger
     } else {
@@ -166,7 +165,7 @@ public struct AnyType {
   ///
   /// - Requires: `self` is canonical.
   public var isBuiltinOrRawTuple: Bool {
-    precondition(self[.isCanonical])
+    precondition(isCanonical)
     if let b = TupleType(self) {
       return b.elements.allSatisfy(\.type.isBuiltin)
     } else {
@@ -289,90 +288,16 @@ public struct AnyType {
         return .stepOver(t)
 
       default:
-        return t[.hasGenericTypeParameter] ? .stepInto(t) : .stepOver(t)
+        return t[.hasSkolem] ? .stepInto(t) : .stepOver(t)
       }
     }
   }
 
-  /// Returns `true` if `self` matches `other`, calling `unify` on `unifier` to attempt unifying
-  /// syntactically different parts.
-  ///
-  /// The method visits `self` and `other` are visited "side-by-side", calling `unify` on inequal
-  /// pairs of non-structural type terms. `unify` returns `true` if these terms can be "unified",
-  /// i.e., considered equivalent under some substitution.
-  public func matches<U>(
-    _ other: AnyType, mutating unifier: inout U,
-    _ unify: (inout U, _ lhs: AnyType, _ rhs: AnyType) -> Bool
-  ) -> Bool {
-    switch (self.base, other.base) {
-    case (let lhs as BoundGenericType, let rhs as BoundGenericType):
-      if lhs.arguments.count != rhs.arguments.count { return false }
-
-      var result = lhs.base.matches(rhs.base, mutating: &unifier, unify)
-      for (a, b) in zip(lhs.arguments, rhs.arguments) {
-        switch (a.value, b.value) {
-        case (.type(let vl), .type(let vr)):
-          result = vl.matches(vr, mutating: &unifier, unify) && result
-        default:
-          result = a.value == b.value && result
-        }
-      }
-      return result
-
-    case (let lhs as MetatypeType, let rhs as MetatypeType):
-      return lhs.instance.matches(rhs.instance, mutating: &unifier, unify)
-
-    case (let lhs as TupleType, let rhs as TupleType):
-      if !lhs.labels.elementsEqual(rhs.labels) { return false }
-
-      var result = true
-      for (a, b) in zip(lhs.elements, rhs.elements) {
-        result = a.type.matches(b.type, mutating: &unifier, unify) && result
-      }
-      return result
-
-    case (let lhs as ArrowType, let rhs as ArrowType):
-      if !lhs.labels.elementsEqual(rhs.labels) { return false }
-
-      var result = true
-      for (a, b) in zip(lhs.inputs, rhs.inputs) {
-        result = a.type.matches(b.type, mutating: &unifier, unify) && result
-      }
-      result = lhs.output.matches(rhs.output, mutating: &unifier, unify) && result
-      result = lhs.environment.matches(rhs.environment, mutating: &unifier, unify) && result
-      return result
-
-    case (let lhs as MethodType, let rhs as MethodType):
-      if !lhs.labels.elementsEqual(rhs.labels) || (lhs.capabilities != rhs.capabilities) {
-        return false
-      }
-
-      var result = true
-      for (a, b) in zip(lhs.inputs, rhs.inputs) {
-        result = a.type.matches(b.type, mutating: &unifier, unify) && result
-      }
-      result = lhs.output.matches(rhs.output, mutating: &unifier, unify) && result
-      result = lhs.receiver.matches(rhs.receiver, mutating: &unifier, unify) && result
-      return result
-
-    case (let lhs as ParameterType, let rhs as ParameterType):
-      if lhs.access != rhs.access { return false }
-      return lhs.bareType.matches(rhs.bareType, mutating: &unifier, unify)
-
-    case (let lhs as RemoteType, let rhs as RemoteType):
-      if lhs.access != rhs.access { return false }
-      return lhs.bareType.matches(rhs.bareType, mutating: &unifier, unify)
-
-    default:
-      return (self == other) || unify(&unifier, self, other)
-    }
-  }
-
 }
 
 extension AnyType: TypeProtocol {
 
-  public var flags: TypeFlags { base.flags }
+  public var flags: ValueFlags { base.flags }
 
   public func transformParts<M>(
     mutating m: inout M, _ transformer: (inout M, AnyType) -> TypeTransformAction
diff --git a/Sources/FrontEnd/Types/ArrowType.swift b/Sources/FrontEnd/Types/ArrowType.swift
index bfc73c6df..e60f9f5bb 100644
--- a/Sources/FrontEnd/Types/ArrowType.swift
+++ b/Sources/FrontEnd/Types/ArrowType.swift
@@ -15,7 +15,7 @@ public struct ArrowType: TypeProtocol {
   /// The output type of the arrow.
   public let output: AnyType
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
   public init(
@@ -28,11 +28,7 @@ public struct ArrowType: TypeProtocol {
     self.environment = environment
     self.inputs = inputs
     self.output = output
-
-    var fs = environment.flags
-    for i in inputs { fs.merge(i.type.flags) }
-    fs.merge(output.flags)
-    flags = fs
+    self.flags = inputs.reduce(output.flags | environment.flags, { (fs, p) in fs | p.type.flags })
   }
 
   /// Creates the type of a function accepting `inputs` as `let` parameters and returning `output`.
diff --git a/Sources/FrontEnd/Types/AssociatedTypeType.swift b/Sources/FrontEnd/Types/AssociatedTypeType.swift
index 4f754abab..ae33b5dc5 100644
--- a/Sources/FrontEnd/Types/AssociatedTypeType.swift
+++ b/Sources/FrontEnd/Types/AssociatedTypeType.swift
@@ -15,7 +15,7 @@ public struct AssociatedTypeType: TypeProtocol {
   public let name: Incidental<String>
 
   /// A set of flags describing recursive properties.
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance denoting the associated type declared by `decl` as a member of `domain`.
   public init(_ decl: AssociatedTypeDecl.ID, domain: AnyType, ast: AST) {
@@ -28,7 +28,7 @@ public struct AssociatedTypeType: TypeProtocol {
 
     let d = AssociatedTypeType(domain)?.root ?? domain
     if !(d.isSkolem || d.base is TypeVariable) {
-      fs.remove(.isCanonical)
+      fs.insert(.hasNonCanonical)
     }
 
     self.decl = decl
diff --git a/Sources/FrontEnd/Types/AssociatedValueType.swift b/Sources/FrontEnd/Types/AssociatedValueType.swift
index 5097e9e75..5d20ff5b3 100644
--- a/Sources/FrontEnd/Types/AssociatedValueType.swift
+++ b/Sources/FrontEnd/Types/AssociatedValueType.swift
@@ -29,7 +29,7 @@ public struct AssociatedValueType: TypeProtocol {
     self.name = Incidental(ast[decl].baseName)
   }
 
-  public var flags: TypeFlags { .isCanonical }
+  public var flags: ValueFlags { .init() }
 
 }
 
diff --git a/Sources/FrontEnd/Types/BoundGenericType.swift b/Sources/FrontEnd/Types/BoundGenericType.swift
index 5e76f0fc4..7ced297ca 100644
--- a/Sources/FrontEnd/Types/BoundGenericType.swift
+++ b/Sources/FrontEnd/Types/BoundGenericType.swift
@@ -12,7 +12,7 @@ public struct BoundGenericType: TypeProtocol {
   /// The type and value arguments of the base type.
   public let arguments: Arguments
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates a bound generic type binding `base` to the given `arguments`.
   ///
@@ -22,13 +22,8 @@ public struct BoundGenericType: TypeProtocol {
     self.base = ^base
     self.arguments = arguments
 
-    var flags: TypeFlags = base.flags
-    for (_, a) in arguments {
-      if case .type(let t) = a {
-        flags.merge(t.flags)
-      } else {
-        UNIMPLEMENTED()
-      }
+    var flags = arguments.reduce(base.flags) { (fs, a) in
+      fs | a.value.flags
     }
 
     // The type isn't canonical if `base` is structural.
@@ -38,7 +33,7 @@ public struct BoundGenericType: TypeProtocol {
     case is ProductType:
       break
     default:
-      flags.remove(.isCanonical)
+      flags.insert(.hasNonCanonical)
     }
 
     self.flags = flags
diff --git a/Sources/FrontEnd/Types/BufferType.swift b/Sources/FrontEnd/Types/BufferType.swift
index 3220c8e1d..46b3464d3 100644
--- a/Sources/FrontEnd/Types/BufferType.swift
+++ b/Sources/FrontEnd/Types/BufferType.swift
@@ -5,16 +5,16 @@ public struct BufferType: TypeProtocol {
   public let element: AnyType
 
   /// The number of elements in the buffer.
-  public let count: CompileTimeValue
+  public let count: AnyTerm
 
   /// The structural properties of the type.
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
-  public init(_ element: AnyType, _ count: CompileTimeValue) {
+  public init(_ element: AnyType, _ count: AnyTerm) {
     self.element = element
     self.count = count
-    self.flags = element.flags
+    self.flags = element.flags | count.flags
   }
 
   public func transformParts<M>(
diff --git a/Sources/FrontEnd/Types/BuiltinType.swift b/Sources/FrontEnd/Types/BuiltinType.swift
index ac4404407..95581f214 100644
--- a/Sources/FrontEnd/Types/BuiltinType.swift
+++ b/Sources/FrontEnd/Types/BuiltinType.swift
@@ -41,7 +41,7 @@ public enum BuiltinType: TypeProtocol {
     }
   }
 
-  public var flags: TypeFlags { .isCanonical }
+  public var flags: ValueFlags { .init() }
 
 }
 
diff --git a/Sources/FrontEnd/Types/ConformanceLensType.swift b/Sources/FrontEnd/Types/ConformanceLensType.swift
index fed1d7249..ae311a34c 100644
--- a/Sources/FrontEnd/Types/ConformanceLensType.swift
+++ b/Sources/FrontEnd/Types/ConformanceLensType.swift
@@ -7,7 +7,7 @@ public struct ConformanceLensType: TypeProtocol {
   /// The trait through which the subject is viewed.
   public let lens: TraitType
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates a new conformance lens.
   public init(viewing subject: AnyType, through lens: TraitType) {
diff --git a/Sources/FrontEnd/Types/ErrorType.swift b/Sources/FrontEnd/Types/ErrorType.swift
index c43d3f7fb..51fde710a 100644
--- a/Sources/FrontEnd/Types/ErrorType.swift
+++ b/Sources/FrontEnd/Types/ErrorType.swift
@@ -1,7 +1,7 @@
 /// A type denoting a type checking error.
 public struct ErrorType: TypeProtocol {
 
-  public var flags: TypeFlags { [.isCanonical, .hasError] }
+  public var flags: ValueFlags { .hasError }
 
 }
 
diff --git a/Sources/FrontEnd/Types/ExistentialType.swift b/Sources/FrontEnd/Types/ExistentialType.swift
index 6e12804bf..f2f82044c 100644
--- a/Sources/FrontEnd/Types/ExistentialType.swift
+++ b/Sources/FrontEnd/Types/ExistentialType.swift
@@ -16,14 +16,14 @@ public struct ExistentialType: TypeProtocol {
     case metatype
 
     /// A set of flags describing recursive properties.
-    public var flags: TypeFlags {
+    public var flags: ValueFlags {
       switch self {
       case .traits(let ts):
-        return .init(merging: ts.map(\.flags))
+        return .init(ts.map(\.flags))
       case .generic(let t):
         return t.flags
       case .metatype:
-        return .isCanonical
+        return .init()
       }
     }
 
@@ -37,7 +37,7 @@ public struct ExistentialType: TypeProtocol {
   /// - Note: This set shall only contain equality and conformance constraints.
   public let constraints: Set<GenericConstraint>
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates a new existential type bound by the given interface and constraints.
   public init(_ interface: Interface, constraints: Set<GenericConstraint>) {
diff --git a/Sources/FrontEnd/Types/GenericTypeParameterType.swift b/Sources/FrontEnd/Types/GenericTypeParameterType.swift
index b3f1a1ab1..215d83750 100644
--- a/Sources/FrontEnd/Types/GenericTypeParameterType.swift
+++ b/Sources/FrontEnd/Types/GenericTypeParameterType.swift
@@ -20,7 +20,7 @@ public struct GenericTypeParameterType: TypeProtocol {
     self.init(ast[trait].receiver, ast: ast)
   }
 
-  public var flags: TypeFlags { [.isCanonical, .hasGenericTypeParameter] }
+  public var flags: ValueFlags { .hasSkolem }
 
 }
 
diff --git a/Sources/FrontEnd/Types/MetatypeType.swift b/Sources/FrontEnd/Types/MetatypeType.swift
index 69f07df75..b8480245a 100644
--- a/Sources/FrontEnd/Types/MetatypeType.swift
+++ b/Sources/FrontEnd/Types/MetatypeType.swift
@@ -14,7 +14,7 @@ public struct MetatypeType: TypeProtocol {
     self.instance = instance
   }
 
-  public var flags: TypeFlags { instance.flags }
+  public var flags: ValueFlags { instance.flags }
 
   public func transformParts<M>(
     mutating m: inout M, _ transformer: (inout M, AnyType) -> TypeTransformAction
diff --git a/Sources/FrontEnd/Types/MethodType.swift b/Sources/FrontEnd/Types/MethodType.swift
index 09ce71d1d..e97c97fa0 100644
--- a/Sources/FrontEnd/Types/MethodType.swift
+++ b/Sources/FrontEnd/Types/MethodType.swift
@@ -15,7 +15,7 @@ public struct MethodType: TypeProtocol {
   /// The output type of the method.
   public let output: AnyType
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
   public init(
@@ -28,11 +28,7 @@ public struct MethodType: TypeProtocol {
     self.receiver = receiver
     self.inputs = inputs
     self.output = output
-
-    var fs = receiver.flags
-    for i in inputs { fs.merge(i.type.flags) }
-    fs.merge(output.flags)
-    flags = fs
+    self.flags = inputs.reduce(output.flags | receiver.flags, { (fs, p) in fs | p.type.flags })
   }
 
   /// Returns the type of the variant `k` in this bundle.
diff --git a/Sources/FrontEnd/Types/ModuleType.swift b/Sources/FrontEnd/Types/ModuleType.swift
index f3c3f98df..3dacfe07f 100644
--- a/Sources/FrontEnd/Types/ModuleType.swift
+++ b/Sources/FrontEnd/Types/ModuleType.swift
@@ -15,7 +15,7 @@ public struct ModuleType: TypeProtocol {
     self.name = Incidental(ast[decl].baseName)
   }
 
-  public var flags: TypeFlags { .isCanonical }
+  public var flags: ValueFlags { .init() }
 
 }
 
diff --git a/Sources/FrontEnd/Types/NamespaceType.swift b/Sources/FrontEnd/Types/NamespaceType.swift
index 186f6129b..05d9f9517 100644
--- a/Sources/FrontEnd/Types/NamespaceType.swift
+++ b/Sources/FrontEnd/Types/NamespaceType.swift
@@ -15,7 +15,7 @@ public struct NamespaceType: TypeProtocol {
     self.name = Incidental(ast[decl].baseName)
   }
 
-  public var flags: TypeFlags { .isCanonical }
+  public var flags: ValueFlags { .init() }
 
 }
 
diff --git a/Sources/FrontEnd/Types/ParameterType.swift b/Sources/FrontEnd/Types/ParameterType.swift
index 08ce30ae0..0888641aa 100644
--- a/Sources/FrontEnd/Types/ParameterType.swift
+++ b/Sources/FrontEnd/Types/ParameterType.swift
@@ -12,7 +12,7 @@ public struct ParameterType: TypeProtocol {
   /// `true` iff the parameter is an autoclosure.
   public let isAutoclosure: Bool
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
   public init(_ access: AccessEffect, _ bareType: AnyType, isAutoclosure: Bool = false) {
diff --git a/Sources/FrontEnd/Types/ProductType.swift b/Sources/FrontEnd/Types/ProductType.swift
index 2d38a396a..537ceb48e 100644
--- a/Sources/FrontEnd/Types/ProductType.swift
+++ b/Sources/FrontEnd/Types/ProductType.swift
@@ -9,15 +9,14 @@ public struct ProductType: TypeProtocol {
   /// The name of the product type.
   public let name: Incidental<String>
 
-  public let flags: TypeFlags
-
   /// Creates an instance denoting the product type declared by `decl`.
   public init(_ decl: ProductTypeDecl.ID, ast: AST) {
     self.decl = decl
     self.name = Incidental(ast[decl].baseName)
-    self.flags = TypeFlags.isCanonical
   }
 
+  public var flags: ValueFlags { .init() }
+
 }
 
 extension ProductType: CustomStringConvertible {
diff --git a/Sources/FrontEnd/Types/RemoteType.swift b/Sources/FrontEnd/Types/RemoteType.swift
index 82a721320..a1379b39d 100644
--- a/Sources/FrontEnd/Types/RemoteType.swift
+++ b/Sources/FrontEnd/Types/RemoteType.swift
@@ -7,13 +7,13 @@ public struct RemoteType: TypeProtocol {
   /// The type of the projected object.
   public let bareType: AnyType
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
   public init(_ access: AccessEffect, _ bareType: AnyType) {
     self.access = access
     self.bareType = bareType
-    self.flags = bareType.flags.inserting(.hasRemoteType)
+    self.flags = bareType.flags
   }
 
   /// Creates an instance converting `t`.
diff --git a/Sources/FrontEnd/Types/SubscriptImplType.swift b/Sources/FrontEnd/Types/SubscriptImplType.swift
index 98830a9c8..00ad2ee2d 100644
--- a/Sources/FrontEnd/Types/SubscriptImplType.swift
+++ b/Sources/FrontEnd/Types/SubscriptImplType.swift
@@ -16,7 +16,7 @@ public struct SubscriptImplType: TypeProtocol {
   /// The type of the value projected by the subscript implementation.
   public let output: AnyType
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
   public init(
@@ -31,11 +31,7 @@ public struct SubscriptImplType: TypeProtocol {
     self.environment = environment
     self.inputs = inputs
     self.output = output
-
-    var fs = environment.flags
-    for i in inputs { fs.merge(i.type.flags) }
-    fs.merge(output.flags)
-    flags = fs
+    self.flags = inputs.reduce(output.flags | environment.flags, { (fs, p) in fs | p.type.flags })
   }
 
   /// Indicates whether `self` has an empty environment.
@@ -55,16 +51,6 @@ public struct SubscriptImplType: TypeProtocol {
       output: output.transform(mutating: &m, transformer))
   }
 
-  private static func makeTransformer<M>() -> (inout M, AnyType) -> TypeTransformAction {
-    { (m, t) in
-      if let type = RemoteType(t), type.access == .yielded {
-        return .stepInto(^RemoteType(.let, type.bareType))
-      } else {
-        return .stepInto(t)
-      }
-    }
-  }
-
 }
 
 extension SubscriptImplType: CustomStringConvertible {
diff --git a/Sources/FrontEnd/Types/SubscriptType.swift b/Sources/FrontEnd/Types/SubscriptType.swift
index 960a8f239..a0a68a29e 100644
--- a/Sources/FrontEnd/Types/SubscriptType.swift
+++ b/Sources/FrontEnd/Types/SubscriptType.swift
@@ -18,7 +18,7 @@ public struct SubscriptType: TypeProtocol {
   /// The type of the value projected by the subscript.
   public let output: AnyType
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance with the given properties.
   public init(
@@ -33,11 +33,7 @@ public struct SubscriptType: TypeProtocol {
     self.environment = environment
     self.inputs = inputs
     self.output = output
-
-    var fs = environment.flags
-    for i in inputs { fs.merge(i.type.flags) }
-    fs.merge(output.flags)
-    flags = fs
+    self.flags = inputs.reduce(output.flags | environment.flags, { (fs, p) in fs | p.type.flags })
   }
 
   /// Accesses the individual elements of the subscript's environment.
diff --git a/Sources/FrontEnd/Types/TraitType.swift b/Sources/FrontEnd/Types/TraitType.swift
index 0b2c1175a..c4d45933c 100644
--- a/Sources/FrontEnd/Types/TraitType.swift
+++ b/Sources/FrontEnd/Types/TraitType.swift
@@ -15,7 +15,7 @@ public struct TraitType: TypeProtocol {
     self.name = Incidental(ast[decl].baseName)
   }
 
-  public var flags: TypeFlags { .isCanonical }
+  public var flags: ValueFlags { .init() }
 
 }
 
diff --git a/Sources/FrontEnd/Types/TupleType.swift b/Sources/FrontEnd/Types/TupleType.swift
index 86db2f8b7..6b26c60a8 100644
--- a/Sources/FrontEnd/Types/TupleType.swift
+++ b/Sources/FrontEnd/Types/TupleType.swift
@@ -23,12 +23,12 @@ public struct TupleType: TypeProtocol {
   /// The elements of the tuple.
   public let elements: [Element]
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates a tuple type with a sequence of elements.
   public init<S: Sequence>(_ elements: S) where S.Element == Element {
     self.elements = Array(elements)
-    self.flags = TypeFlags(merging: self.elements.map(\.type.flags))
+    self.flags = ValueFlags(self.elements.map(\.type.flags))
   }
 
   /// Creates a tuple type with a sequence of label-type pairs.
@@ -49,10 +49,9 @@ public struct TupleType: TypeProtocol {
   public func transformParts<M>(
     mutating m: inout M, _ transformer: (inout M, AnyType) -> TypeTransformAction
   ) -> Self {
-    let newElements = elements.map(
-      { (e) -> Element in
-        .init(label: e.label, type: e.type.transform(mutating: &m, transformer))
-      })
+    let newElements = elements.map { (e) -> Element in
+      .init(label: e.label, type: e.type.transform(mutating: &m, transformer))
+    }
     return TupleType(newElements)
   }
 
diff --git a/Sources/FrontEnd/Types/TypeAliasType.swift b/Sources/FrontEnd/Types/TypeAliasType.swift
index 9650df7df..bd94c7cad 100644
--- a/Sources/FrontEnd/Types/TypeAliasType.swift
+++ b/Sources/FrontEnd/Types/TypeAliasType.swift
@@ -13,7 +13,7 @@ public struct TypeAliasType: TypeProtocol {
   public let aliasee: Incidental<AnyType>
 
   /// A set of flags describing recursive properties.
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates a type alias resolving to `aliasee` and declared by `d` in `ast`.
   public init(aliasing aliasee: AnyType, declaredBy d: TypeAliasDecl.ID, in ast: AST) {
@@ -25,7 +25,7 @@ public struct TypeAliasType: TypeProtocol {
     self.decl = decl
     self.name = Incidental(name)
     self.aliasee = Incidental(aliasee)
-    self.flags = aliasee.flags.removing(.isCanonical)
+    self.flags = aliasee.flags | .hasNonCanonical
   }
 
   /// The transitive aliasee of this alias.
diff --git a/Sources/FrontEnd/Types/TypeFlags.swift b/Sources/FrontEnd/Types/TypeFlags.swift
deleted file mode 100644
index 4c88e12d0..000000000
--- a/Sources/FrontEnd/Types/TypeFlags.swift
+++ /dev/null
@@ -1,102 +0,0 @@
-/// A set of type flags.
-public struct TypeFlags: Hashable {
-
-  /// Universal flags.
-  private var universal: UInt8
-
-  /// Existential flags.
-  private var existential: UInt8
-
-  private init(universal: UInt8, existential: UInt8) {
-    self.universal = universal
-    self.existential = existential
-  }
-
-  /// Create a new set of type flags that merges all sets in `elements`.
-  ///
-  /// - Note: `self` only contains `.isCanonical` if `elements` is empty.
-  public init<C: Collection>(merging elements: C) where C.Element == TypeFlags {
-    if let first = elements.first {
-      self = elements.dropFirst().reduce(into: first, { (a, b) in a.merge(b) })
-    } else {
-      self = .isCanonical
-    }
-  }
-
-  /// Returns whether the set contains all the specified flags.
-  public func contains(_ flags: TypeFlags) -> Bool {
-    (universal & flags.universal == flags.universal)
-      && (existential & flags.existential == flags.existential)
-  }
-
-  /// Inserts the specified flags.
-  public mutating func insert(_ flags: TypeFlags) {
-    universal = universal | flags.universal
-    existential = existential | flags.existential
-  }
-
-  /// Returns a set of flags in which `flags` have been inserted.
-  public func inserting(_ flags: TypeFlags) -> TypeFlags {
-    var newFlags = self
-    newFlags.insert(flags)
-    return newFlags
-  }
-
-  /// Removes the specified flags.
-  public mutating func remove(_ flags: TypeFlags) {
-    universal = universal & ~flags.universal
-    existential = existential & ~flags.existential
-  }
-
-  /// Returns a set of flags in which `flags` have been removed.
-  public func removing(_ flags: TypeFlags) -> TypeFlags {
-    var newFlags = self
-    newFlags.remove(flags)
-    return newFlags
-  }
-
-  /// Merge this set of flags with another set.
-  public mutating func merge(_ flags: TypeFlags) {
-    universal = universal & flags.universal
-    existential = existential | flags.existential
-  }
-
-  /// Returns a set of flags in which `flags` have been merged.
-  public func merging(_ flags: TypeFlags) -> TypeFlags {
-    var newFlags = self
-    newFlags.merge(flags)
-    return newFlags
-  }
-
-  /// The type is in canonical from.
-  public static let isCanonical = TypeFlags(universal: 1 << 0, existential: 0)
-
-  /// The type contains one or more error types.
-  public static let hasError = TypeFlags(universal: 0, existential: 1 << 0)
-
-  /// Te type contains one or more type variables.
-  public static let hasVariable = TypeFlags(universal: 0, existential: 1 << 1)
-
-  /// The type contains one or more generic type parameters.
-  public static let hasGenericTypeParameter = TypeFlags(universal: 0, existential: 1 << 2)
-
-  /// The type contains one or more generic value parameters.
-  public static let hasGenericValueParameter = TypeFlags(universal: 0, existential: 1 << 3)
-
-  /// The type contains one or more remote types.
-  public static let hasRemoteType = TypeFlags(universal: 0, existential: 1 << 4)
-
-}
-
-extension TypeFlags: ExpressibleByArrayLiteral {
-
-  public init(arrayLiteral elements: TypeFlags...) {
-    universal = 0
-    existential = 0
-    for e in elements {
-      universal |= e.universal
-      existential |= e.existential
-    }
-  }
-
-}
diff --git a/Sources/FrontEnd/Types/TypeProtocol.swift b/Sources/FrontEnd/Types/TypeProtocol.swift
index c4341c134..cd152c67a 100644
--- a/Sources/FrontEnd/Types/TypeProtocol.swift
+++ b/Sources/FrontEnd/Types/TypeProtocol.swift
@@ -3,8 +3,8 @@ import Utils
 /// A protocol describing the API of a Hylo type.
 public protocol TypeProtocol: Hashable {
 
-  /// A set of flags describing recursive properties.
-  var flags: TypeFlags { get }
+  /// Properties about the representation of `self`.
+  var flags: ValueFlags { get }
 
   /// Apply `transform(_:_:)` on `m` and the types that are part of `self`.
   func transformParts<M>(
@@ -36,7 +36,12 @@ extension TypeProtocol {
   }
 
   /// Returns whether the specified flags are raised on this type.
-  public subscript(fs: TypeFlags) -> Bool { flags.contains(fs) }
+  public subscript(fs: ValueFlags) -> Bool { flags.contains(fs) }
+
+  /// Indicates whether `self` is canonical.
+  public var isCanonical: Bool {
+    !self[.hasNonCanonical]
+  }
 
   /// Returns this type transformed with `transformer` applied to `m`.
   ///
diff --git a/Sources/FrontEnd/Types/TypeVariable.swift b/Sources/FrontEnd/Types/TypeVariable.swift
index 4150318cc..ff4ceecfd 100644
--- a/Sources/FrontEnd/Types/TypeVariable.swift
+++ b/Sources/FrontEnd/Types/TypeVariable.swift
@@ -6,14 +6,13 @@ public struct TypeVariable: TypeProtocol {
   /// The identifier of the variable.
   public let rawValue: UInt64
 
-  /// A set of flags describing recursive properties.
-  public let flags: TypeFlags = [.isCanonical, .hasVariable]
-
   /// Creates an instance with given `rawValue`.
   public init(_ rawValue: UInt64) {
     self.rawValue = rawValue
   }
 
+  public var flags: ValueFlags { .hasVariable }
+
   /// The context in which this instance was created.
   var context: UInt8 { UInt8(rawValue >> 56) }
 
diff --git a/Sources/FrontEnd/Types/UnionType.swift b/Sources/FrontEnd/Types/UnionType.swift
index a93c89b74..9034057f0 100644
--- a/Sources/FrontEnd/Types/UnionType.swift
+++ b/Sources/FrontEnd/Types/UnionType.swift
@@ -15,15 +15,15 @@ public struct UnionType: TypeProtocol {
   /// The elements of the union.
   public let elements: Elements
 
-  public let flags: TypeFlags
+  public let flags: ValueFlags
 
   /// Creates an instance type with the specified elements.
   public init<S: Sequence>(_ elements: S) where S.Element == AnyType {
     self.elements = Array(elements)
 
-    var fs = TypeFlags(merging: self.elements.map(\.flags))
+    var fs = ValueFlags(self.elements.map(\.flags))
     if self.elements.count == 1 {
-      fs.remove(.isCanonical)
+      fs.insert(.hasNonCanonical)
     }
     self.flags = fs
   }
diff --git a/Sources/FrontEnd/Types/WtinessType.swift b/Sources/FrontEnd/Types/WtinessType.swift
index 04436ff86..87d3cbd41 100644
--- a/Sources/FrontEnd/Types/WtinessType.swift
+++ b/Sources/FrontEnd/Types/WtinessType.swift
@@ -10,7 +10,7 @@ public struct WitnessType: TypeProtocol {
   }
 
   /// A set of flags describing recursive properties.
-  public var flags: TypeFlags { container.flags }
+  public var flags: ValueFlags { container.flags }
 
   /// Apply `transform(_:_:)` on `m` and the types that are part of `self`.
   public func transformParts<M>(
diff --git a/Sources/IR/FunctionID.swift b/Sources/IR/FunctionID.swift
index 9c0a2f846..aa14aa169 100644
--- a/Sources/IR/FunctionID.swift
+++ b/Sources/IR/FunctionID.swift
@@ -39,7 +39,7 @@ extension Function {
 
     /// Creates the identity of the lowered form of `s`.
     init(_ s: SynthesizedFunctionDecl) {
-      precondition(s.type[.isCanonical])
+      precondition(s.type.isCanonical)
       self.value = .synthesized(s)
     }
 
diff --git a/Sources/IR/Mangling/Mangler.swift b/Sources/IR/Mangling/Mangler.swift
index b70f7010a..8715d5a6d 100644
--- a/Sources/IR/Mangling/Mangler.swift
+++ b/Sources/IR/Mangling/Mangler.swift
@@ -431,8 +431,19 @@ struct Mangler {
     switch s {
     case .type(let t):
       append(type: t, to: &output)
-    case .compilerKnown(let v) where v is Int:
-      append(integer: v as! Int, to: &output)
+    case .term(let t):
+      append(term: t, to: &output)
+    }
+  }
+
+  /// Writes the mangled representation of `symbol` to `output`.
+  mutating func append(term symbol: AnyTerm, to output: inout Output) {
+    switch symbol.base {
+    case let t as ConcreteTerm:
+      let v = (t.value as? Int) ?? UNIMPLEMENTED()
+      append(integer: v, to: &output)
+    case let t as GenericTermParameter:
+      append(entity: t.decl, to: &output)
     default:
       UNIMPLEMENTED()
     }
@@ -453,7 +464,7 @@ struct Mangler {
     let n = Symbol.type(s)
     if appendIf(reservedOrRecorded: n, to: &output) { return }
 
-    assert(s[.isCanonical])
+    assert(s.isCanonical)
     switch s.base {
     case let t as ArrowType:
       append(arrow: t, to: &output)
@@ -524,7 +535,7 @@ struct Mangler {
   private mutating func append(buffer t: BufferType, to output: inout Output) {
     append(operator: .bufferType, to: &output)
     append(type: t.element, to: &output)
-    append(value: t.count, to: &output)
+    append(term: t.count, to: &output)
   }
 
   /// Writes the mangled representation of `z` to `output`.
diff --git a/Sources/IR/Operands/Constant/FunctionReference.swift b/Sources/IR/Operands/Constant/FunctionReference.swift
index b801f889d..ed3497671 100644
--- a/Sources/IR/Operands/Constant/FunctionReference.swift
+++ b/Sources/IR/Operands/Constant/FunctionReference.swift
@@ -21,7 +21,7 @@ public struct FunctionReference: Constant, Hashable {
 
     let v = module[f]
     let t = ArrowType(inputs: v.inputs.map({ .init(type: ^$0.type) }), output: v.output)
-    assert(t[.isCanonical])
+    assert(t.isCanonical)
 
     self.function = f
     self.type = .address(t)
diff --git a/Sources/IR/Operands/Constant/WitnessTableType.swift b/Sources/IR/Operands/Constant/WitnessTableType.swift
index 2cc66c1c9..902f4f881 100644
--- a/Sources/IR/Operands/Constant/WitnessTableType.swift
+++ b/Sources/IR/Operands/Constant/WitnessTableType.swift
@@ -6,7 +6,7 @@ public struct WitnessTableType: TypeProtocol, CustomStringConvertible {
   /// Creates an instance.
   public init() {}
 
-  public var flags: TypeFlags { .isCanonical }
+  public var flags: ValueFlags { .init() }
 
   public var description: String { "WitnessTable" }
 
diff --git a/Sources/IR/Operands/Instruction/AllocStack.swift b/Sources/IR/Operands/Instruction/AllocStack.swift
index e83cecc8c..681b7096d 100644
--- a/Sources/IR/Operands/Instruction/AllocStack.swift
+++ b/Sources/IR/Operands/Instruction/AllocStack.swift
@@ -39,7 +39,7 @@ extension Module {
   ///
   /// - Requires: `t` is canonical.
   func makeAllocStack(_ t: AnyType, at site: SourceRange) -> AllocStack {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
     return .init(allocatedType: t, site: site)
   }
 
diff --git a/Sources/IR/Operands/Instruction/OpenUnion.swift b/Sources/IR/Operands/Instruction/OpenUnion.swift
index 7a1d4eb64..d4692596f 100644
--- a/Sources/IR/Operands/Instruction/OpenUnion.swift
+++ b/Sources/IR/Operands/Instruction/OpenUnion.swift
@@ -75,7 +75,7 @@ extension Module {
     at site: SourceRange
   ) -> OpenUnion {
     precondition(type(of: container).isAddress)
-    precondition(payload[.isCanonical])
+    precondition(payload.isCanonical)
     return .init(
       container: container,
       payloadType: payload,
diff --git a/Sources/IR/StaticStorage.swift b/Sources/IR/StaticStorage.swift
index b000e5227..05289b371 100644
--- a/Sources/IR/StaticStorage.swift
+++ b/Sources/IR/StaticStorage.swift
@@ -17,7 +17,7 @@ public struct StaticStorage {
   public init(
     _ t: AnyType, identifiedBy id: AnyDeclID, initializedWith initializer: Function.ID
   ) {
-    precondition(t[.isCanonical])
+    precondition(t.isCanonical)
     self.id = id
     self.pointee = t
     self.initializer = initializer
diff --git a/Sources/IR/Type.swift b/Sources/IR/Type.swift
index e88b817ee..015de1838 100644
--- a/Sources/IR/Type.swift
+++ b/Sources/IR/Type.swift
@@ -16,7 +16,7 @@ public struct Type: Hashable {
   ///
   /// - Requires: `ast` must be canonical.
   public init<T: TypeProtocol>(ast: T, isAddress: Bool) {
-    precondition(ast[.isCanonical], "source type is not canonical")
+    precondition(ast.isCanonical, "source type is not canonical")
     self.ast = ^ast
     self.isAddress = isAddress
   }
diff --git a/StandardLibrary/Sources/Array.hylo b/StandardLibrary/Sources/Array.hylo
index 9342d417f..b778503fd 100644
--- a/StandardLibrary/Sources/Array.hylo
+++ b/StandardLibrary/Sources/Array.hylo
@@ -11,6 +11,22 @@ public type Array<Element: SemiRegular>: SemiRegular {
     &storage = .new()
   }
 
+  /// Creates an array with the given `elements`.
+  public init<n: Int>(_ elements: sink Element[n]) {
+    &storage = .new()
+    &reserve_capacity(n)
+
+    // Note: lifetime of `p` is guaranteed by the use of `elements` after the loop.
+    let p = PointerToMutable<Element>(type_punning: mutable_pointer[to: &elements])
+    var i = 0
+    while i < n {
+      &append(p.advance(by: i).unsafe_pointee())
+      &i += 1
+    }
+
+    Builtin.mark_uninitialized(elements)
+  }
+
   /// Creates an array whose contents are the results, of calling `initialize` with the values
   /// `0 ..< count`, in order.
   ///
diff --git a/Tests/HyloTests/TestCases/TypeChecking/BufferExpr.hylo b/Tests/HyloTests/TestCases/TypeChecking/BufferExpr.hylo
new file mode 100644
index 000000000..1ba4ad4d7
--- /dev/null
+++ b/Tests/HyloTests/TestCases/TypeChecking/BufferExpr.hylo
@@ -0,0 +1,5 @@
+//- typeCheck expecting: .failure
+
+public fun main() {
+  var x: Int[true] //! diagnostic expected type 'Int' but found 'Bool'
+}
diff --git a/Tests/HyloTests/TestCases/TypeChecking/GenericParameters.hylo b/Tests/HyloTests/TestCases/TypeChecking/GenericParameters.hylo
index 58f259fca..335808016 100644
--- a/Tests/HyloTests/TestCases/TypeChecking/GenericParameters.hylo
+++ b/Tests/HyloTests/TestCases/TypeChecking/GenericParameters.hylo
@@ -3,7 +3,8 @@
 //! @+1 diagnostic expected type but 'v' denotes a value
 fun f0<X, v: Int>(_ x: X, _ y: v) {}
 
-//! @+1 diagnostic only one annotation is allowed on generic value parameter declarations
+//! @+2 diagnostic conformance to non-trait type 'Float64'
+//! @+1 diagnostic conformance to non-trait type 'Int'
 fun f1<X, v: Int & Float64>(_ x: X) {}
 
 //! @+1 diagnostic conformance to non-trait type 'Float64'
diff --git a/Tests/HyloTests/TestCases/TypeChecking/TypeExpressionSugars.hylo b/Tests/HyloTests/TestCases/TypeChecking/TypeExpressionSugars.hylo
new file mode 100644
index 000000000..f6f655f0b
--- /dev/null
+++ b/Tests/HyloTests/TestCases/TypeChecking/TypeExpressionSugars.hylo
@@ -0,0 +1,11 @@
+//- typeCheck expecting: .failure
+
+public fun main() {
+  // Buffer type.
+  let x0: Int[2] = [1, 2]
+  // Array type.
+  let x1: Int[] = Array()
+
+  //! @+1 diagnostic buffer type requires exactly one generic argument (found 2)
+  let x2: Int[1, 2]
+}
diff --git a/Tests/LibraryTests/TestCases/ArrayTests.hylo b/Tests/LibraryTests/TestCases/ArrayTests.hylo
index b6786ee7c..0405d5231 100644
--- a/Tests/LibraryTests/TestCases/ArrayTests.hylo
+++ b/Tests/LibraryTests/TestCases/ArrayTests.hylo
@@ -5,6 +5,13 @@ fun test_init_empty() {
   precondition(d.count() == 0)
 }
 
+fun test_init_with_buffer() {
+  let d = Array([21, 42])
+  precondition(d.count() == 2)
+  precondition(d[0] == 21)
+  precondition(d[1] == 42)
+}
+
 fun test_init_with_lambda() {
   let d = Array<Int>(count: 10, initialized_with: fun (_ i) { i * 2 })
   precondition(d.count() == 10)
@@ -144,6 +151,7 @@ fun test_array_is_copyable() {
 
 public fun main() {
   test_init_empty()
+  test_init_with_buffer()
   test_init_with_lambda()
   test_append()
   test_insert_at()