On this page · 19 sections

OCaml/Hindley-Milner Failure Modes

OCaml-style HM is the right inspiration: fast, local-feeling, strong on ordinary code. Failures cluster where the "compiler just knows" illusion breaks — distant errors, value restriction, clever public surfaces, and advanced-feature stress. Keep the joy; learn the failure points. Inference policy lives in 02-type-inference.md; functions in book/003-Functions.shp.

Pain ranking (practical)

Rank	Failure	Ship response
1	Non-local type errors	Origin + conflict spans; optional inference trace
2	Value restriction / weak types	Keep soundness; no `_weakN` in UX; name the rule; suggest annotation
3	Clever inferred public APIs	Inference in `.shp`, including parameters; stabilize with `.shc`, not by restating types on the implementation
4	No ad-hoc overloading	Nominal canonical behaviors + explicit module params; preserve principal types
5	Labels / optionals weaken inference	Required for Ship; explicit rules (see `book/003-Functions.shp`)
6	Product / constructor ambiguity	Unique/nearest/tie; hard error on collision (`02-type-inference.md`)
7	Module abstraction cliff	Name the boundary; `.shc` makes opacity obvious
8	Feature composition	Small core first; gate advanced features with diagnostics
9	GADTs	Advanced; require annotations; name existentials
10	Open variants / rows	Closed default; Ship-native row diagnostics
11	Higher-rank not inferred	Explicit only
12	Polymorphic recursion	Explicit generic on binding
13	Let- vs lambda-polymorphism	Diagnose "parameter would need to be polymorphic"
14	Optional + partial application	Uncurried; no OCaml erasure (see `book/003-Functions.shp`)
15	Weak types at module boundary	"Would be exported"; suggest binding annotation
16	Relaxed VR needs variance	Infer variance; diagnose when abstraction hid it

Failure modes

One OCaml shape each; Ship lesson only.

1. Non-local errors

let stringify_all xs = List.map (fun x -> x + 1) xs
let names = stringify_all ["teej"; "ship"]
(* error often at the string list; cause is x + 1 *)

Ship: show origin and conflict; explain why the expected type was expected; optional verbose constraint trail.

2. Let-polymorphism ≠ lambda-polymorphism

let id x = x
let both = (id 1, id "ship")          (* ok *)
let use_id id = (id 1, id "ship")     (* fails — monomorphic param *)

Ship: diagnose higher-rank need; keep rank-n explicit.

3. Value restriction

let store = ref None   (* '_weak1 option ref, not 'a option ref *)

Applications (not syntactic values) also weaken; eta-expand or annotate.

Ship: keep the soundness rule; say "not generalized because mutable / not a value"; suggest annotation or eta-expansion; never lead with _weakN.

4. Weak types cannot escape modules

let option_ref = ref None
(* compiled module: type variables that cannot be generalized *)

Ship: "unresolved weak type would be exported"; point at the binding; suggest annotation.

5. Relaxed value restriction / variance

let empty = List.empty ()   (* 'a list when covariant *)
(* abstract sig without +'a t loses the polymorphism *)

Ship: infer variance where possible; document when it matters; diagnose "abstraction hid covariance needed for generalization."

6. Polymorphic recursion

let rec depth = function
  | List _ -> 1
  | Nested n -> 1 + depth n   (* needs 'a. 'a nested -> int *)

Ship: require explicit polymorphic annotation; say "recursive call uses a different instantiation."

7. Higher-rank

let average f x y = (f x + f y) / 2
(* infers ('a -> int) -> 'a -> 'a -> int, not forall in the argument *)

Ship: explicit syntax only (e.g. polymorphic product fields). See ../questions/081-generics-and-advanced-types.md.

8. GADTs

Branch-local equalities; existentials must not escape; principal types may be absent. Diagnostics historically leak ex#0.

Ship: ordinary ADTs stay simple; GADTs are advanced and annotation-heavy; name existentials in patterns/diagnostics.

9. Open variants / rows

let is_ok = function `Ok -> true | `Error _ -> false
(* [< `Error of 'a | `Ok ] -> bool *)

Ship: closed default for domain modeling; open variants for errors/channels with Ship tags (:ok, :error(v)); human-first row diagnostics. See 02-type-inference.md, open-variant.

10. Labels and optionals

OCaml may infer required labels from HOF use sites; optional erasure needs a later positional; trailing optionals + currying surprise users.

Ship: labels required; uncurried calls; Option(T) omit → None or = default; no erasure/(); explicit partial app (f(x, ...)). See book/003-Functions.shp.

11. No ad-hoc overloading

1 + 2
1.0 +. 2.0

Overloaded + breaks principal types for let double x = x + x.

Ship: nominal canonical behaviors + explicit module params (11-behavior-modules.md). Do not break principal inference for prettier arithmetic; any numeric story stays separate from general behavior lookup.

12. Product / constructor disambiguation

type user = { id : int; name : string }
type team = { id : int; members : user list }
let get_id x = x.id   (* which id? last-defined-wins, maybe warning 41 *)

Ship: unique/nearest, then a hard error — not last-defined-wins / warning

Same rule for constructors, literals, fields, updates, and patterns (02-type-inference.md).

13. Clever public APIs

Most-general inferred types (rows, paths, private aliases) become unwanted contracts without an interface.

Ship: joy in .shp, including unannotated parameters; .shc for the stable public shape. Do not stabilize a public API by copying types onto the implementation.

14. Module abstraction cliff

(* sealed M.t is opaque — not int — outside the signature *)

Ship: say "abstract because of this module boundary"; .shc / public shapes make the cliff visible.

15. Feature composition

GADT + polymorphic recursion + abstraction + rows + labels compound into lore.

Ship: small first typechecker; add advanced features only with diagnostics and examples.

Design rules

Principal types for the ordinary core.
Annotations anywhere; required only at real limits. Named .shp helpers are not a real limit.
Closed variants by default; deliberate open-variant design.
Labels/optionals with predictable, documented rules.
GADTs and higher-rank explicit.
Value-restriction and weak-boundary diagnostics teach the rule.
Origin spans + constraint trails; no raw internal names as primary UX.
.shc controls public surfaces.

02-type-inference.md, book/003-Functions.shp, 01-syntax.md
11-behavior-modules.md, lexicon open-variant / open-binder
../questions/081-generics-and-advanced-types.md