🌐 한국어로 읽기

09 — Types at last

Where we are

Chapter 08 closes at 298c9824 ("Rename uhs to mhs.", 2023-07-20 14:58:46): the compiler is self-hosting, bootcombtest passes, and the binary finally answers to the name this book has used from the start, mhs. Nothing about that binary checks a single type. f :: T has parsed since chapter 03's e96d04be (2023-05-30) and gone straight to dsDef (Sign _ _) = [] — accepted, then thrown away. Chapter 08's own db418344 (2023-07-18) gave signatures a real grammar — EType, a TVar/TConstr/TUVar type distinct from Expr, and ETypeScheme for forall — but left the desugarer's verdict unchanged: Sign _ _ -> [], still nothing downstream reads what's parsed. This chapter's range, 298c9824..a38c64ce, 24 commits over 21 days, is where something finally does.

What happened

Three commits named "Update"

The range opens with 7936c701, bca0b02d, and 3719955b, all on 2023-07-20, all titled "Update", and all touching exactly one file each time: README.md (4 insertions/13 deletions, 1/1, and 6 insertions with nothing removed, in that order). None of the three has anything to do with type checking — they're documentation upkeep sitting in the gap between chapter 08's close and this chapter's first substantive commit. Included here only because "commits named vaguely and checked anyway" is this book's own standard, not because there's anything more to say about them.

The prep, in one day: 33b009fa through e5bc9236

Five commits, all 2023-07-21, each making the ground firmer before anyone tries to write a type checker on it.

33b009fa ("Use Expr for EType.") deletes the three-constructor EType db418344 had introduced two days and twenty hours earlier and replaces it with type EType = Expr plus a validType predicate — the change aux/hindley-milner-gently.md opens with, since it's the one decision the rest of the checker is built on. The same commit, not mentioned in its own title, breaks showEType — the function that would pretty-print a type for a human — into a function that never returns (33b009fa:src/MicroHs/Parse.hs, quoted whole, the whole diff to this function):

 showEType :: EType -> String
-showEType at =
-  case at of
-    TVar i -> i
-    TConstr c ts ->
-      if null ts then
-        c
-      else
-        "(" ++ unwords (c : map showEType ts) ++ ")"
-    TUVar n -> "a" ++ showInt n
+showEType = showEType

There's no longer a TVar/TConstr/TUVar to pattern-match on — EType is just Expr now — and rather than rewrite showEType to walk Expr directly, 33b009fa leaves a stub that would loop forever if it were ever called. Checked directly: nothing in TypeCheck.hs or Main.hs calls showEType or showETypeScheme at any commit between 33b009fa and 617475b6 (below) — the stub sits dead in the source for nearly sixteen days (15 days 21 hours), across c0b279fc's skeleton checker, both "Transfer" commits, and f7db30f1's library-wide signature sweep, without ever being exercised.

45b34015, sixteen seconds later, is a genuine rewrite of a different function, showExpr — sixteen alternatives replaced to print terms without the (EVar "x")-style constructor-tagged debug format they used before ("(EVar " ++ v ++ ")" becomes plain v, and so on), the format unify's own error messages read from (aux/hindley-milner-gently.md quotes unifyR's use of it directly). 93a2f76e ("Allow '()' and '[]' as uppercase identifiers.") teaches pUIdent two new alternatives so that () and [] parse as ordinary constructor names rather than only as special-cased tuple/list punctuation (93a2f76e:src/MicroHs/Parse.hs, two lines added to pUIdent, quoted whole):

  <|> ("()" <$ (pSym '(' *> pWhite *> pSym ')'))  -- Allow () as a constructor name
  <|> ("[]" <$ (pSym '[' *> pWhite *> pSym ']'))  -- Allow [] as a constructor name

