Improve error messages for common typo and inference-failure cases

[hierophantos]

Summary

Several elaborator error messages produce diagnostics that are technically accurate but unhelpful for users — surfacing internal-feeling errors without guidance toward a fix. This issue tracks specific cases identified during PR review and language-exploration work for improvement, with concrete suggestions for each.

Specific cases identified

Case 1: "Expression is not a valid type" with hole types

Reproducer:

;; Typo or missing spec → defn elaborates with hole types
defn constantly [x] (fn [u : Unit] x)
def my-3 := [constantly 3]
;; Error: Expression is not a valid type / Expression: Unit -> _

What happens: defn has no matching spec, elaborates with _ -> Unit -> _. Partial application infers first hole but not second. System reports the partially-resolved type with unsolved hole.

Current message: Expression is not a valid type / Expression: Unit -> _

Suggested message:

Could not fully infer type at: [constantly 3]
  Inferred so far: Unit -> ?A
  Where ?A is unconstrained.
  
  Suggestions:
  - Add a type annotation: def my-3 : <Unit -> Int> := ...
  - Provide a `spec` for `constantly` so the elaborator can resolve
  - Apply all arguments inline: [constantly 3 unit]

Case 2: "fn: all parameters except body must be bare symbols or a binder (x : T)" for empty params

Reproducer:

def f := (fn [] 42)
;; Error: fn: all parameters except body must be bare symbols or a binder (x : T)

What happens: 0-arg lambdas don't fit the Pi-type structure (no binder to bind). The parser rejects empty parameter lists.

Current message: technically accurate but doesn't tell the user what to do

Suggested message:

fn: parameters cannot be empty in this dependent type system.
  
  "Function of no arguments" is encoded as Unit -> A:
    (fn [u : Unit] body)
  
  Alternatively, in pure code, (fn [] x) ≡ x — just bind x directly.
  
  See <link to docs section on Unit-encoded thunks>

Case 3: "Multiplicity violation" surfacing for kind-level mult mismatch

Reproducer:

spec scale-vec Rat [List Rat] -> [List Rat]
defn scale-vec [s xs]
  [map (fn [x : Rat] [rat* s x]) xs]
;; Error: Multiplicity violation [fn [x <Rat>] ...]

What happens: List's kind is Pi(m0, Type, Type); map's {C : Type → Type} elaborates to Pi(mw, Type, Type). The kind-level mult mismatch surfaces as a value-level "Multiplicity violation" — confusing because the closure looks fine.

Current message: surfaces at the fn body, blames the closure

Suggested message:

