Add typed holes for partial program generation.

Motivation

The Hazel typed-holes paper (OOPSLA 2024) showed that exposing type context for incomplete program fragments dramatically improves LLM completion quality. A typed hole is a placeholder expression ? with a known expected type that a tool or LLM can fill in.

Proposed syntax

fn example(@Int -> @Int)
  requires(@Int.0 > 0)
  ensures(@Int.result > @Int.0)
{
  ?   -- hole: expected type Int, context: @Int.0 : Int (> 0)
}

Compiler behavior

• vera check reports each hole with its expected type, available bindings, and active contracts
• vera check --json includes holes in structured output for agent consumption
• Programs with holes type-check (reporting holes as warnings) but cannot compile

Dependencies

• None (grammar + checker change)