# STLC Refinements and Diagnostics


The refinement surface gives a source-language spelling to the HOAS
refinement carrier and preserves diagnostic intent. A missing annotation,
an ordinary type mismatch, and a failed refinement proof are distinct
failures.

## Refinement values

A refinement type is represented as a dependent pair whose second
component is a positive decision. The surface `refine` form packages
the witness and proof into that carrier.

```nix
atLeastOneNat =
  refinement "AtLeastOne" H.nat (n: H.le one n);

oneLeOne = H.leSS H.leZ;
oneAtLeastOne = refine atLeastOneNat one oneLeOne;

stlcRefinementValueChecks =
  let
    r = check oneAtLeastOne atLeastOneNat
      { path = [ "refinement" "value" ]; };
  in
  !(r ? error) && r.tag == "pair";
```

## Refinement failure

If the witness and proof do not match, the surface reports a
refinement-specific diagnostic instead of exposing the raw Sigma
mismatch as the main error.

```nix
zeroWithOneProof = refine atLeastOneNat H.zero oneLeOne;

stlcBadRefinementHasSurfaceDiagnostic =
  let
    position = { path = [ "bad" "refinement" ]; };
    r = check zeroWithOneProof atLeastOneNat position;
  in
  (r ? error)
  && (r.kind or null) == "stlc.refinement-failure"
  && (r.position or null) == position;
```

## Diagnostic classes

The examples keep three failure classes separate: unsolved implicit
information, ordinary checker errors, and refinement failures. That
gives editors and command-line tools enough structure to suggest the
right repair.

```nix
stlcDiagnosticUnsolvedImplicitIsDistinct =
  let
    position = { path = [ "diagnostic" "implicit" ]; };
    r = elaborate (Core.holeLam "x" (x: Core.var x)) position;
  in
  (r ? error)
  && (r.kind or null) == "surface.unsolved-implicit"
  && (r.position or null) == position;

stlcDiagnosticRefinementFailureIsDistinct =
  let
    position = { path = [ "diagnostic" "refinement" ]; };
    r = check zeroWithOneProof atLeastOneNat position;
  in
  (r ? error)
  && (r.kind or null) == "stlc.refinement-failure";
```