— needed because, with types now just Expr, a type like () or [a] has to resolve to an ordinary EVar constructor name (tCon "()", tApps "[]" [...], in the checker's own vocabulary) the same way Int or Maybe does, and before this commit ()/[] were parseable only inside expression syntax, never as a bare uppercase identifier a type application could apply to. ca512ed2 ("Get rid of Data.List_Type") folds data [] a = [] | (:) a [a] directly into lib/Data/List.hs, deleting the separate Data.List_Type module that used to carry only the type declaration — now that a module's own Data/Sign definitions and its term-level bindings live in the same EDef list the checker reads together, there's no structural reason to keep them apart. e5bc9236 ("Change ELam to abstract just one variable.") narrows ELam [Ident] Expr to ELam Ident Expr, with a new eLams :: [Ident] -> Expr -> Expr folding multi-argument lambdas down to nested single-argument ones at parse time (e5bc9236:src/MicroHs/Parse.hs, quoted whole):

pLam :: P Expr
pLam = eLams <$> (pSymbol "\\" *> esome pLIdent_) <*> (pSymbol "->" *> pExpr)

eLams :: [Ident] -> Expr -> Expr
eLams is e = foldr ELam e is

— the checker's own ELam case, added the next day, expects exactly one bound variable per lambda so it can unify it against exactly one tArrow at a time; a multi-argument ELam would have needed its own multi-step unification logic instead.

c0b279fc: a skeleton, wired into nothing

c0b279fc ("Start of type checking.", 2023-07-22 10:50:52) adds one new file, src/MicroHs/TypeCheck.hs, 57 lines — and touches nothing else, not the Makefile, not Compile.hs, not Main.hs. Nothing in the build imports it yet. It isn't even Haskell that GHC would accept on its own: tcExpr's type signature mentions a monad T (tcExpr :: Maybe EType -> Expr -> T (Typed Expr)), but the file's only import is import Control.Monad.State as T (c0b279fc:src/MicroHs/TypeCheck.hs line 3) — qualified import syntax that makes names like T.get available, not a bare type called T. Several cases are undefined outright (ECase _ = undefined, ELet _ = undefined, EDo _ = undefined), and the function runs off the end mid-definition — the file's last line is tc, an unfinished identifier with nothing after it. This is the first draft in the most literal sense: a shape for what the checker's core recursion over Expr will look like (tcExpr, an EVar/EApp/ELam/EInt walk with a Maybe EType for bidirectional checking, already recognizable in cc57346e's working version two weeks later), committed before it compiles, let alone runs.

An unrelated fix, and two commits called "Transfer"

7ae8c443 ("Make int64_t printing portable.", 2023-07-22 15:57:15) is a one-file runtime fix — eval.c's number formatting — with nothing to do with type checking; included here because it lands between c0b279fc and the next TypeCheck.hs work, a reminder that this project's git history doesn't pause other work while one feature is in progress. Then, one minute fifty seconds apart the same evening, 3437518f and 031d2125, both titled "Transfer", touch only src/MicroHs/TypeCheck.hs — 114 lines changed (74 insertions, 40 deletions) and then 6 more (4/2). Neither commit message says what's being transferred or from where; read as diffs, both are straightforward elaborations of the same skeleton c0b279fc started (more cases filled in, more helper functions), not a wholesale replacement — consistent with, though not confirmed by anything in the repository beyond the diffs themselves, work drafted somewhere else (a second checkout, a different machine) and copied in by hand rather than merged.

f7db30f1: the chapter 03 debt, collected — in the library

