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.

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.

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.

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";