     }
   }
 
+  private func formCompleteApply(_ n : FullyQualifiedName, _ args: [Expr]) -> Expr {
+    let head: ApplyHead
+    if self.isBoundVariable(n.name) {
+      head = .variable(n.name)
+    } else if let (fqn, info) = self.lookupLocalName(n.name) {
+      switch info {
+      case .constructor(_, _):
+        return .constructor(fqn, args)
+      default:
+        head = .definition(fqn)
+      }
+    } else if self.lookupFullyQualifiedName(n) != nil {
+      head = .definition(n)
+    } else {
+      // If it's not a definition or a local variable, it's undefined.
+      // Recover by introducing a local variable binding anyways.
+      self.engine.diagnose(.undeclaredIdentifier(n), node: n.node)
+      head = .variable(n.name)
+    }
+
+    return .apply(head, args.map(Elimination.apply))
+  }
+
   /// Scope check and validate an expression.
   private func scopeCheckExpr(_ syntax: ExprSyntax) -> Expr {
     switch syntax {
     case let syntax as NamedBasicExprSyntax:
       let n = QualifiedName(ast: syntax.name)
-      let head: ApplyHead
-      if self.isBoundVariable(n.name) {
-        head = .variable(n.name)
-      } else if let nameInfo = self.lookupFullyQualifiedName(n) {
-        guard case .definition(_) = nameInfo else {
-          return .constructor(n, [])
-        }
-        head = .definition(n)
-      } else if let (fqn, nameInfo) = self.lookupLocalName(n.name) {
-        guard case .definition(_) = nameInfo else {
-          return .constructor(fqn, [])
-        }
-        head = .definition(fqn)
-      } else {
-        // If it's not a definition or a local variable, it's undefined.
-        // Recover by introducing a local variable binding anyways.
-        self.engine.diagnose(.undeclaredIdentifier(n), node: n.node)
-        head = .variable(n.name)
-      }
-      return .apply(head, [])
+      return formCompleteApply(n, [])
     case _ as TypeBasicExprSyntax:
       return .type
     case _ as UnderscoreExprSyntax:
       return .meta
     case let syntax as ParenthesizedExprSyntax:
-      return self.scopeCheckExpr(syntax.expr)
+      return self.underScope { _ in
+        return self.scopeCheckExpr(syntax.expr)
+      }
     case let syntax as LambdaExprSyntax:
       return self.underScope { _ in
         let bindings = self.scopeCheckBindingList(syntax.bindingList)

          args.append(elim)
        }

        let head: ApplyHead
        if self.isBoundVariable(n.name) {
          head = .variable(n.name)
        } else if let (fqn, _) = self.lookupLocalName(n.name) {
          head = .definition(fqn)
        } else if self.lookupFullyQualifiedName(n) != nil {
          head = .definition(n)
        } else {
          // If it's not a definition or a local variable, it's undefined.
          // Recover by introducing a local variable binding anyways.
          self.engine.diagnose(.undeclaredIdentifier(n), node: n.node)
          head = .variable(n.name)
        }

        return .apply(head, args.map(Elimination.apply))

      default:
        fatalError("Cannot yet handle this case")
      }

        args.append(elim)
      }

      return formCompleteApply(n, args)
    case let syntax as ApplicationExprSyntax:
      guard syntax.exprs.count > 1 else {
        return self.scopeCheckExpr(syntax.exprs[0])