f7db30f1 ("Add lots of type signatues and forall.", 2023-07-23 19:28:49) is the commit aux/hindley-milner-gently.md quotes closely: 9 files, 134 insertions, 74 deletions, 80 added lines containing forall, 128 added lines containing ::. Worth stating precisely, because the shape is easy to get wrong: every file this commit touches is under lib/ (Data/Either.hs, Data/Function.hs, Data/Int.hs, Data/List.hs, Data/Map.hs, Data/Maybe.hs, Data/Tuple.hs, Primitives.hs) plus the Makefile — the standard library every MicroHs program (including the compiler's own src/ tree, which imports it) pulls in, not src/MicroHs itself. And most of those 128 :: lines are not brand-new signatures — const :: a -> b -> a already existed in lib/Data/Function.hs; what f7db30f1 adds to it is forall a b . in front. Chapter 03's e96d04be:Desugar.hs comment says "the meaning arrives months later" — f7db30f1 lands 54 days after e96d04be, and cc57346e's working checker another 14 days after that, 68 days total. What arrives first, at f7db30f1, is not "the compiler reads Sign" — the checker doesn't exist as a working feature yet — it's the library gaining the quantifiers the checker's rigid-variable mechanism will need to accept anything polymorphic at all, once it does exist, exactly as aux/hindley-milner-gently.md's forall/instantiation section demonstrates by removing one.

Two more unrelated commits, one of them quietly load-bearing

677a0f0e ("Handle negative literals.", 2023-07-25 14:58:16) is another runtime-only fix, eval.c, twelve insertions and one deletion. Eighteen seconds later, 17b450fc ("Add more lib modules.") adds two files outright: lib/Control/Monad/State.hs (52 lines) and lib/Data/IntMap.hs (77 lines). The commit message doesn't say why a compiler needs an IntMap, but TypeCheck.hs's own state — TCState's last field, the unification substitution (aux/hindley-milner-gently.md's "Metavariables and substitution" section) — is exactly IM.IntMap EType, and cc57346e's import list confirms it: import qualified Data.IntMap as IM. 17b450fc isn't titled as type-checking work, but it's the commit that puts the checker's core data structure within reach.

The quiet grind: 9a392312 to 617475b6

9a392312 ("Temp commit", 2023-07-27 13:47:19) touches TypeCheck.hs with 173 insertions and 26 deletions, and touches five other files besides (Makefile, Compile.hs, Desugar.hs, Main.hs, Parse.hs) — wiring the checker into the build for the first time, unlike every commit before it. Then nothing, for 9 days 21 hours 51 minutes, until 617475b6 ("Temp", 2023-08-06 11:38:42) — a single commit that rewrites TypeCheck.hs again, 543 insertions and 65 deletions this time, across 11 files total including a near-total restructuring of Desugar.hs (67 insertions, 205 deletions). Nothing in the repository explains the gap the same way chapter 07's 24-day silence goes unexplained in 00-overview.md — the log simply resumes. What the two commits' titles share — "Temp commit", "Temp" — is an honest description: neither claims to be finished, and neither is committed as a clean, working state so much as a savepoint. 617475b6 is also where the showEType infinite loop from 33b009fa, nearly sixteen days earlier, finally gets fixed — one line, alongside everything else this commit touches (617475b6:src/MicroHs/Parse.hs, quoted whole): showEType = showExpr. Not a redesign, just routing the type-printer through the (already rewritten, in 45b34015) term-printer, since EType has been Expr all along.

cc57346e: "First version with type checking."

