# STLC Core Surface


This example builds a small source language over the existing HOAS
checker. The surface adds syntax and source positions; the kernel still
owns typing and normalization.

## Define the surface

`defineSurface` maps each source constructor to a HOAS expression.
The core STLC fragment has Pi types, lambdas, annotations, and
applications.

```nix
surface = S.defineSurface {
  name = "STLC";
  description = "Small typed lambda-calculus surface example.";
  constructors = {
    lam = {
      tag = "stlc.lam";
      handler = { depth, h, lower, hoas, ... }:
        lower depth (hoas.lam h.name h.domain h.body);
    };

    app = {
      tag = "stlc.app";
      handler = { depth, h, lower, hoas, ... }:
        lower depth (hoas.app h.fn h.arg);
    };
  };
};
```

## Smart constructors

Users construct source terms with small Nix functions. The values are
surface nodes until `check` elaborates them into HOAS.

```nix
arrow = domain: codomain: pi "_" domain (_: codomain);
lam = name: domain: body: surface.mk "lam" { inherit name domain body; };
ann = term: type: surface.mk "ann" { inherit term type; };
app = fn: arg: surface.mk "app" { inherit fn arg; };

idNatTy = arrow H.nat H.nat;
idNat = lam "x" H.nat (x: var x);
idNatAnn = ann idNat idNatTy;
```

## Expected-type holes

`holeLam` omits a lambda domain. The handler reads the expected type,
solves a surface implicit metavariable with the Pi domain, and then
elaborates an ordinary typed lambda.

```nix
holeLambdaFromExpected = { context, name, body, hoas ? H }:
  let
    implicit = context.implicitMeta {
      type = { ctx = C.emptyCtx; ty = V.vU V.vLevelZero; };
      label = "stlc.lambda-domain";
    };
    expectedType = context.expectedType or null;
    domain = if expectedType == null then null else piDomain expectedType;
  in
  if expectedType == null
  then S.unsolvedImplicitError { metas = [{ id = implicit.id; }]; }
  else if domain == null
  then expectedFunctionError context
  else {
    term = hoas.lam name domain body;
    solvedState = M.solveMeta implicit.id (E.eval [ ] (hoas.elab domain)) implicit.state;
  };
```

## Implicit insertion

Plicity-style implicit binders are carried as sidecars on Pi and
lambda nodes. During application, the elaborator inserts fresh metas
for implicit arguments and solves them from explicit arguments or
the expected residual type.

```nix
polyIdTy = implicitPi "A" universe0 (A: arrow A A);
polyId = implicitLam "A" universe0 (A: lam "x" A (x: var x));
polyIdAnn = ann polyId polyIdTy;

stlcPolyIdAppliedSolvesImplicit =
  let
    position = { path = [ "poly" "id" "zero" ]; };
    r = check (app polyIdAnn H.zero) H.nat position;
  in
  !(r ? error) && r.tag == "app";
```