module Typesweeper where  —  elaborate :: Board → Either TypeError Board
λ Typesweeper.hs  —  GHCi
FileEditTypeHelp
036
🙂
000
How Typesweeper works

Every tile is a typed hole _ — a metavariable GHC must solve. You win when the whole board elaborates, i.e. the program type-checks. Each hole has the form F a: an outer functor F and a parameter a (the leaf). These are two independent facts and they arrive from opposite directions.

▼ checking
Pushed down from an expected type / signature. It pins the hole's functor F — one of Maybe, [], IO, Map. Every hole is genuinely wrapped: there is no bare-scalar case (a plain 42 :: Int would be [] / Maybe / …'s parameter, not a functor of its own). Teal.
▲ synthesis
Flowing up from a value. The amber chip shows a representative inhabitant of the parameter type a — 23, True, 'z', () — so 23 ⟹ a = Int. It witnesses the element/result type only; it is not the whole F a value and says nothing about F. A parameter that propagated over a wire shows the bare type instead.

Two wires, two ways two functorial types relate:

fmap wire — fmap :: (a→b) → f a → f b keeps the functor and may change the parameter. So a teal wire means same outer functor; it transmits F.
nat-trans wire — a natural transformation η :: f a → g a keeps the parameter and may change the functor. So an amber wire means same parameter; it transmits a.

Constraints & ambiguity (Intermediate / Expert): a hole may instead carry a typeclass constraint — Ixed on the functor axis or Bits on the parameter axis. A constraint narrows an axis to a set, never a point: Ixed f ⇒ f ∈ {[], Maybe, Map} (not IO); Bits a ⇒ a ∈ {Int, Bool} (not Char/()). So a constraint chip is not a known fact — you cannot elaborate a hole while it still shows one. It resolves only when a concrete type reaches it over its own island: Ixed over a teal wire, Bits over an amber one. A constraint whose island never touches a concrete pin — an isolated cell, or a whole region of constraints — stays permanently ambiguous.

The rule: a hole elaborates only once both its functor (▼) and its parameter (▲) are concretely pinned. Facts travel along wires, but only out of an already-elaborated hole. Start from a hole solid on both axes, elaborate it, and watch the cascade spread — on Beginner that alone clears the board.

Left-click / tap to elaborate a hole whose facts have arrived. Click one too early, or click a permanently-ambiguous hole, and you get an ambiguous type variable → 💥. Right-click / Annotate-mode tap writes @ — a type annotation. You win by elaborating every inferable hole and annotating every ambiguous one (the holes GHC genuinely can't infer for you).

Solid chip = a clue in the source; dotted chip = a fact propagated over a wire; violet/magenta chip = an unresolved constraint. Beginner Maybe·[]·IO, pure inference, no constraints. Intermediate adds Map + Ixed/Bits, ~10% ambiguous. Expert ~20% ambiguous. The instance lattice is curated/simplified for play.

A toy of GHC's bidirectional elaboration in Minesweeper's clothes. The functor comes down (checking ▼), the parameter comes up (synthesis ▲); a hole solves where they meet. Teal wires are fmap (same functor), amber wires are natural transformations (same parameter).