Type-constructor kind mismatch in implicit position:
  List has kind: Pi(m0, Type, Type)   ;; erased type arg
  map expects: Pi(mw, Type, Type)     ;; the `->` defaults to mw
  
  This is the kind-level "m0 vs mw" mismatch (eigentrust pitfall #2).
  The fix is in #23 (multiplicity subtyping); for now, workaround:
  <suggest workaround when known>

(Pending #23 / multiplicity subtyping work — once that lands, the diagnostic should distinguish the kind-level case from genuine value-level mult violations.)

Case 4: "Unbound variable: NAME" cascading from upstream errors

Reproducer: any failing def NAME := ... produces "Unbound variable: NAME" at every downstream site.

What happens: the def silently fails (returns error, doesn't bind), then every reference reports "Unbound variable" — the actual error is upstream.

Current message: just "Unbound variable: NAME" — doesn't explain why NAME isn't bound

Suggested message:

Unbound variable: my-3
  
  This name was attempted to be defined at line N but the def failed:
    def my-3 := ...
    ↑ failed with: <upstream error>
  
  Fix the def to make my-3 available.

Or, better: have the elaborator track failed-def names and report a single "definition NAME failed; downstream uses suppressed" rather than cascading.

Case 5: Typo detection in spec/defn pairs

Reproducer:

spec consntantly Int -> Int   ;; typo
defn constantly [x] x          ;; no matching spec

What happens: spec doesn't match any defn, defn has no spec, both proceed with hole types and produce confusing downstream errors.

Suggested behavior:

defn `constantly` has no matching spec.
  Did you mean `consntantly` (declared at line N)? Edit distance: 2.
  
  Without a spec, the type will be inferred from usage with hole defaults.

Scope

This issue tracks UX improvements to error messages. Implementation can land incrementally — each case can be addressed independently.

• Add user-facing diagnostic messages with suggestions
• Add typo-detection (Levenshtein distance) for unmatched spec/defn pairs
• Improve cascading-error suppression (don't report "Unbound variable" for names whose def failed; report the def failure once)
• Add documentation links from common errors to relevant guide sections
• Test that suggested messages render correctly for each reproducer

Out of scope

• Underlying type-system changes (most of these are orthogonal to language semantics)
• Internationalization of error messages
• IDE/LSP integration (separate)

Why this matters

Error messages are the user's primary feedback loop. A concise, actionable diagnostic costs us a small amount of code and saves users debugging time, especially during their first encounter with dependent typing concepts (Unit, multiplicity, hole types).

The current language-design exploration (PRs from external contributors, internal experimentation) repeatedly surfaces these errors without clear paths forward. Improving the diagnostics directly improves contributor and learner experience.

References

• Cases 1-2 surfaced via constantly discussion 2026-04-26
• Case 3 surfaced via PR unify: lenient {m0, mw} compatibility (eigentrust pitfall #2) #17 (eigentrust pitfall Add EigenTrust reputation algorithm: implementation, tests, benchmark #2)
• Case 4 surfaced via PR Multi-line let body wrapping in expand-let (eigentrust pitfall #5) #11 / Pre-register top-level defn types for mutual recursion (eigentrust pitfall #4) #14 reviews and various reproducer attempts
• Case 5 surfaced via testing 2026-04-26 (typo consntantly)
• Related: Multiplicity subtyping: implement m0 <: mw (and broader subtyping infrastructure) #23 (multiplicity subtyping — would change the surface of Case 3)
• Related: #25 (let-generalization gap — would change the surface of Case 1)

Priority

Medium. Compounds across all language features. Each case improved is a small UX win that's permanently visible.

[hierophantos]

Adding Case 6: Parser crash on misindented clause body

Surfaced 2026-04-26 while exploring the multi-line clause body convention (now codified in .claude/rules/prologos-syntax.md § "Pattern matching and dispatch").

Reproducer

defn foo [n xs]
  | n nil -> "a"
  | n [cons h t] ->
  match xs            ;; ← body at SAME indent as `|` (should be deeper)
    | nil -> "b"

What happens

Hard internal Racket error:

given: '()
context...:
 racket/prologos/parser.rkt:3688:0: body of top-level
 racket/private/map.rkt:40:19: loop
 racket/prologos/driver.rkt:1707:0: process-file-inner

This is an internal exception, not a structured prologos-error. The user sees a Racket stack trace into our parser internals, which is unhelpful and exposes implementation details.

Suggested message

Layout error in clause body at <line, column>:
  The body of `| n [cons h t] -> ...` must be indented FURTHER than the `|` column.
  Currently `match xs` is at indent N (same as `|`), which causes the parser
  to treat it as a sibling clause start, but no `|` precedes it.
  
  Fix: indent the body line(s) past the `|` column. See:
  <link to prologos-syntax.md § Pattern matching and dispatch>

Implementation note

Likely localized to the parser's clause-handling code (around parser.rkt:3688 per the stack trace). The fix is twofold:

1. Detect the "body absent / improperly indented" condition early and emit a structured prologos-error (not an internal exception)
2. Surface the indent expectation in the diagnostic message

This is the same diagnostic-quality issue as Cases 1, 2, 4 — the underlying parser/elaborator error is correct, but the user-facing surface is unhelpful. Worth handling alongside the others.

Cross-references

• The successful (correctly-indented) form is verified working as of 2026-04-26 — the form was always supported, just lacked diagnostic for the misindented variant.
• Style convention codified in .claude/rules/prologos-syntax.md § "Pattern matching and dispatch" (commit pending).

[hierophantos]

Adding Cases 7 and 8

Surfaced 2026-04-26 during my-second language exploration with Prolog-style head-tail patterns.

Case 7: Malformed list patterns crash compile-match-tree

Reproducer:

ns repro
spec what-am-i {A : Type} [List A] -> Bool
defn what-am-i [xs]
  | [a nil]   -> true
  | _         -> false

what-am-i '[1]

What happens: hard internal Racket error from the pattern compiler:

given: '()
context...:
 racket/prologos/macros.rkt:9191:0: compile-match-tree
 [repeats 1 more time]
 racket/prologos/macros.rkt:9498:0: compile-pattern-group
 racket/prologos/macros.rkt:9572:0: expand-defn-multi
 racket/prologos/driver.rkt:449:0: process-command
 racket/prologos/driver.rkt:1707:0: process-file-inner

The user's intent: probably "match a 1-element list" (interpreting [a nil] as [a | nil]).

The actual interpretation (per the bracket-list-literal pattern syntax): would be a 2-element list where the first element is bound to a and the second element must equal the value nil. That's a valid pattern shape — but the pattern compiler crashes rather than handling it.

Either case (genuine intent or compiler bug), internal crash is wrong UX.

Suggested message (if the pattern is intended as 2-element-with-nil-second):

Pattern `[a nil]` is a 2-element list pattern.
  Position 1: variable `a` (binds the first element)
  Position 2: literal `nil` (the second element must equal nil — the empty list)

  This pattern matches lists of exactly 2 elements where the second element
  is the empty list (e.g., '[1 nil] or '[42 nil]).

  Did you mean `[a | nil]`? That matches a 1-element list (head a, tail nil).

Suggested message (if the pattern is genuinely malformed):

Pattern `[a nil]` not yet supported by the pattern compiler.
  For a 1-element list pattern, use `[a | nil]`.
  For a 2-element list, use `[a b]` or `[a b | _]`.

The right fix depends on whether [a nil] should be a valid pattern. If yes, fix the compiler. If no, surface a parse-time error.

Case 8: ??__match-fail as user-facing output for non-exhaustive matches

Reproducer:

spec my-second {A : Type} [List A] -> [Option A]
defn my-second [xs]
  | nil       -> none
  | [a b | _] -> some b
  ;; missing: 1-element list case

my-second '[1]

Output:

??__match-fail : [Option A]

The match falls through (no pattern matches a 1-element list). The runtime returns the sentinel value ??__match-fail rather than raising a structured error.

Issues:

1. Looks like a value, not an error — confusing in the REPL
2. Doesn't say what went wrong (just the sentinel)
3. Doesn't show what input failed to match
4. Doesn't suggest adding a fallback clause
5. Type prints as the expected return type ([Option A]), making the sentinel look like a valid value

Suggested behavior — two layers:

Compile-time: exhaustiveness checking. When defn has clauses but doesn't cover all inhabitants of the input type, warn (or error):

Warning: defn `my-second` does not exhaustively match its input type.
  Input type: [List A]
  Covered patterns: nil, [a b | _]
  Missing: [a | nil]    ;; 1-element list

  Add a clause for the missing case, or add `| _ -> ...` as a fallback.

Runtime (when exhaustiveness check is unavailable or disabled): structured error:

match-failure-error
  Function: my-second
  Input value: '[1]
  Inferred type: [List Int]
  No pattern matched. Patterns tried:
    | nil       (matched: 0-element list)
    | [a b | _] (matched: 2+-element list)

Compile-time exhaustiveness is the higher-impact fix; runtime structured error is the floor.

Scope additions to this issue

• Case 6 (already drafted above): parser crash on misindented clause body
• Case 7: malformed list patterns crash compile-match-tree
• Case 8: ??__match-fail sentinel as user-facing output, plus exhaustiveness checking

All three are surface-of-error-message work. Case 8 has the additional dimension of a compile-time check (exhaustiveness) that would prevent the runtime error class entirely — that's a real language feature, not just a diagnostic improvement, but it lives naturally in this issue's scope as the structural fix for the symptom Case 8 describes.

Cross-references

• Pattern-syntax asymmetry filed as separate issue (the [a] doesn't match '[1] case)
• Both surfaced from the same exploration thread 2026-04-26