Seven hours thirty-eight minutes after 617475b6's rewrite lands, the same day, cc57346e (2023-08-06 19:16:48) is the commit both this chapter and aux/hindley-milner-gently.md treat as the checker's first real snapshot: 16 files, 187 insertions, 78 deletions. src/MicroHs/TCMonad.hs is new — 13 lines, a thin re-export of Control.Monad.State.Strict under the compiler's own qualified name T, finally giving c0b279fc's two-week-old, never-compiling type signature somewhere real to point. TypeCheck.hs itself, at this commit, is the file aux/hindley-milner-gently.md quotes from throughout — unify/unifyR, EUVar-as-metavariable, tInst, tcDefValue, all present and in the shape that document describes. What it can do by this commit: check EVar/EApp/ELam/literals, ECase, ELet, ETuple, EList, EDo, EIf, and list comprehensions — every case c0b279fc had left as undefined two weeks earlier is filled in. What it demands in return shows up immediately in the same commit's own test suite: all six files under tests/ gain a main :: IO () signature they didn't have before (tests/Arith.hs, ListTest.hs, StringTest.hs each need only that one line; Fac.hs also needs res :: (Int, Int); IOTest.hs needs f :: Int -> Int and foo :: IO (); Misc.hs's existing first :: (a, b) -> a needs forall a b . added in front) — the same "every top-level binding needs an explicit signature" rule aux/hindley-milner-gently.md demonstrates by removing one from lib/Data/List.hs's null, now visible landing on the project's own test files at the exact commit that turns checking on.

The fix streak

Six commits, da5350d2 through 64345fe2, spread across three calendar days with two full silent calendar days in the middle — 2023-08-06 (da5350d2 19:31, 3bf3924a 23:56), 2023-08-07 (a90d1175 12:21, bb8aec3b 12:22), nothing on the 8th or 9th, then 2023-08-10 (64345fe2 11:06, the same day as the chapter's final commit). Read together, most of their TypeCheck.hs diffs are not new type-checking logic at all — they're the same "diet" aux/bootstrapping-a-compiler.md describes for the rest of the compiler, applied to the newest module so that it, too, can eventually compile under mhs itself, not only under GHC. da5350d2 ("Improve.") strips every HasCallStack => constraint behind a --X comment marker and switches bare mapM/mapM_ to qualified T.mapM/T.mapM_ — GHC.Stack and an unqualified Prelude mapM are exactly the kind of import mhs's own restricted dialect doesn't have. 3bf3924a ("Various type fixes.") continues the same pattern: EApp <$> expandType f <*> expandType a-style Applicative code, which needs <$>/<*> instances mhs has no type classes to provide, rewritten as explicit T.do binds; bare return/pure qualified to T.return. a90d1175 ("Better import") is three insertions and two deletions in TCMonad.hs, an import tweak. bb8aec3b ("More type fixes") is six insertions and one deletion in Parse.hs, mostly commented-out (--X-marked) pretty-printer alternatives for showExpr, not live code. 64345fe2 ("More type checking fixes.") is the largest of the six — 163 lines in TypeCheck.hs alone — and, checked directly rather than assumed from its title, contains at least one genuine correctness fix, not just portability churn: expandSyn's handling of a multi-argument type synonym. Before this commit, type Pair a b = (a, b) used with two arguments fails to type-check at all — confirmed by building cc57346e and compiling a one-line program that uses one: mhs: Cannot unify SynTest.Pair and ,. 64345fe2 rewrites the EApp case of expandSyn to walk the application spine correctly, expanding each argument before pushing it onto the accumulator instead of recursing into the wrong sub-term (64345fe2:src/MicroHs/TypeCheck.hs, quoted whole, the changed case):

        EApp f a -> T.do
          aa <- expandSyn a
          syn (aa:ts) f

— confirmed fixed by building a38c64ce and compiling the identical SynTest.hs: it compiles and runs, printing 1. One more honest detail, found by trying to build 64345fe2 on its own rather than only reading its diff: this commit does not compile standalone under GHC, failing with Not in scope: 'T.fail' / Not in scope: 'T.>>=' wherever TypeCheck.hs pattern-matches inside a T.do block. The fix, a38c64ce's own TCMonad.hs change, is the --X/--Y marker trick aux/bootstrapping-a-compiler.md documents, caught mid-flip: at 64345fe2, src/MicroHs/TCMonad.hs line 16 reads --import Control.Monad, a plain comment with no --X marker, so convertX.sh never touches it and Control.Monad — the module that would bring fail/(>>=) into scope for MicroHs.TCMonad's own module MicroHs.TCMonad export item to re-export — is never actually imported for the GHC build. a38c64ce changes that one line to --Ximport Control.Monad hiding(ap) (a38c64ce:src/MicroHs/TCMonad.hs line 17) — now marked, so convertX.sh's sed -e 's/--X//' strips the marker and the bin/mhs build actually sees import Control.Monad hiding(ap), and T.fail/ T.>>= resolve. Consistent with 00-overview.md's framing of this project's commit history — broken states get committed, not held back until clean.

a38c64ce: the fixpoint

a38c64ce ("Now bootstraps with type checking.", 2023-08-10 20:37:30) is seven files, 29 insertions, 24 deletions — small, by this chapter's standards, for a commit that closes the book's whole arc. The Makefile change is one number: bootcombtest's eval invocation grows its heap from -H10000000 to -H50000000, and the same commit deletes the $(MHS)test target (originally uhstest, chapter 07's 1d6d1210, 2023-07-05, renamed by 298c9824 in chapter 08) — an interpreted-mode smoke test, $(BIN)/$(MHS) -ilib -isrc Main; $(BIN)/eval with no arguments, superseded once bootcombtest itself is the thing that has to work. In TypeCheck.hs, the load-bearing change is four lines, a new function called between every top-level definition's own check (a38c64ce:src/MicroHs/TypeCheck.hs lines 360–364, quoted whole):

-- Reset type variable and unification map
tcReset :: T ()
tcReset = T.do
  TC mn _ tenv venv _ <- get
  put (TC mn 0 tenv venv IM.empty)

— wired in at both call sites that walk a module's definition list, tcDefsType and tcDefsValue, each changed from T.mapM tcDefType ds / T.mapM tcDefValue ds to T.mapM (\ d -> T.do {tcReset; tcDefType d}) ds and the value-checking equivalent. Before this commit, the fresh- metavariable counter and the unification substitution map accumulated across every top-level definition in a module without ever being cleared; after it, each definition starts from EUVar 0 and an empty substitution. The commit message doesn't explain what checking the compiler's own ~30-file source — 571 distinct top-level combinator labels in the resulting mhs.comb, counted directly — without that reset actually did — whether it was simply slow, or something worse — only that adding tcReset is what the title reports finally working. Alongside it, two correctness fixes narrower in scope: ESectR's case used to pattern-match its checked operator as EVar ii directly, which crashes for any section built from a data constructor rather than a plain function (the checker's own EVar case can return ECon cti qi from tLookupInst, not only EVar) — fixed to match a generic var and extract the name through getIdent (a38c64ce:src/MicroHs/TypeCheck.hs line 694: T.return (ESectR (getIdent var) ee, t)). And primTypes gains one new entry, "Any", the same commit that adds forall a b . to lib/Unsafe/Coerce.hs's unsafeCoerce :: a -> b — the "Any" primitive type and unsafeCoerce's forced universal quantification arrive together. The rest of the diff — a qualified MicroHs.StateIO.return in StateIO.hs where a bare return used to be ambiguous between two returns now both in scope, an unqualified Handle import fix in Compile.hs, a fallback-arm tweak in Desugar.hs's single-arm case handling — is the same self-hosting-compatibility housekeeping the fix streak above already established as this range's dominant texture. Built and run, at this commit, exactly as bootcombtest runs it (see "Try it" below): bin/mhs compiles MicroHs.Main from source; bin/eval, interpreting mhs's own combinator translation, compiles the identical source a second time; the two outputs, 140,782 bytes each, are byte-identical. The typed compiler type-checks itself, compiling itself.

Undisclosed extras

Three found by reading diffs rather than titles, gathered here: the showEType = showEType infinite loop 33b009fa introduces silently (under a title about EType's representation, not its printing) and 617475b6 fixes silently nearly sixteen days later, never once exercised in between; 64345fe2 ("More type checking fixes.") not compiling standalone under GHC, discovered only by building it rather than trusting the next commit's message; and the two "Transfer" commits, 3437518f/031d2125, whose titles say nothing about what's being transferred but whose diffs — 114 and 6 lines, both confined to TypeCheck.hs — are at least consistent with what they claim to be, unlike chapter 08's 8e2f7109 (which dropped a safety flag its title never mentioned). Nothing found this chapter rises to that level — everything here is scope not stated plainly, not effects contradicting a title.

Why it matters

Types came last. Not first, not alongside the parser, not even alongside do-notation or modules — after the language, the runtime, IO, and self-hosting all worked, on a compiler that had already compiled itself for three weeks with every signature in its own source doing nothing at all. That ordering is the whole shape of this book's method, not an accident of one project: chapter 03's dsDef (Sign _ _) = [] bought two months and change of writing signatures as documentation, free of any obligation to make them true; chapter 05's habits — commit often, note what's broken, keep a lab notebook — are exactly what let 9a392312 and 617475b6 sit nine days apart under titles that admit they're unfinished, without the project stalling; chapter 08's self-hosting push is what gives this chapter a workload — the compiler's own ~30-file source — big enough to need tcReset at all, a fix nothing smaller would have surfaced. The untyped compiler wasn't a detour from building a typed one; it was the scaffolding that made building a typed one tractable, one small commit at a time, on a language that already worked before anyone had to prove it worked. Two files, Lam.hs and eval.c, on 2023-05-25. A self-hosting typed compiler that checks itself compiling itself, 77 days later, on a38c64ce, 2023-08-10. This account stops here because that's where git log says the story 00-overview.md promised is told in full: "The last stretch, through early August, adds a Hindley-Milner type checker and gets the self-hosted compiler bootstrapping with type checking ...".

Notebook margin

• "Temp commit" and "Temp" are not filler titles — they're savepoints, committed mid-thought on purpose, 9 days 21 hours 51 minutes apart, with no explanation in between for the gap. The habit this book has tracked since chapter 05 — commit even when it doesn't work — is what makes a multi-week rewrite like 617475b6's 608-line TypeCheck.hs diff possible without losing 9a392312's 199-line first attempt.
• Refactor before feature, again: 33b009fa/e5bc9236's prep (types as Expr, one-variable lambdas) lands a full day before c0b279fc's first line of actual checker code — the same rhythm chapter 03's "Notebook margin" named for 4e4c5252 and ff4622e8, now operating one level up, on the checker's own prerequisites rather than the parser's.
• The fix-streak rhythm: six commits, three calendar days, two full silent calendar days in the middle (08-08, 08-09) — and the very last commit in that streak, 64345fe2, doesn't even build standalone. Fixing real bugs (a multi-argument type synonym) and fixing self-hosting portability (qualified T.do binds, stripped HasCallStack) happen in the same commits, not separated into "correctness" and "cleanup" passes.
• 17b450fc ("Add more lib modules.") never says why the compiler needs an IntMap — the connection to TypeCheck.hs's own substitution map is legible only from reading both files, not from either commit message.

Try it

Anchor: a38c64ce ("Now bootstraps with type checking."), 2023-08-10 20:37:30 — the commit that makes the typed self-compile agree with itself. Convention (see 00-overview.md):

git worktree add /tmp/mhs-a38c64ce a38c64ce
cd /tmp/mhs-a38c64ce

No Build-note patch needed at this commit — the GHC-9.8/mtl issues chapters 02, 03, and others in this book had to route around are gone from Main.hs's own import list by this point in the project. Build both binaries as written:

mkdir -p bin
nix develop $MICROHS -c make bin/mhs
nix develop $MICROHS -c make bin/eval

[...]
[16 of 16] Linking bin/mhs

gcc -Wall -O3 src/runtime/eval.c -o bin/eval

(The same -Wx-partial head/tail warnings every earlier chapter's Build notes already flag appear during the bin/mhs build; omitted.) Run the ordinary test suite first — seven tests/*.hs files (the six cc57346e had to add main :: IO () to, per "What happened" above, plus Case.hs, which already had one), each compiled and its output diffed against a checked-in .ref file:

nix develop $MICROHS -c make test

cd tests; make test
../bin/mhs -i../lib IOTest && (echo q | ../bin/eval -- a bb ccc > IOTest.out) && diff IOTest.ref IOTest.out
../bin/mhs -i../lib StringTest && ../bin/eval > StringTest.out && diff StringTest.ref StringTest.out
../bin/mhs -i../lib ListTest && ../bin/eval > ListTest.out && diff ListTest.ref ListTest.out
../bin/mhs -i../lib Fac && ../bin/eval > Fac.out && diff Fac.ref Fac.out
../bin/mhs -i../lib Misc && ../bin/eval > Misc.out && diff Misc.ref Misc.out
../bin/mhs -i../lib Case && ../bin/eval > Case.out && diff Case.ref Case.out
../bin/mhs -i../lib Arith && ../bin/eval > Arith.out && diff Arith.ref Arith.out

Every diff above is silent — all seven pass. Now the money shot, the same bootcombtest target chapter 08's Try-it ran without type checking — first make bootcombtest whole, then each of its three lines timed separately the way chapter 08's own Try-it does:

nix develop $MICROHS -c bash -c 'time make bootcombtest'

bin/mhs -ilib -isrc -omhs.comb MicroHs.Main
bin/mhs -ilib -isrc -omain-mhs.comb  MicroHs.Main
bin/eval -H50000000 -rmhs.comb --  -ilib -isrc -omain-comb.comb MicroHs.Main
cmp main-mhs.comb main-comb.comb

real	0m37.674s

nix develop $MICROHS -c bash -c 'time bin/mhs -ilib -isrc -omain-mhs.comb MicroHs.Main'

real	0m1.794s

nix develop $MICROHS -c bash -c 'time bin/eval -H50000000 -rmhs.comb -- -ilib -isrc -omain-comb.comb MicroHs.Main'

real	0m32.254s

cmp prints nothing and exits 0: main-mhs.comb and main-comb.comb — 140,782 bytes each, confirmed with ls -la and a second explicit cmp run — are byte-identical. Compare against chapter 08's own numbers at this chapter's own starting point, 298c9824 (75,052-byte outputs, 0.890s native / 20.715s interpreted, no type checking at all): the typed compiler's self-compiled output is nearly twice the size, the native compile is about twice as slow (1.794s), and the interpreted step is about 55% slower (32.254s) — and every byte of that output now passed through unify on the way, the same combinator-level oracle chapter 08 established, now proving something chapter 08 couldn't: that the type checker agrees with itself about its own source, not just that the untyped compiler does.

Exercise 1: a deliberate type error, traced to its source

cat > TypeErr.hs <<'EOF'
module TypeErr(module TypeErr) where
import Prelude

bad :: Int
bad = 1 + "hello"

main :: IO ()
main = putStrLn (showInt bad)
EOF
nix develop $MICROHS -c ./bin/mhs -ilib TypeErr

mhs: Cannot unify [Char] and Primitives.Int
EApp (EVar "Data.List.[]") (EVar "Primitives.Char") - EVar "Primitives.Int"
Map [("Data.Char.String",ETypeScheme [] (EApp (EVar "Data.List.[]") (EVar "Primitives.Char")))]
CallStack (from HasCallStack):
  error, called at src/MicroHs/TypeCheck.hs:334:11 in main:MicroHs.TypeCheck
  unifyR, called at src/MicroHs/TypeCheck.hs:326:3 in main:MicroHs.TypeCheck
  ...

(exit code 1; the rest of the CallStack — more unify/unifyR frames from +'s own two-argument check — omitted above.) The message comes from unifyR's bad binding (a38c64ce:src/MicroHs/TypeCheck.hs line 334, quoted): bad = error $ "Cannot unify " ++ showExpr a ++ " and " ++ showExpr b ++ "\n". 1 + "hello" needs "hello"'s type, [Char] (String is a type synonym for it, hence the Map line naming Data.Char.String), to unify with +'s second-argument type, Int — an EApp/EVar mismatch that unifyR's structural case rejects immediately, exactly as aux/hindley-milner-gently.md's unification section traces by hand.

Exercise 2: remove a signature the checker needs

(python3 here comes from the host system, not the devShell — the same caveat chapter 01 discloses for diff.)

python3 -c "
with open('lib/Data/List.hs') as f:
    lines = f.readlines()
out = [l for l in lines if l.strip() != 'null :: forall a . [a] -> Bool']
with open('lib/Data/List.hs', 'w') as f:
    f.writelines(out)
"
nix develop $MICROHS -c ./bin/mhs -ilib Example

mhs: undefined variable null
CallStack (from HasCallStack):
  error, called at src/MicroHs/TypeCheck.hs:382:16 in main:MicroHs.TypeCheck

Inference doesn't cope — there is no inference step for a missing top-level signature to fall back on. addValueType (a38c64ce:src/MicroHs/TypeCheck.hs lines 553–559) only adds a name to the value table when it sees a Sign; a Fcn with no matching Sign in the same module never gets one, and tcDefValue's tLookup i on that name hits the "not found" branch directly — even though null is never called anywhere in Example.hs, lib/Data/List.hs itself still has to type-check as a whole module once anything imports it, and every one of its top-level bindings, used or not, needs its own signature to be checked at all. Restore the file before continuing:

git checkout -- lib/Data/List.hs

Exercise 3: hand-infer a Prelude function, then check the source

lib/Data/Function.hs, flip:

flip :: forall a b c . (b -> a -> c) -> a -> b -> c
flip f a b = f b a

Hand-inferring flip f a b = f b a's body against the checker's own algorithm (tcExpr''s EApp case: to check g x, check x first with no expected type, then check g against (type of x) -> (fresh result)):

1. f b a is EApp (EApp f b) a. Checking the outer application: a (the argument) gets a type first — it's a lambda-bound variable, so its type is whatever fresh metavariable flip's own ELam case gave it when it bound a; call that τ_a. The result of the whole expression gets a fresh metavariable too, τ_r. Then f b is checked against the expected type τ_a -> τ_r.
2. f b is itself EApp f b. b's type is its own binding's metavariable, τ_b. f is checked against τ_b -> (τ_a -> τ_r). f is a bound variable too, with its own metavariable τ_f from flip's outermost ELam; unifying τ_f against τ_b -> (τ_a -> τ_r) binds it directly (f's type is τ_b -> τ_a -> τ_r, nothing left to check).
3. Unwinding: flip's constructed type is τ_f -> τ_a -> τ_b -> τ_r, substituting step 2's result for τ_f: (τ_b -> τ_a -> τ_r) -> τ_a -> τ_b -> τ_r. Unified against the declared (b -> a -> c) -> a -> b -> c: τ_b ↦ b, τ_a ↦ a, τ_r ↦ c, every metavariable resolving to exactly the signature's own names, no contradiction — the same shape aux/hindley-milner-gently.md's const walk-through ends on.

Checked against the source: a38c64ce:lib/Data/Function.hs's own signature for flip is exactly forall a b c . (b -> a -> c) -> a -> b -> c — matching the hand-inferred type above term for term. Confirmed live, not just by inspection, with a program that uses it at a concrete type:

cat > FlipDemo.hs <<'EOF'
module FlipDemo(module FlipDemo) where
import Prelude

main :: IO ()
main = putStrLn (showInt (flip (-) 3 10))
EOF
nix develop $MICROHS -c ./bin/mhs -ilib FlipDemo
nix develop $MICROHS -c ./bin/eval

7

(flip (-) 3 10 = (-) 10 3 = 7, b ↦ Int, a ↦ Int, c ↦ Int all instantiated to the same concrete type here, which is why this one call doesn't distinguish flip's type from a monomorphic one — the point of the hand-trace above is that the checker never needed to know that in advance.)

Clean up:

git worktree remove --force /tmp/mhs-a38c64ce