 }
 
 extension TypeChecker {
+  /// Evaluates a TT term.
+  ///
+  /// This strategy is the most drastic form of evaluation and also the most
+  /// expensive.  In most cases WHNF suffices.
+  func toNormalForm(_ t: TT) -> TT {
+    let normTerm = self.toWeakHeadNormalForm(t).ignoreBlocking
+    switch normTerm {
+    case .refl:
+      return .refl
+    case .type:
+      return .type
+    case let .lambda(body):
+      return .lambda(self.toNormalForm(body))
+    case let .pi(dom, cod):
+      return .pi(self.toNormalForm(dom), self.toNormalForm(cod))
+    case let .equal(A, x, y):
+      return .equal(self.toNormalForm(A),
+                    self.toNormalForm(x), self.toNormalForm(y))
+    case let .constructor(dataCon, args):
+      return .constructor(dataCon.mapArgs(self.toNormalForm),
+                          args.map(self.toNormalForm))
+    case let .apply(h, args):
+      let newArgs = args.map({ (a) -> Elim<TT> in
+        switch a {
+        case let .apply(tt):
+          return .apply(self.toNormalForm(tt))
+        case .project(_):
+          return a
+        }
+      })
+      switch h {
+      case .meta(_):
+        return TT.apply(h, newArgs)
+      case .variable(_):
+        return TT.apply(h, newArgs)
+      case let .definition(def):
+        return TT.apply(.definition(def.mapArgs(self.toNormalForm)), newArgs)
+      }
+    }
+  }
+
   /// Reduces a TT term to head normal form, and produces a representation of
   /// any new problems encountered during the reduction.
   ///

    default:
      return .notBlocked(t)
    }
  }

  /// Apply a list of eliminations to a term.

      let clauses = inv.ignoreInvertibility.map { clause in
        return self.forceInstantiate(clause, name.args)
      }
      return self.eliminateClauses(name, clauses, es)

    // If we have an application with an unknown callee, try to
    // eagerly solve for it if possible.
