diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,208 @@
 # Changelog
 
-## Unreleased — compile time of large grammars
+## Unreleased
+
+### Breaking. The environment no longer carries FIRST sets
+
+An entry of a grammar's environment was a rule's nullability, its FIRST set
+and its result type.  It is now the result type:
+
+```haskell
+type CalcEnv =
+  '[ '("expr" , 'EnvEntry Expr)     -- was 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr
+   , '("term" , 'EnvEntry Expr)
+   , '("atom" , 'EnvEntry Expr)
+   ]
+```
+
+`PExp` loses its `ty` index and is now `PExp s env a`; `Grammar` is
+`Grammar s env a`.  `PEG.Type.Ty`, `Nullable`, `First`, `TyOf`,
+`PEG.Syntax.SeqTy`, `ChoiceTy`, `NTTy`, `NTGo`, `PEG.Grammar.Acyclic` and the
+sorted-set families in `PEG.TyLevel` — `Union`, `Elem`, `ConsIfAbsent`, `If`,
+`And`, `Or`, `SymEq` — are gone.  A grammar written with `pegGrammar` needs no
+change; one that writes its environment by hand needs the `'MkTy` component
+deleted from each entry and the `ty` argument deleted from its signatures.
+
+**Why.**  The FIRST sets in the environment were the entire cost of compiling
+a large grammar, and the measurement that says so is that *not computing them
+was worth nothing*.  A mode that kept the large environment but handed GHC
+every rule's index as a literal, so that `SeqTy`, `ChoiceTy` and `Union` were
+never reduced, ran no faster than one that reduced them all.  What cost was
+the environment being `O(N^2)` type nodes and each of the `2N` reference
+constraints being solved against it: in the micro-benchmark, giving each entry
+a payload that no type family ever reads takes `N = 64` from 0.77 s to 11.8 s
+and exhausts 8 GB at `N = 96`.
+
+**What it bought**, on a grammar of `N` mutually referring rules
+(`bench-compile/`, `ghc -fno-code`):
+
+| N | before | after | |
+|---|---|---|---|
+| 64, environment by hand | 15.15 s | 1.99 s | 7.6x |
+| 64, through `pegGrammar` | 7.23 s | 1.19 s | 6.1x |
+| 128, through `pegGrammar` | — | 5.28 s | |
+
+The curve changed and not only the constant: doubling the grammar from 32 to
+64 rules used to cost about 8x and now costs 3.3x, so what was cubic in the
+number of rules is closer to quadratic.  A 128-rule grammar through
+`pegGrammar` now costs less than a 64-rule one did.
+
+Two shapes that used to differ by 4.9x — a rule beginning with a non-terminal
+against one beginning with a terminal — are now indistinguishable, which is
+the check that the cost is gone rather than moved.
+
+**Leaving the environment to inference now works.**  `Grammar s _ a` with a
+wildcard environment used to be unusable: GHC inferred entries full of
+unreduced type-family applications and was past 24 GB of heap at `N = 16`.
+There are none left to leave unreduced, and it is now within noise of writing
+the environment out — 2.25 s at `N = 64`.  A hand-written rule set need not
+declare an environment at all.
+
+**What this gives up.**  Left recursion was a type error, checked on every
+compilation by `Acyclic`.  It is now checked once, by `PEG.Analysis`, when
+`pegRules` or `pegGrammar` splices the grammar — which is where it was already
+reported, with the rule and its cycle named, and which is the message you
+actually saw.  What is no longer checked at all:
+
+- A `Rules` chain assembled by hand from `RCons`, with no quasi-quoter
+  involved.  A rule that begins with itself compiles and loops.
+- Left recursion that closes *across* two `pegRules` blocks spliced together.
+  A block is analysed open-world, since `RCons` lets two be combined, and
+  `Acyclic` used to be the backstop.  Writing the grammar as a single
+  `pegGrammar` closes the gap: it is closed-world.
+
+`Star` no longer demands a non-nullable operand, for the same reason; a
+nullable repetition is reported by `PEG.Analysis`, and by nothing at all if
+the `Star` is built by hand.
+
+**What this makes simpler.**  A combinator over expressions is now an ordinary
+polymorphic function.  What had to be written
+
+```haskell
+lexeme :: PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a
+```
+
+is `PExp s env a -> PExp s env a`, and composes without the caller having to
+get a nesting of type families right.  `examples/Patterns.hs` is where that
+shows.
+
+**And what now keeps the analysis honest.**  While the FIRST sets were also in
+the types, `PEG.Analysis` could not be quietly wrong: `Grammar` demands
+`Rules s env env`, so GHC recomputed everything and rejected an environment
+that did not match.  It no longer does.  The `typed-peg-analysis` test-suite
+therefore checks the analysis against a separate statement of what its results
+mean — nullability as a least fixpoint, and a FIRST set as the transitive
+closure of the one-step head relation — over every grammar in `examples/` and
+over 400 generated ones, and asserts that the generated corpus keeps
+containing both left-recursive and left-recursion-free grammars so the
+agreement cannot go vacuous.
+
+### Grammar checking at splice time
+
+The environment a grammar declares is no longer something only GHC can
+compute.  `PEG.Analysis` runs the same nullability and FIRST-set fixpoint in
+ordinary Haskell, over the quasi-quoter's syntax tree.
+
+*(Superseded above: the environment no longer states either, and
+`PEG.Analysis` is the only thing that computes them.)*
+
+Measurement first, because it redirected the work.  On a synthetic grammar of
+`N` rules with `2N` non-terminal occurrences (`bench-compile/`, `ghc -fno-code
+-freduction-depth=0`):
+
+| N | environment written by hand | same, FIRST sets emptied | same, indices handed to GHC as literals |
+|---|---|---|---|
+| 16 | 0.59 s | 0.55 s | 0.52 s |
+| 32 | 1.80 s | 1.09 s | 1.43 s |
+| 48 | 6.39 s | 1.97 s | 5.19 s |
+| 64 | 18.25 s | 3.75 s | 14.99 s |
+
+Left to inference, the same grammar runs out of memory rather than time: at
+`N = 16` GHC was past 24 GB of heap and still climbing.  It does derive
+exactly the environment the examples write by hand — the entries it derives
+are just full of unreduced type-family applications.
+
+And, isolating the environment search alone — `N` entries, `2N` references:
+
+| N | `Lookup` + `KnownMember` | witness, equality kept | witness, no equality |
+|---|---|---|---|
+| 32 | 0.55 s | 0.20 s | 0.18 s |
+| 64 | 3.37 s | 0.86 s | 0.56 s |
+
+Three quarters of it is the instance chain, and that quarter-to-three-quarters
+split is the useful part: supplying the proof while keeping the `Lookup`
+equality — so the reference still cannot name the wrong rule — collects most
+of the win.  On the real library, on the grammar above, it is worth **2.6x**
+at `N = 64`: 16.60 s becomes 6.27 s.
+
+So the cost that remains after the 0.2 work is mostly **not** the FIRST-set
+arithmetic: computing it in advance and handing GHC the answer is worth 1.2x.
+It is the environment — searched once per occurrence of every non-terminal,
+over entries whose size is dominated by the FIRST sets they carry.  Those are
+two independent levers that compose: 2.6x for how a reference is resolved
+(taken below) and 4.9x for what the entries carry (taken above — and the
+1.2x turned out to be the whole of the arithmetic, so what the entries carry
+cost nothing to compute and everything to have).  `PEG.Analysis` computes the
+whole environment for the 64-rule grammar in 6 ms.
+
+### Added
+
+- `PEG.Analysis`: nullability, FIRST sets and well-formedness computed at
+  splice time.  It was then the value-level twin of `PEG.TyLevel`, which was
+  the specification; it is now the only implementation, and what checks it is
+  the `typed-peg-analysis` test-suite.
+- `pegRules` now reports left recursion, a nullable repetition and a duplicate
+  rule **from the splice**, naming the rule and, for left recursion, the chain
+  of head references that closes the cycle.  A block is analysed open-world,
+  since `RCons` lets two blocks be combined, so an unknown name is treated as
+  opaque rather than reported; `Acyclic` was then the backstop, and is now
+  gone, so a cycle closing across two blocks is caught by nothing.  Write the
+  grammar as one `pegGrammar` to close that gap.
+- `PEG.QQ.Syntax`: the DSL's syntax tree and parser, split out of `PEG.QQ` so
+  that the analysis and the translation can both consume it.
+- **`pegGrammar`**, a quasi-quoter for a whole grammar.  In expression
+  position it produces the `Grammar` value; in declaration position it also
+  declares the environment and the signature, so that a grammar of `n` rules
+  is `n` lines and nothing else:
+
+  ```haskell
+  [pegGrammar|
+    %name  arith
+    %start expr
+    expr   :: Exp <- t:term ts:(o:[+-] u:term)* { foldl addOp t ts }
+    ...
+  |]
+  ```
+
+  Because it owns the whole grammar it knows each rule's position, so it emits
+  `ntw` and the membership proof rather than `nt` and a search — **2.1x** on the
+  64-rule grammar above.  It also knows that a name no rule defines is an
+  error rather than a reference to somewhere else, so it says so at the
+  splice.
+
+  A rule's result type is the one thing the grammar does not determine, which
+  is what the `:: T` annotations are for.  They are claims, not assertions:
+  `Grammar` demands `Rules s env env`, so GHC checks each against what the
+  rule body actually returns.  *(At the time this also meant GHC recomputed
+  the FIRST sets and so could not be lied to about them; the entry above is
+  what changed that.)*
+
+  `examples/Arith.hs` and `examples/Layout.hs` are written this way now and
+  declare no environment at all.  `pegRules` is unchanged and still the way to
+  write a rule set that is only part of a grammar; `examples/Compat.hs` and
+  `examples/Patterns.hs` keep using it.
+- `PEG.Syntax.NTW` and `ntw`: a non-terminal reference that carries its own
+  `Member` proof instead of having `KnownMember` search for it.  The `Lookup`
+  equality is kept, so `ty` and `a` still come from the environment and a
+  proof that names the wrong rule does not compile — this is not a weaker
+  claim than `NT`, only a cheaper one.  Worth **2.6x** on a 64-rule grammar.
+  A splice knows each rule's position and can write the proof down; a
+  hand-written grammar has nothing to gain and should keep using `nt`.
+- `bench-compile/`: a generator and a sweep script for the numbers above.
+- A test-suite, `typed-peg-analysis`, that reads `examples/` and requires the
+  computed environment of each grammar to equal the one written there.
+
+### Compile time of large grammars
 
 Checking a grammar was **exponential in the size of its FIRST sets**.  On a
 chain of `n` mutually referring rules, GHC needed 0.7 s at `n = 8`, 12 s at
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,14 +2,15 @@
 
 Type-safe PEG (Parsing Expression Grammar) parser combinators for Haskell.
 
-Grammar non-terminals are indexed at the type level by their nullability and
-FIRST sets, so left-recursive grammars are caught at compile time rather than
-looping at runtime.
+Grammar non-terminals are checked at the type level against an environment
+that binds each rule to the type it returns, and left-recursive grammars are
+caught when the grammar is written rather than looping at runtime.
 
 ## Features
 
-- Type-level FIRST-set and nullability tracking
-- Compile-time left-recursion detection (type error)
+- Non-terminal references checked at the type level
+- Left recursion, a repetition that cannot consume input, an undefined
+  non-terminal and a duplicate rule reported at the splice, naming the rule
 - Indentation-sensitive parsing (`PEG.Indent`)
 - Quasi-quoter for concrete grammar syntax (`PEG.QQ`)
 - Parses any `PEG.Stream`: `String`, strict/lazy `Text`, strict/lazy
@@ -56,37 +57,99 @@
 
 ```haskell
 import PEG
+import PEG.QQ (pegGrammar)
 
--- Define a grammar using the quasi-quoter
--- See examples/Arith.hs for a complete arithmetic expression parser
+data Exp = Lit Int | Add Exp Exp | Mul Exp Exp
+
+[pegGrammar|
+  %name  arith
+  %start expr
+
+  expr   :: Exp <- t:term ts:(o:[+] u:term)*     { foldl addOp t ts }
+  term   :: Exp <- f:factor fs:(o:[*] g:factor)* { foldl addOp f fs }
+  factor :: Exp <- n:number / '(' e:expr ')'
+  number :: Exp <- ds:[0-9]+ { Lit (read (chunkToString ds)) }
+|]
 ```
 
-## Grammar size
+That declares three things: `type ArithEnv s`, the signature
+`arith :: Stream s => Grammar s (ArithEnv s) Exp`, and `arith` itself.  Run
+it with `parse arith "1+2*3"`.
 
-The nullability and FIRST set of every rule are computed by GHC while it
-type-checks the grammar, so a grammar's size shows up as compile time.  A
-FIRST set is a type-level list of non-terminal names kept in **alphabetical
-order**:
+A rule's **result type** is the one thing the grammar does not determine — it
+comes from the Haskell in the semantic action — which is what the `:: T`
+annotations are for.  They are claims, and GHC checks them: `Grammar` demands
+`Rules s env env`, so an annotation that disagrees with what the body returns
+is a type error.
 
+`pegRules` remains, for a rule set that is only part of a grammar or that is
+combined with hand-written `PExp` combinators.  It needs the environment
+written out by hand; `examples/Compat.hs` and `examples/Patterns.hs` show
+that style.  See `examples/Arith.hs` and `examples/Layout.hs` for the
+generated one.
+
+## Grammar size, and what is checked where
+
+A grammar's size shows up as compile time, because every reference in it is a
+constraint GHC has to solve against the environment.  An entry of that
+environment is a rule's name and the type it returns:
+
 ```haskell
 type CalcEnv =
-  '[ '("expr" , 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr)
-   , '("term" , 'EnvEntry ('MkTy 'False '["atom", "unary"])         Expr)
-   , '("unary", 'EnvEntry ('MkTy 'False '["atom"])                  Expr)
-   , '("atom" , 'EnvEntry ('MkTy 'False '[])                        Expr)
+  '[ '("expr" , 'EnvEntry Expr)
+   , '("term" , 'EnvEntry Expr)
+   , '("unary", 'EnvEntry Expr)
+   , '("atom" , 'EnvEntry Expr)
    ]
 ```
 
-The order is not cosmetic.  It gives a set exactly one spelling, which is what
-lets the union of two FIRST sets be a single merge pass; listing one in some
-other order is a type error naming the first position that disagrees.
+Entries used to carry more: each rule's nullability and its FIRST set, the
+non-terminals that can begin it.  That is what made left recursion a type
+error — an `Acyclic` constraint checked that no rule was in its own FIRST set
+— and it was also, measurably, the entire cost of compiling a large grammar.
+A FIRST set grows with the grammar, so the environment was quadratic in the
+number of rules, and each of the two reference constraints per rule was solved
+against the whole of it.  Removing it took a 64-rule grammar from 15 s to 2 s,
+and a 128-rule one from more than two minutes to 5 s.  `bench-compile/` has
+the measurements.
 
-That merge nests one type-family reduction per element of the result, so a
-grammar with a FIRST set of more than about a hundred non-terminals hits GHC's
-default reduction limit and reports `Reduction stack overflow`.  Add
-`-freduction-depth=0` to `ghc-options` if you get there; it is a limit rather
-than a slowdown, and a union of two 128-element sets takes about 0.3 s once it
-is lifted.
+Nullability and FIRST sets are still computed — by `PEG.Analysis`, in ordinary
+Haskell, when the quasi-quoter runs, in 6 ms for a 64-rule grammar.  It is
+what reports left recursion, a nullable repetition, an undefined non-terminal
+or a duplicate rule **from the splice**, naming the rule and the chain of head
+references that closes the cycle:
+
+```
+Arith.hs:8:13: error: [GHC-39584]
+    • pegRules:
+      left-recursive non-terminal: expr
+        the cycle is expr -> term -> factor -> expr
+        a PEG cannot backtrack into a committed choice, so this rule
+        would not consume input before calling itself
+```
+
+So the checks divide like this:
+
+| what | checked by | when |
+|---|---|---|
+| a reference names a rule that exists, at the right type | GHC | every compilation |
+| a rule's `:: T` annotation matches what its body returns | GHC | every compilation |
+| left recursion, nullable repetition, duplicate rule | `PEG.Analysis` | at the splice |
+
+The second half of that table is the trade.  A `Rules` chain assembled by hand
+from `RCons`, without a quasi-quoter, is checked for reference errors only: a
+rule that begins with itself compiles and loops.  And `pegRules` analyses its
+block open-world, since two blocks can be combined, so left recursion that
+closes *across* two blocks is reported by neither it nor GHC.  Writing the
+grammar as one `pegGrammar` closes both gaps — it is closed-world, so every
+reference resolves and every cycle is visible — and it is also the fastest to
+compile, because it knows each rule's position and emits the membership proof
+instead of a `KnownMember` search.
+
+Since nothing recomputes what `PEG.Analysis` concludes, the
+`typed-peg-analysis` test-suite checks it against a separate statement of what
+nullability and a FIRST set mean, over the grammars in `examples/` and a few
+hundred generated ones.
 
 ## Patterns
 
diff --git a/bench/Bench/Peg.hs b/bench/Bench/Peg.hs
--- a/bench/Bench/Peg.hs
+++ b/bench/Bench/Peg.hs
@@ -62,14 +62,14 @@
 readInt ds = Lit (read (chunkToString ds))
 
 type ArithEnv =
-  '[ '("expr"  , 'EnvEntry ('MkTy 'False '["factor", "number", "term"]) Exp)
-   , '("term"  , 'EnvEntry ('MkTy 'False '["factor", "number"])         Exp)
-   , '("factor", 'EnvEntry ('MkTy 'False '["number"])                   Exp)
-   , '("number", 'EnvEntry ('MkTy 'False '[])                           Exp)
+  '[ '("expr"  , 'EnvEntry Exp)
+   , '("term"  , 'EnvEntry Exp)
+   , '("factor", 'EnvEntry Exp)
+   , '("number", 'EnvEntry Exp)
    ]
 
 {-# INLINABLE arith #-}
-arith :: Stream s => Grammar s ArithEnv _ Exp
+arith :: Stream s => Grammar s ArithEnv Exp
 arith =
   Grammar
     [pegRules|
@@ -87,13 +87,13 @@
 --------------------------------------------------------------------------------
 
 type CsvEnv =
-  '[ '("csv", 'EnvEntry ('MkTy 'False '["num", "row"]) [[Int]])
-   , '("row", 'EnvEntry ('MkTy 'False '["num"])        [Int])
-   , '("num", 'EnvEntry ('MkTy 'False '[])             Int)
+  '[ '("csv", 'EnvEntry [[Int]])
+   , '("row", 'EnvEntry [Int])
+   , '("num", 'EnvEntry Int)
    ]
 
 {-# INLINABLE csv #-}
-csv :: Stream s => Grammar s CsvEnv _ [[Int]]
+csv :: Stream s => Grammar s CsvEnv [[Int]]
 csv =
   Grammar
     [pegRules|
@@ -113,12 +113,12 @@
 -- The environment is parameterised by the stream: @ident@ is a character
 -- class, so its result is a chunk of the input.
 type IdentEnv s =
-  '[ '("idents", 'EnvEntry ('MkTy 'False '["ident"]) [s])
-   , '("ident" , 'EnvEntry ('MkTy 'False '[])        s)
+  '[ '("idents", 'EnvEntry [s])
+   , '("ident" , 'EnvEntry s)
    ]
 
 {-# INLINABLE idents #-}
-idents :: Stream s => Grammar s (IdentEnv s) _ [s]
+idents :: Stream s => Grammar s (IdentEnv s) [s]
 idents =
   Grammar
     [pegRules|
@@ -149,20 +149,20 @@
 orEmpty (Just xs) = xs
 
 type JsonEnv =
-  '[ '("json"   , 'EnvEntry ('MkTy 'False '["array","number","object","strlit","value","ws"]) JValue)
-   , '("value"  , 'EnvEntry ('MkTy 'False '["array","number","object","strlit"])              JValue)
-   , '("object" , 'EnvEntry ('MkTy 'False '[])                                                JValue)
-   , '("members", 'EnvEntry ('MkTy 'False '["pair","strlit"])                    [(String, JValue)])
-   , '("pair"   , 'EnvEntry ('MkTy 'False '["strlit"])                             (String, JValue))
-   , '("array"  , 'EnvEntry ('MkTy 'False '[])                                                JValue)
-   , '("elems"  , 'EnvEntry ('MkTy 'False '["array","number","object","strlit","value"])    [JValue])
-   , '("strlit" , 'EnvEntry ('MkTy 'False '[])                                                String)
-   , '("number" , 'EnvEntry ('MkTy 'False '[])                                                JValue)
-   , '("ws"     , 'EnvEntry ('MkTy 'True  '[])                                                    ())
+  '[ '("json"   , 'EnvEntry JValue)
+   , '("value"  , 'EnvEntry JValue)
+   , '("object" , 'EnvEntry JValue)
+   , '("members", 'EnvEntry [(String, JValue)])
+   , '("pair"   , 'EnvEntry (String, JValue))
+   , '("array"  , 'EnvEntry JValue)
+   , '("elems"  , 'EnvEntry [JValue])
+   , '("strlit" , 'EnvEntry String)
+   , '("number" , 'EnvEntry JValue)
+   , '("ws"     , 'EnvEntry ())
    ]
 
 {-# INLINABLE json #-}
-json :: Stream s => Grammar s JsonEnv _ JValue
+json :: Stream s => Grammar s JsonEnv JValue
 json =
   Grammar
     [pegRules|
@@ -196,18 +196,18 @@
 
 -- @(!'"' .)*@ is a compound repetition, so it still yields a @['Char']@ ...
 type QuotedNotEnv =
-  '[ '("qs", 'EnvEntry ('MkTy 'False '["q"]) [String])
-   , '("q" , 'EnvEntry ('MkTy 'False '[])    String)
+  '[ '("qs", 'EnvEntry [String])
+   , '("q" , 'EnvEntry String)
    ]
 
 -- ... whereas @[^"]*@ is a character class and yields a chunk.
 type QuotedClsEnv s =
-  '[ '("qs", 'EnvEntry ('MkTy 'False '["q"]) [s])
-   , '("q" , 'EnvEntry ('MkTy 'False '[])    s)
+  '[ '("qs", 'EnvEntry [s])
+   , '("q" , 'EnvEntry s)
    ]
 
 {-# INLINABLE quotedNot #-}
-quotedNot :: Stream s => Grammar s QuotedNotEnv _ [String]
+quotedNot :: Stream s => Grammar s QuotedNotEnv [String]
 quotedNot =
   Grammar
     [pegRules|
@@ -217,7 +217,7 @@
     (nt @"qs")
 
 {-# INLINABLE quotedCls #-}
-quotedCls :: Stream s => Grammar s (QuotedClsEnv s) _ [s]
+quotedCls :: Stream s => Grammar s (QuotedClsEnv s) [s]
 quotedCls =
   Grammar
     [pegRules|
diff --git a/examples/Arith.hs b/examples/Arith.hs
--- a/examples/Arith.hs
+++ b/examples/Arith.hs
@@ -1,9 +1,8 @@
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE QuasiQuotes           #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE PartialTypeSignatures #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE QuasiQuotes      #-}
+{-# LANGUAGE TemplateHaskell  #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators    #-}
 
 module Arith
   ( Exp (..)
@@ -14,7 +13,7 @@
   ) where
 
 import PEG
-import PEG.QQ (pegRules)
+import PEG.QQ (pegGrammar)
 
 data Exp
   = Lit Int
@@ -51,29 +50,29 @@
 addOp l ('/', r) = Div l r
 addOp _ (c  , _) = error ("addOp: unexpected operator " ++ show c)
 
-type ArithEnv =
-  '[ '("expr"  , 'EnvEntry ('MkTy 'False '["factor", "number", "term"]) Exp)
-   , '("term"  , 'EnvEntry ('MkTy 'False '["factor", "number"])         Exp)
-   , '("factor", 'EnvEntry ('MkTy 'False '["number"])                   Exp)
-   , '("number", 'EnvEntry ('MkTy 'False '[])                           Exp)
-   ]
-
--- | Polymorphic in the stream, so the same grammar can be run over 'String',
--- 'Data.Text.Text' and 'Data.ByteString.ByteString'.  Note the cost: this is
--- a function of a 'Stream' dictionary rather than a constant, so the compiled
--- parser is not shared between calls.  Bind a monomorphic parser
+-- | The environment, the signature and the grammar are all declared by the
+-- quasi-quoter.  A rule's result type is the one thing the grammar does not
+-- determine, which is what the @:: T@ annotations are for; left recursion and
+-- the rest are checked by 'PEG.Analysis' at the splice.
+--
+-- The annotations are still claims that GHC checks, not assertions:
+-- 'PEG.Grammar.Grammar' demands @Rules s env env@, so an annotation that
+-- disagrees with what the rule body actually returns is a type error here.
+--
+-- Being polymorphic in the stream has a cost: this is a function of a
+-- 'Stream' dictionary rather than a constant, so the compiled parser is not
+-- shared between calls.  Bind a monomorphic parser
 -- (@arithString = parse arith :: String -> Result String Exp@) where that
 -- matters.
-arith :: Stream s => Grammar s ArithEnv _ Exp
-arith =
-  Grammar
-    [pegRules|
-       expr   <- t:term ts:(o:[+-] u:term)* { foldl addOp t ts }
-       term   <- f:factor fs:(o:[*/] g:factor)*
-                   { foldl (\acc (op, r) -> addOp acc (op, r)) f fs }
-       factor <- n:number
-               / '(' e:expr ')'
-               / '-' f:factor { Neg f }
-       number <- ds:[0-9]+ { Lit (read (chunkToString ds) :: Int) }
-    |]
-    (nt @"expr")
+[pegGrammar|
+  %name  arith
+  %start expr
+
+  expr   :: Exp <- t:term ts:(o:[+-] u:term)* { foldl addOp t ts }
+  term   :: Exp <- f:factor fs:(o:[*/] g:factor)*
+                     { foldl (\acc (op, r) -> addOp acc (op, r)) f fs }
+  factor :: Exp <- n:number
+                 / '(' e:expr ')'
+                 / '-' f:factor { Neg f }
+  number :: Exp <- ds:[0-9]+ { Lit (read (chunkToString ds) :: Int) }
+|]
diff --git a/examples/Compat.hs b/examples/Compat.hs
--- a/examples/Compat.hs
+++ b/examples/Compat.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE OverloadedStrings      #-}
-{-# LANGUAGE PartialTypeSignatures  #-}
 {-# LANGUAGE QuasiQuotes            #-}
 {-# LANGUAGE RankNTypes             #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 
 -- | A differential test: it renders the complete 'Result' (value, consumed
 -- prefix and remaining suffix) for a fixed battery of inputs.
@@ -81,11 +79,11 @@
 -- reaches them.  @!c*@ can never succeed, because the star matches the empty
 -- run.
 type SpanEnv s =
-  '[ '("digits", 'EnvEntry ('MkTy 'True  '[]) s)
-   , '("digits1", 'EnvEntry ('MkTy 'False '[]) s)
+  '[ '("digits", 'EnvEntry s)
+   , '("digits1", 'EnvEntry s)
    ]
 
-spanG :: Stream s => Grammar s (SpanEnv s) _ (s, s)
+spanG :: Stream s => Grammar s (SpanEnv s) (s, s)
 spanG =
   Grammar
     [pegRules|
@@ -96,10 +94,10 @@
 
 -- @!'x'+ .@ accepts any character that is not an @x@; @!'x'* .@ accepts
 -- nothing at all.
-notSpan1G :: Stream s => Grammar s '[] _ Char
+notSpan1G :: Stream s => Grammar s '[] Char
 notSpan1G = Grammar RNil [pegExpr| !'x'+ c:. |]
 
-notSpanG :: Stream s => Grammar s '[] _ Char
+notSpanG :: Stream s => Grammar s '[] Char
 notSpanG = Grammar RNil [pegExpr| !'x'* c:. |]
 
 spanCases :: [String]
diff --git a/examples/Layout.hs b/examples/Layout.hs
--- a/examples/Layout.hs
+++ b/examples/Layout.hs
@@ -1,9 +1,8 @@
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE QuasiQuotes           #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE PartialTypeSignatures #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE QuasiQuotes      #-}
+{-# LANGUAGE TemplateHaskell  #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators    #-}
 
 module Layout
   ( DoStmt (..)
@@ -13,43 +12,38 @@
   ) where
 
 import PEG
-import PEG.QQ (pegExpr, pegRules)
+import PEG.QQ (pegGrammar)
 
 data DoStmt
   = Atom   String
   | Nested [DoStmt]
   deriving (Eq, Show)
 
--- | The environment is parameterised by the stream, because @name@ is a
--- character class and so produces a chunk of the input rather than a
--- 'String'.  Any rule whose result is a chunk pushes @s@ into the
--- environment this way.
-type DoEnv s =
-  '[ '("doexp" , 'EnvEntry ('MkTy 'False '[])                               [DoStmt])
-   , '("istmts", 'EnvEntry ('MkTy 'False '["doexp", "name", "stmt", "ws"]) [DoStmt])
-   , '("stmts" , 'EnvEntry ('MkTy 'False '["ws"])                          [DoStmt])
-   , '("stmt"  , 'EnvEntry ('MkTy 'False '["doexp", "name"])               DoStmt)
-   , '("name"  , 'EnvEntry ('MkTy 'False '[])                              s)
-   , '("ws"    , 'EnvEntry ('MkTy 'True  '[])                              ())
-   ]
+-- | @name@ is a character class, so its result is a chunk of the input rather
+-- than a 'String' — which is why its annotation is @s@ and why the generated
+-- environment takes the stream as a parameter.
+--
+-- @ws@ has neither a label nor an action, so it returns @()@: that is the
+-- DSL's rule for a rule body, and the annotation has to agree with it.  A
+-- start expression is different — @%start ws d:doexp ws !.@ returns what its
+-- one labelled item returns.
+[pegGrammar|
+  %name  doExp
+  %env   DoEnv
+  %start ws d:doexp ws !.
 
-doExp :: Stream s => Grammar s (DoEnv s) _ [DoStmt]
-doExp =
-  Grammar
-    [pegRules|
-       doexp  <- "do" b:(i:istmts / j:stmts)
+  doexp  :: [DoStmt] <- "do" b:(i:istmts / j:stmts)
 
-       istmts <- ss:(ws st:|s:stmt|)+^>
+  istmts :: [DoStmt] <- ss:(ws st:|s:stmt|)+^>
 
-       stmts  <- r:(ws '{' ws s:stmt ss:(ws ';' ws t:stmt)* ws '}' { s : ss })^~
+  stmts  :: [DoStmt] <- r:(ws '{' ws s:stmt ss:(ws ';' ws t:stmt)* ws '}' { s : ss })^~
 
-       stmt   <- d:doexp { Nested d } / n:name { Atom (chunkToString n) }
+  stmt   :: DoStmt   <- d:doexp { Nested d } / n:name { Atom (chunkToString n) }
 
-       name   <- cs:[a-z]+
+  name   :: s        <- cs:[a-z]+
 
-       ws     <- [ \t\r\n]*_~
-    |]
-    [pegExpr| ws d:doexp ws !. |]
+  ws     :: ()       <- [ \t\r\n]*_~
+|]
 
 layoutOpts :: Opts
 layoutOpts = defaultOpts { optTokenMode = relD geR }
diff --git a/examples/Patterns.hs b/examples/Patterns.hs
--- a/examples/Patterns.hs
+++ b/examples/Patterns.hs
@@ -3,8 +3,6 @@
 {-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE PartialTypeSignatures #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 
 -- | Worked examples for @peg-patterns.md@.
 --
@@ -31,21 +29,30 @@
 
 -- | Zero or more layout characters.  A character class, so this compiles to a
 -- single 'Span' node and returns a chunk of the input.
-ws :: PExp s env ('MkTy 'True '[]) s
+ws :: PExp s env s
 ws = spanOf (fromRanges [(' ', ' '), ('\t', '\t'), ('\r', '\r'), ('\n', '\n')])
 
 -- | Run @p@, then consume /trailing/ whitespace only.
-lexeme :: PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a
+--
+-- A combinator over expressions is an ordinary polymorphic function.  It did
+-- not use to be: when a 'PExp' carried its nullability and FIRST set in a
+-- fourth index, this had to be written
+--
+-- @
+-- lexeme :: PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a
+-- @
+--
+-- and every combinator built on it had to restate the nesting exactly.  See
+-- "PEG.Type" for where those indices went.
+lexeme :: PExp s env a -> PExp s env a
 lexeme p = (\x _ -> x) <$>. p <*>. ws
 
 -- | End of input: nothing can follow.
-eof :: PExp s env ('MkTy 'True '[]) ()
+eof :: PExp s env ()
 eof = Not AnyChar
 
 -- | Leading whitespace, then @p@, then end of input.
-fully :: PExp s env ty a
-      -> PExp s env (SeqTy ('MkTy 'True '[])
-                           (SeqTy ty ('MkTy 'True '[]))) a
+fully :: PExp s env a -> PExp s env a
 fully p = (\_ x _ -> x) <$>. ws <*>. p <*>. eof
 
 --------------------------------------------------------------------------------
@@ -60,7 +67,7 @@
 -- The negative lookahead is the whole pattern: @keyword "negate"@ fails on
 -- @negatex@ because an identifier character follows.  In a backtracking
 -- combinator library this needs @try@; in a PEG it is just @!@.
-keyword :: String -> PExp s env ('MkTy 'False '[]) ()
+keyword :: String -> PExp s env ()
 keyword k = (\_ _ -> ()) <$>. stringNE k <*>. Not (sat identCont)
 
 --------------------------------------------------------------------------------
@@ -121,18 +128,18 @@
 --------------------------------------------------------------------------------
 
 type CalcEnv s =
-  '[ '("expr" , 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr)
-   , '("term" , 'EnvEntry ('MkTy 'False '["atom", "unary"])         Expr)
-   , '("unary", 'EnvEntry ('MkTy 'False '["atom"])                  Expr)
-   , '("atom" , 'EnvEntry ('MkTy 'False '[])                        Expr)
+  '[ '("expr" , 'EnvEntry Expr)
+   , '("term" , 'EnvEntry Expr)
+   , '("unary", 'EnvEntry Expr)
+   , '("atom" , 'EnvEntry Expr)
    ]
 
 -- | The classic expression language.
 --
 -- Note what is /not/ here: no @try@, no left recursion, and no rule that can
--- loop.  @expr <- expr '+' term@ would be rejected by 'PEG.Grammar.Acyclic'
--- at compile time with a type error naming @expr@.
-calc :: Stream s => Grammar s (CalcEnv s) _ Expr
+-- loop.  @expr <- expr '+' term@ would be rejected by 'PEG.Analysis' when the
+-- @pegRules@ block below is spliced, naming @expr@ and the cycle.
+calc :: Stream s => Grammar s (CalcEnv s) Expr
 calc =
   Grammar
     [pegRules|
@@ -148,9 +155,9 @@
 
 -- | The same pattern inside a quasi-quoted grammar: a string literal followed
 -- by a negative lookahead on the identifier-continuation class.
-type KwEnv = '[ '("kw", 'EnvEntry ('MkTy 'False '[]) String) ]
+type KwEnv = '[ '("kw", 'EnvEntry String) ]
 
-kwG :: Stream s => Grammar s KwEnv _ String
+kwG :: Stream s => Grammar s KwEnv String
 kwG = Grammar [pegRules| kw <- k:"negate" ![a-zA-Z0-9_]  { k } |] (nt @"kw")
 
 --------------------------------------------------------------------------------
@@ -163,9 +170,9 @@
 --------------------------------------------------------------------------------
 
 type OpEnv =
-  '[ '("op", 'EnvEntry ('MkTy 'False '[]) (Expr -> Expr -> Expr)) ]
+  '[ '("op", 'EnvEntry (Expr -> Expr -> Expr)) ]
 
-addOp :: Stream s => Grammar s OpEnv _ (Expr -> Expr -> Expr)
+addOp :: Stream s => Grammar s OpEnv (Expr -> Expr -> Expr)
 addOp = Grammar [pegRules| op <- '+' { Add } / '-' { Sub } |] (nt @"op")
 
 --------------------------------------------------------------------------------
@@ -173,12 +180,12 @@
 --------------------------------------------------------------------------------
 
 type ProgEnv s =
-  '[ '("prog" , 'EnvEntry ('MkTy 'False '["asgn"]) [Asgn])
-   , '("asgn" , 'EnvEntry ('MkTy 'False '[])       Asgn)
-   , '("expr" , 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr)
-   , '("term" , 'EnvEntry ('MkTy 'False '["atom", "unary"])         Expr)
-   , '("unary", 'EnvEntry ('MkTy 'False '["atom"])                  Expr)
-   , '("atom" , 'EnvEntry ('MkTy 'False '[])                        Expr)
+  '[ '("prog" , 'EnvEntry [Asgn])
+   , '("asgn" , 'EnvEntry Asgn)
+   , '("expr" , 'EnvEntry Expr)
+   , '("term" , 'EnvEntry Expr)
+   , '("unary", 'EnvEntry Expr)
+   , '("atom" , 'EnvEntry Expr)
    ]
 
 -- | @a := 1; b := a * 2@
@@ -187,7 +194,7 @@
 -- illustrates is the one PEG newcomers get wrong: in an ordered choice the
 -- longer alternative must come first, because the first success wins and
 -- there is no backtracking into a committed branch.
-prog :: Stream s => Grammar s (ProgEnv s) _ [Asgn]
+prog :: Stream s => Grammar s (ProgEnv s) [Asgn]
 prog =
   Grammar
     [pegRules|
diff --git a/peg-patterns.md b/peg-patterns.md
--- a/peg-patterns.md
+++ b/peg-patterns.md
@@ -11,11 +11,13 @@
 - **Ordered choice is committed.** Once an alternative succeeds, a PEG never
   reconsiders it. There is no `try`, because there is nothing to undo — but the
   order in which you write alternatives becomes part of the specification.
-- **Left recursion is a type error**, not a discipline to remember. The
-  `Acyclic` constraint is checked when you construct a `Grammar`.
-- **The grammar's shape is written down in a type.** The `Env` records every
-  rule's nullability, FIRST set and result type. Several of the paper's
-  patterns become things the compiler enforces rather than things you adopt.
+- **Left recursion is rejected when you write the grammar**, not a discipline
+  to remember. `PEG.Analysis` runs inside the quasi-quoter and reports it,
+  naming the rule and the cycle.
+- **The grammar's shape is written down in a type.** The `Env` records what
+  every rule returns, so a reference to a rule that does not exist, or at the
+  wrong type, is a type error. Several of the paper's patterns become things
+  the compiler enforces rather than things you adopt.
 
 Every code fragment below is compiled: it lives in
 [`examples/Patterns.hs`](examples/Patterns.hs) and runs as part of
@@ -55,20 +57,23 @@
 
 and observing that it loops. Section 2 is then about the rewrite that fixes it.
 
-In typed-peg you cannot write it in the first place. Each rule's type carries
-its FIRST set, and `Grammar` demands `Acyclic env`:
+In typed-peg you cannot write it in the first place. The quasi-quoter
+computes each rule's FIRST set as it splices the grammar, and rejects one that
+contains its own rule:
 
 ```
 expr <- e:expr '+' t:term { Add e t }
 ```
 
 ```
-Left-recursive non-terminal: "expr"
-Its head set already contains itself: ["expr", "term"]
-Violates the acyclicity condition i `notElem` Gamma(i).F.
+    • pegRules:
+      left-recursive non-terminal: expr
+        the cycle is expr -> expr
+        a PEG cannot backtrack into a committed choice, so this rule
+        would not consume input before calling itself
 ```
 
-reported at the `Grammar` constructor, before anything runs.
+reported at the quasi-quoter, before anything runs.
 
 **Pattern.** Do not treat left-recursion removal as a step you perform. Write
 the grammar; if it compiles, no rule can loop on its own head. The rewrite
@@ -117,10 +122,10 @@
 
 ```haskell
 type CalcEnv s =
-  '[ '("expr" , 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr)
-   , '("term" , 'EnvEntry ('MkTy 'False '["atom", "unary"])         Expr)
-   , '("unary", 'EnvEntry ('MkTy 'False '["atom"])                  Expr)
-   , '("atom" , 'EnvEntry ('MkTy 'False '[])                        Expr)
+  '[ '("expr" , 'EnvEntry Expr)
+   , '("term" , 'EnvEntry Expr)
+   , '("unary", 'EnvEntry Expr)
+   , '("atom" , 'EnvEntry Expr)
    ]
 ```
 
@@ -140,17 +145,21 @@
 makes a misplaced operator a type error, exactly as in the paper — at the cost
 of an AST with one constructor per layer.
 
-Note the FIRST set columns. They are not decoration: `'["atom", "term", "unary"]` says that entering `expr` can immediately enter any of those, and it
-is what the acyclicity check consumes. Getting them wrong is a compile error,
-so they double as a checked comment.
+An entry used to carry the rule's nullability and FIRST set as well —
+`'("expr", 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr)` — which
+is what the acyclicity check consumed. It was also the whole cost of compiling
+a large grammar, because a FIRST set grows with the grammar and the
+environment is solved against once per reference; see `bench-compile/`. The
+sets are now computed by `PEG.Analysis` at the splice instead, so what is left
+to write down is the part only you know: what the rule returns.
 
-A FIRST set is written in **alphabetical order**, and with no repeats. The
-order is not a matter of taste: it is what makes a set have exactly one
-spelling, which in turn lets the compiler take the union of two FIRST sets in
-one merge pass instead of re-scanning one of them for every element of the
-other. Write `'["atom", "term", "unary"]`, not `'["term", "unary", "atom"]`;
-the latter is a type error naming the first position that disagrees.
+Better still, do not write it down at all. `pegGrammar` generates the
+environment from the same `:: T` annotations:
 
+```
+expr :: Expr <- t:term ts:(o:[+-] u:term)* { chainl t ts }
+```
+
 ### 1.4 Precedence tables: absent, but not impossible
 
 *(Willis & Wu, Pattern 1c: Precedence Tables.)*
@@ -203,21 +212,24 @@
 position reporting and makes it ambiguous who is responsible for a given space.
 
 ```haskell
-ws :: PExp s env ('MkTy 'True '[]) s
+ws :: PExp s env s
 ws = spanOf (fromRanges [(' ', ' '), ('\t', '\t'), ('\r', '\r'), ('\n', '\n')])
 
-lexeme :: PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a
+lexeme :: PExp s env a -> PExp s env a
 lexeme p = (\x _ -> x) <$>. p <*>. ws
 
-eof :: PExp s env ('MkTy 'True '[]) ()
+eof :: PExp s env ()
 eof = Not AnyChar
 
-fully :: PExp s env ty a
-      -> PExp s env (SeqTy ('MkTy 'True '[])
-                           (SeqTy ty ('MkTy 'True '[]))) a
+fully :: PExp s env a -> PExp s env a
 fully p = (\_ x _ -> x) <$>. ws <*>. p <*>. eof
 ```
 
+These are ordinary polymorphic functions. They did not use to be: while a
+`PExp` carried its nullability and FIRST set in a fourth index, `lexeme` had
+to be written `PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a`
+and everything built on it had to restate the nesting exactly.
+
 ```
 "12"     => OK "12"
 "  12  " => OK "12"
@@ -272,7 +284,7 @@
 In a PEG it is just `!`:
 
 ```haskell
-keyword :: String -> PExp s env ('MkTy 'False '[]) ()
+keyword :: String -> PExp s env ()
 keyword k = (\_ _ -> ()) <$>. stringNE k <*>. Not (sat identCont)
 ```
 
@@ -358,9 +370,9 @@
 just a rule whose result type is a function:
 
 ```haskell
-type OpEnv = '[ '("op", 'EnvEntry ('MkTy 'False '[]) (Expr -> Expr -> Expr)) ]
+type OpEnv = '[ '("op", 'EnvEntry (Expr -> Expr -> Expr)) ]
 
-addOp :: Stream s => Grammar s OpEnv _ (Expr -> Expr -> Expr)
+addOp :: Stream s => Grammar s OpEnv (Expr -> Expr -> Expr)
 addOp = Grammar [pegRules| op <- '+' { Add } / '-' { Sub } |] (nt @"op")
 ```
 
@@ -471,7 +483,7 @@
 ```
 Couldn't match expected type 's' with actual type '[Char]'
   's' is a rigid type variable bound by the inferred type of
-    identG :: Stream s => Grammar s (IdEnv s) (MkTy False '["ident"]) s
+    identG :: Stream s => Grammar s (IdEnv s) s
 ```
 
 So the idiom quietly ties a grammar to one stream. The fix is also faster,
@@ -494,14 +506,16 @@
 
 ```haskell
 type CalcEnv s =
-  '[ '("expr" , 'EnvEntry ('MkTy 'False '["atom", "term", "unary"]) Expr)
+  '[ '("expr" , 'EnvEntry Expr)
    , ...
    ]
 ```
 
-Each entry states three things: whether the rule can match the empty string,
-which non-terminals it can enter first, and what it produces. All three are
-verified against the rule bodies.
+Each entry states what the rule produces, and that is verified against the
+rule body. Entries used to state two things more — whether the rule can match
+the empty string, and which non-terminals it can enter first — which is what
+made left recursion a type error and what made a large grammar slow to
+compile; both now happen at the splice instead.
 
 **Pattern.** Write the `Env` before the rules, as you would write a signature
 before a function. When a rule's FIRST set surprises you, that is usually the
diff --git a/src/PEG.hs b/src/PEG.hs
--- a/src/PEG.hs
+++ b/src/PEG.hs
@@ -1,21 +1,30 @@
 -- | Type-safe PEG (Parsing Expression Grammar) parser combinators.
 --
--- Grammar non-terminals are indexed at the type level by their nullability and
--- FIRST sets. Left-recursive grammars are rejected at compile time via a
--- 'GHC.TypeLits.TypeError'.
+-- Grammar non-terminals are checked at the type level against an environment
+-- that binds each rule's name to the type it returns, so a reference to a
+-- rule that does not exist, or a use of one at the wrong type, is a type
+-- error.  Left recursion, a repetition that cannot consume input, an
+-- undefined non-terminal and a duplicate rule are rejected by the
+-- quasi-quoter when the grammar is spliced; see "PEG.Grammar" for exactly
+-- what is checked where.
 --
 -- == Quick start
 --
 -- @
 -- import PEG
--- import PEG.QQ (pegRules)
+-- import PEG.QQ (pegGrammar)
 -- @
 --
--- 1. Declare the grammar environment as a type-level list of @(name, entry)@
---    pairs (see 'PEG.Type.Env').
--- 2. Build a 'Grammar' using 'pegRules' (quasi-quoter) or the combinators in
---    "PEG.Syntax".
--- 3. Run the grammar on a 'String' with 'parse' or 'parseWith'.
+-- 1. Write the grammar with the 'PEG.QQ.pegGrammar' quasi-quoter, giving each
+--    rule its result type.  It declares the environment, the grammar and its
+--    signature.
+-- 2. Run the grammar on a 'String' with 'parse' or 'parseWith'.
+--
+-- The environment can also be declared by hand — a type-level list of
+-- @(name, entry)@ pairs, see 'PEG.Type.Env' — and the rules built with
+-- 'PEG.QQ.pegRules' or the combinators in "PEG.Syntax".  That is what
+-- 'PEG.QQ.pegGrammar' generates, and it stays supported; it is only more to
+-- write and slower to compile.
 --
 -- See the @examples/@ directory for complete working grammars.
 module PEG
diff --git a/src/PEG/Analysis.hs b/src/PEG/Analysis.hs
new file mode 100644
--- /dev/null
+++ b/src/PEG/Analysis.hs
@@ -0,0 +1,362 @@
+-- | Nullability, FIRST sets and well-formedness, computed in Haskell.
+--
+-- This module is the value-level twin of "PEG.TyLevel" and "PEG.Grammar":
+-- it computes, from the grammar DSL's syntax tree, exactly the environment
+-- that GHC would otherwise derive by reducing 'PEG.Syntax.SeqTy',
+-- 'PEG.Syntax.ChoiceTy' and 'PEG.TyLevel.Union' while type-checking a
+-- 'PEG.Grammar.Rules' value.
+--
+-- == Why it moved here
+--
+-- It used to be a type-level computation, and that is what made left
+-- recursion a type error.  It was billed to every compilation of every module
+-- that mentioned the grammar, and its cost grew sharply with the grammar's
+-- size: every entry of the environment carried a FIRST set, so the
+-- environment was quadratic in the number of rules, and each of the two
+-- reference constraints per rule had to be solved against it.  A 64-rule
+-- grammar cost GHC 15 s.  The same fixpoint runs here, at splice time and
+-- once, in 6 ms for that grammar and 286 ms for one of 256 rules.  See
+-- @bench-compile/@ for the measurements and "PEG.Type" for the trade.
+--
+-- == This module is now load-bearing
+--
+-- While the FIRST sets were also in the types, this module could be wrong
+-- without being dangerous: GHC recomputed everything and rejected a grammar
+-- whose environment did not match.  It no longer does.  A left-recursive
+-- grammar that this module accepts is a parser that loops.
+--
+-- What replaces the type checker is @tests/typed-peg-analysis@, which checks
+-- the results here against a straightforward statement of what they mean —
+-- nullability as a least fixpoint, and a FIRST set as the transitive closure
+-- of the one-step head relation — over the grammars in @examples/@ and over a
+-- few hundred generated ones.
+--
+-- == The fixpoint
+--
+-- Nullability and FIRST are both computed as the least solution of the
+-- equations the type families state.  For a grammar without left recursion
+-- that solution is the only one, which is why GHC can find it by unification
+-- alone; for a left-recursive grammar the least solution is the one that puts
+-- a non-terminal in its own FIRST set, which is precisely what
+-- 'PEG.Grammar.Acyclic' rejects.
+module PEG.Analysis
+  ( Ty (..)
+  , RuleEnv
+  , Diagnostic (..)
+  , World (..)
+  , analyse
+  , analyseWith
+  , exprTy
+  , seqTy
+  , choiceTy
+  , insertSym
+  , unionSym
+  , renderEnv
+  , renderDiagnostic
+  , spannable
+  ) where
+
+import Data.List (foldl1', nub)
+import Data.Maybe (fromMaybe)
+
+import PEG.QQ.Syntax (Def (..), Item (..), PExpr (..))
+
+-- | The value-level image of 'PEG.Type.Ty': a nullability flag and a FIRST
+-- set of non-terminal names.
+--
+-- The FIRST set is kept strictly sorted by 'compare', which agrees with
+-- 'GHC.TypeLits.CmpSymbol' on the identifiers the DSL admits.  Sortedness is
+-- what makes the set canonical, so that a generated environment is
+-- /syntactically/ the type GHC computes rather than merely an equivalent one.
+data Ty = Ty
+  { tyNullable :: !Bool
+  , tyFirst    :: ![String]
+  } deriving (Eq, Show)
+
+-- | A grammar environment in definition order: the value-level image of
+-- 'PEG.Type.Env', minus the result types, which only the type checker knows.
+type RuleEnv = [(String, Ty)]
+
+-- | Something that makes the grammar ill-formed.
+--
+-- Each of these used to be a type error — or, in the case of 'NullableStar',
+-- a type error whose message mentioned neither the rule nor the repetition
+-- that caused it.  Reporting them here means naming the rule, and is now the
+-- only place any of them is reported.
+data Diagnostic
+  = -- | A non-terminal is in its own FIRST set, with the chain of head
+    -- references that puts it there.
+    LeftRecursive String [String]
+  | -- | @e*@ or @e+@ where @e@ can match the empty string: the repetition
+    -- would not consume input and the parser would not terminate.
+    NullableStar String
+  | -- | A rule body references a name that no rule defines; the second field
+    -- lists the names that are defined.
+    UndefinedNT String [String]
+  | -- | Two rules with the same name.
+    DuplicateRule String
+  deriving (Eq, Show)
+
+--------------------------------------------------------------------------------
+-- Sorted sets, mirroring PEG.TyLevel
+--------------------------------------------------------------------------------
+
+-- | The image of 'PEG.TyLevel.ConsIfAbsent'.
+insertSym :: String -> [String] -> [String]
+insertSym x [] = [x]
+insertSym x (y:ys) = case compare x y of
+  LT -> x : y : ys
+  EQ -> y : ys
+  GT -> y : insertSym x ys
+
+-- | The image of 'PEG.TyLevel.Union': a single merge pass over two sorted
+-- sets.
+unionSym :: [String] -> [String] -> [String]
+unionSym [] ys = ys
+unionSym xs [] = xs
+unionSym (x:xs) (y:ys) = case compare x y of
+  LT -> x : unionSym xs (y:ys)
+  EQ -> x : unionSym xs ys
+  GT -> y : unionSym (x:xs) ys
+
+-- | The image of 'PEG.Syntax.SeqTy'.
+seqTy :: Ty -> Ty -> Ty
+seqTy t1 t2 =
+  Ty (tyNullable t1 && tyNullable t2)
+     (unionSym (tyFirst t1) (if tyNullable t1 then tyFirst t2 else []))
+
+-- | The image of 'PEG.Syntax.ChoiceTy'.
+choiceTy :: Ty -> Ty -> Ty
+choiceTy t1 t2 =
+  Ty (tyNullable t1 || tyNullable t2)
+     (unionSym (tyFirst t1) (tyFirst t2))
+
+nullTy, termTy :: Ty
+nullTy = Ty True  []
+termTy = Ty False []
+
+--------------------------------------------------------------------------------
+-- The type of one expression
+--------------------------------------------------------------------------------
+
+-- | The 'Ty' of a DSL expression, given the 'Ty' of every non-terminal it may
+-- reference.
+--
+-- This has to follow @PEG.QQ.translateExpr@ case for case, including its
+-- optimisations: a repetition of a bare class, character or dot compiles to
+-- 'PEG.Syntax.Span' or 'PEG.Syntax.Span1' rather than to
+-- 'PEG.Syntax.Star', and those two have different FIRST sets from the generic
+-- form.  A case that disagrees with the translation produces an environment
+-- GHC will reject.
+exprTy :: (String -> Ty) -> PExpr -> Ty
+exprTy look = go
+  where
+    go (EChar _)        = termTy
+    go EDot             = termTy
+    go (EClass _ _)     = termTy
+    go (EString s)
+      | null s          = nullTy          -- pureP ""
+      | otherwise       = termTy
+    -- NTGo: the reference adds its own name to the rule's FIRST set.
+    go (ENT n)          = let t = look n
+                          in Ty (tyNullable t) (insertSym n (tyFirst t))
+    -- Both lookaheads are 'Not' at bottom, which is nullable and keeps the
+    -- FIRST set of its operand.  @&e@ is @Not (Not e)@.
+    go (EAnd e)         = Ty True (tyFirst (go e))
+    go (ENot e)         = Ty True (tyFirst (go e))
+    go (EOpt e)         = choiceTy (go e) nullTy
+    go (EStar e)
+      | spannable e     = nullTy          -- spanOf
+      | otherwise       = Ty True (tyFirst (go e))
+    go (EPlus e)
+      | spannable e     = termTy          -- spanOf1
+      | otherwise       = let t = go e in seqTy t (Ty True (tyFirst t))
+    go (EIndent _ e)    = go e
+    go (EPos _ e)       = go e
+    go (EAlign e)       = go e
+    go (EChoice es)     = foldl1' choiceTy (map go es)
+    go (ESeq [] _)      = nullTy          -- pureP
+    go (ESeq items _)   = foldl1' seqTy [ go e | Item _ e <- items ]
+
+-- | Does a repetition of this expression compile to a 'PEG.Syntax.Span'?
+spannable :: PExpr -> Bool
+spannable (EClass _ _) = True
+spannable (EChar _)    = True
+spannable EDot         = True
+spannable _            = False
+
+--------------------------------------------------------------------------------
+-- The grammar
+--------------------------------------------------------------------------------
+
+-- | Is this the whole grammar, or part of one?
+--
+-- 'PEG.Grammar.RCons' is exported, so two quasi-quoted blocks can be spliced
+-- into one rule set and a rule in the first may reference a rule in the
+-- second.  A block analysed 'Open' therefore treats an unknown name as
+-- opaque — non-nullable, with an empty FIRST set — instead of reporting it.
+--
+-- Under-approximating a FIRST set loses a 'LeftRecursive' or a
+-- 'NullableStar'; over-approximating would reject a grammar that is fine.
+-- The second is the worse failure, so an unknown name is treated as opaque —
+-- but nothing catches what that loses, since the type checker no longer
+-- computes FIRST sets of its own.  Left recursion that closes across two
+-- blocks spliced together is reported by nobody; a grammar written as a
+-- single 'PEG.QQ.pegGrammar' is 'Closed' and has no such gap.  The
+-- environment returned for an 'Open' block is, for the same reason, not the
+-- grammar's environment: only the diagnostics are meaningful.
+data World = Closed | Open
+  deriving (Eq, Show)
+
+-- | Compute the environment of a complete set of rules, or report why it has
+-- none.
+--
+-- All diagnostics of a kind are reported together, so a grammar with three
+-- undefined non-terminals names all three rather than one per recompilation.
+analyse :: [Def] -> Either [Diagnostic] RuleEnv
+analyse = analyseWith Closed
+
+-- | 'analyse', over a whole grammar or a fragment of one.
+analyseWith :: World -> [Def] -> Either [Diagnostic] RuleEnv
+analyseWith world defs
+  | not (null dups)      = Left dups
+  | not (null undefs)    = Left undefs
+  | not (null illFormed) = Left illFormed
+  | not (null leftRecs)  = Left leftRecs
+  | otherwise            = Right env
+  where
+    names = [ n | Def n _ _ <- defs ]
+
+    dups = [ DuplicateRule n
+           | n <- nub names, length (filter (== n) names) > 1 ]
+
+    undefs = case world of
+      Open   -> []
+      Closed -> [ UndefinedNT n names
+                | n <- nub (concatMap (refs . body) defs), n `notElem` names ]
+      where body (Def _ _ e) = e
+
+    -- Kleene iteration from the empty environment.  Every clause of 'exprTy'
+    -- is monotone in the environment and the lattice is finite, so this
+    -- terminates; it is the least solution of the equations the type families
+    -- state.
+    env = fix [ (n, Ty False []) | n <- names ]
+      where
+        fix m = let m' = step m in if m' == m then m else fix m'
+        step m = [ (n, exprTy (at m) e) | Def n _ e <- defs ]
+
+    at m n = fromMaybe (Ty False []) (lookup n m)
+
+    -- A repetition must consume input, which 'PEG.Syntax.Star' states as a
+    -- non-nullable operand.  Checking it here names the rule it is in.
+    illFormed = [ NullableStar n | Def n _ e <- defs, hasNullableRep (at env) e ]
+
+    -- Every rule on a cycle is left-recursive, and reporting each of them
+    -- prints the same cycle once per entry point.  Two paths that are
+    -- rotations of each other are the same cycle, so only the first is kept.
+    leftRecs = dedupe [] [ LeftRecursive n (cycleFrom n)
+                         | (n, t) <- env, n `elem` tyFirst t ]
+      where
+        dedupe _ [] = []
+        dedupe seen (d@(LeftRecursive _ path) : rest)
+          | key `elem` seen = dedupe seen rest
+          | otherwise       = d : dedupe (key : seen) rest
+          where key = canonical path
+        dedupe seen (d : rest) = d : dedupe seen rest
+
+    -- A cycle is written as @n -> ... -> n@; drop the repeated end and turn
+    -- it so that it starts at its least name.
+    canonical path = case reverse (drop 1 (reverse path)) of
+      []    -> []
+      nodes -> minimum [ rotate k nodes | k <- [0 .. length nodes - 1] ]
+      where rotate k xs = drop k xs ++ take k xs
+
+    -- The FIRST set is already transitive, so it says /that/ a rule is
+    -- left-recursive but not /how/.  The chain is recovered from the graph of
+    -- direct head references, which is 'exprTy' again with the environment
+    -- cut back to nullability alone.
+    heads n = tyFirst (exprTy (\k -> Ty (tyNullable (at env k)) []) (bodyOf n))
+
+    bodyOf n = case [ e | Def m _ e <- defs, m == n ] of
+                 (e:_) -> e
+                 []    -> ESeq [] Nothing
+
+    cycleFrom n = go [n] n
+      where
+        go path cur = case [ h | h <- heads cur, h == n ] of
+          (_:_) -> reverse (n : path)
+          []    -> case [ p | h <- heads cur
+                            , h `notElem` path
+                            , n `elem` tyFirst (at env h)
+                            , p <- [go (h : path) h]
+                            , not (null p) ] of
+                     (p:_) -> p
+                     []    -> []
+
+-- | Every non-terminal a body references, at any position.
+refs :: PExpr -> [String]
+refs (ENT n)       = [n]
+refs (EAnd e)      = refs e
+refs (ENot e)      = refs e
+refs (EOpt e)      = refs e
+refs (EStar e)     = refs e
+refs (EPlus e)     = refs e
+refs (EIndent _ e) = refs e
+refs (EPos _ e)    = refs e
+refs (EAlign e)    = refs e
+refs (EChoice es)  = concatMap refs es
+refs (ESeq its _)  = concat [ refs e | Item _ e <- its ]
+refs _             = []
+
+-- | Does the expression contain a repetition whose operand is nullable?
+hasNullableRep :: (String -> Ty) -> PExpr -> Bool
+hasNullableRep look = go
+  where
+    go (EStar e)     = (not (spannable e) && tyNullable (exprTy look e)) || go e
+    go (EPlus e)     = (not (spannable e) && tyNullable (exprTy look e)) || go e
+    go (EAnd e)      = go e
+    go (ENot e)      = go e
+    go (EOpt e)      = go e
+    go (EIndent _ e) = go e
+    go (EPos _ e)    = go e
+    go (EAlign e)    = go e
+    go (EChoice es)  = any go es
+    go (ESeq its _)  = or [ go e | Item _ e <- its ]
+    go _             = False
+
+--------------------------------------------------------------------------------
+-- Rendering
+--------------------------------------------------------------------------------
+
+-- | Render an environment as the source of a 'PEG.Type.Env' type, given a
+-- result type for each rule.
+--
+-- Used to tell a user what to write while the environment still has to be
+-- written by hand.  An entry no longer carries a FIRST set, so the analysis
+-- contributes only the rule names and their order; what used to be the
+-- interesting half of this function is now something no one has to write
+-- down.
+renderEnv :: (String -> String) -> RuleEnv -> String
+renderEnv resultOf entries = unlines (zipWith line prefixes entries) ++ "   ]"
+  where
+    prefixes = "  '[ " : repeat "   , "
+    line p (n, _) =
+      p ++ "'(" ++ show n ++ ", 'EnvEntry " ++ resultOf n ++ ")"
+
+-- | A one-paragraph explanation of a 'Diagnostic', in the shape the
+-- quasi-quoter reports it.
+renderDiagnostic :: Diagnostic -> String
+renderDiagnostic (LeftRecursive n path) =
+  "left-recursive non-terminal: " ++ n
+    ++ (if null path then "" else "\n  the cycle is " ++ arrows path)
+    ++ "\n  a PEG cannot backtrack into a committed choice, so this rule\n"
+    ++ "  would not consume input before calling itself"
+  where arrows = foldr1 (\a b -> a ++ " -> " ++ b)
+renderDiagnostic (NullableStar n) =
+  "in rule " ++ n ++ ": a repetition whose operand can match the empty\n"
+    ++ "  string; it would not consume input and the parse would not terminate"
+renderDiagnostic (UndefinedNT n defined) =
+  "undefined non-terminal: " ++ n
+    ++ "\n  the grammar defines " ++ unwords defined
+renderDiagnostic (DuplicateRule n) =
+  "the rule " ++ n ++ " is defined twice"
diff --git a/src/PEG/Grammar.hs b/src/PEG/Grammar.hs
--- a/src/PEG/Grammar.hs
+++ b/src/PEG/Grammar.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE ConstraintKinds      #-}
 {-# LANGUAGE DataKinds            #-}
 {-# LANGUAGE FlexibleContexts     #-}
 {-# LANGUAGE GADTs                #-}
@@ -7,24 +6,50 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- | Grammar type and the acyclicity constraint.
+-- | Grammar and rule-set types.
 --
 -- A 'Grammar' bundles a set of named rules ('Rules') and a start expression.
--- The 'Acyclic' constraint is checked at the definition site of every
--- 'Grammar' value: if any non-terminal is left-recursive (its own name appears
--- in its own FIRST set), GHC emits a 'GHC.TypeLits.TypeError' naming the
--- offending non-terminal.
+--
+-- == Where left recursion is caught
+--
+-- In the quasi-quoters, and only there.  'PEG.QQ.pegGrammar' and
+-- 'PEG.QQ.pegRules' run "PEG.Analysis" at splice time: it computes each
+-- rule's nullability and FIRST set and rejects a grammar in which any rule
+-- can begin with itself, naming the rule and the chain of head references
+-- that closes the cycle.  It also rejects a repetition of something nullable,
+-- an undefined non-terminal and a duplicate rule.  That happens once, when
+-- the grammar is written, in milliseconds.
+--
+-- It used to happen again, and differently, on every compilation of every
+-- module that mentioned the grammar: entries of the environment carried the
+-- FIRST set as type-level data and an @Acyclic@ constraint checked that no
+-- rule was in its own.  "PEG.Type" records what that cost — it was the whole
+-- cost of a large grammar — and why it is gone.
+--
+-- What is given up is the case the splice cannot see:
+--
+-- * A 'Rules' chain assembled by hand from 'RCons', or a 'Grammar' built
+--   around one, is checked for /reference/ errors only.  A rule that begins
+--   with itself compiles, and loops when run.
+-- * 'PEG.QQ.pegRules' analyses its block open-world, because 'RCons' lets two
+--   blocks be combined and a name the block does not define may be defined by
+--   the other one.  Left recursion that closes /across/ two blocks is
+--   therefore reported by neither.  A grammar written as one
+--   'PEG.QQ.pegGrammar' has no such gap: it is closed-world, so every
+--   reference is resolved and every cycle is visible.
+--
+-- Prefer 'PEG.QQ.pegGrammar'.  It is the only way to write a grammar that is
+-- checked completely, and it is also the fastest to compile, because it knows
+-- each rule's position and emits 'PEG.Syntax.ntw' with the membership proof
+-- rather than a 'PEG.Member.KnownMember' search.
 module PEG.Grammar
   ( Rules (..)
   , Grammar (..)
-  , Acyclic
   ) where
 
-import Data.Kind    (Constraint, Type)
-import GHC.TypeLits (ErrorMessage (..), Symbol, TypeError)
+import Data.Kind    (Type)
 
 import PEG.Syntax  (Name, PExp)
-import PEG.TyLevel (Elem)
 import PEG.Type
 
 -- | A typed, heterogeneous list of named grammar rules.
@@ -35,38 +60,25 @@
 data Rules (s :: Type) (env :: Env) (defs :: Env) where
   RNil  :: Rules s env '[]
   RCons :: Name n
-        -> PExp s env ty a
+        -> PExp s env a
         -> Rules s env rest
-        -> Rules s env ('(n, 'EnvEntry ty a) ': rest)
-
-type family Acyclic (env :: Env) :: Constraint where
-  Acyclic '[]                                      = ()
-  Acyclic ('(s, 'EnvEntry ('MkTy _ f) _) ': rest) =
-    (NotLeftRec s (Elem s f) f, Acyclic rest)
-
-type family NotLeftRec (s :: Symbol) (b :: Bool)
-                       (f :: [Symbol]) :: Constraint where
-  NotLeftRec _ 'False _ = ()
-  NotLeftRec s 'True  f =
-    TypeError ('Text "Left-recursive non-terminal: " ':<>: 'ShowType s
-         ':$$: 'Text "Its head set already contains itself: "
-               ':<>: 'ShowType f
-         ':$$: 'Text "Violates the acyclicity condition i `notElem` Gamma(i).F.")
+        -> Rules s env ('(n, 'EnvEntry a) ': rest)
 
 -- | A complete PEG grammar over the stream @s@: a set of mutually recursive
 -- rules and a start expression.
 --
+-- The @Rules s env env@ field is what ties the two halves together: every
+-- rule's body is checked against the same environment the rule set defines,
+-- so a reference can only name a rule that exists and only at the type that
+-- rule has.
+--
 -- A 'Grammar' is monomorphic in its stream.  To reuse one grammar across
 -- several stream types, give it a signature of the form
--- @forall s. 'PEG.Stream.Stream' s => Grammar s Env ty a@ — but note that
+-- @forall s. 'PEG.Stream.Stream' s => Grammar s Env a@ — but note that
 -- doing so turns the value into a function of a dictionary, so the compiled
 -- parser is no longer shared between calls.  Prefer a monomorphic top-level
 -- signature.
---
--- Constructing a 'Grammar' value discharges the 'Acyclic' constraint, so
--- any left-recursion in @env@ becomes a compile-time type error.
-data Grammar (s :: Type) (env :: Env) (startTy :: Ty) (startA :: Type) where
-  Grammar :: Acyclic env
-          => Rules s env env
-          -> PExp s env startTy startA
-          -> Grammar s env startTy startA
+data Grammar (s :: Type) (env :: Env) (a :: Type) where
+  Grammar :: Rules s env env
+          -> PExp s env a
+          -> Grammar s env a
diff --git a/src/PEG/Member.hs b/src/PEG/Member.hs
--- a/src/PEG/Member.hs
+++ b/src/PEG/Member.hs
@@ -18,15 +18,19 @@
 -- materialised from type information at runtime, enabling non-terminal lookup
 -- during parsing.
 --
--- == Why the 'PEG.Type.Ty' is not an index
+-- == Why the class has only the indices it has
 --
--- The witness deliberately does /not/ record the non-terminal's
--- 'PEG.Type.Ty'.  Resolving @KnownMember s env a@ walks @env@ one instance at
--- a time, and every index of the class is carried along — and re-normalised —
--- at each of those steps.  A 'PEG.Type.Ty' carries a FIRST set, so an index
--- for it makes each step cost @O(|env|)@ instead of @O(1)@.  Nothing needs
--- it: 'Here' binds the entry's @ty@ existentially, which is enough to pull
--- the matching rule out of a rule table.
+-- Resolving @KnownMember s env a@ walks @env@ one instance at a time, and
+-- every index of the class is carried along — and re-normalised — at each of
+-- those steps.  An index whose size grows with the grammar therefore makes
+-- each step cost @O(|env|)@ instead of @O(1)@.  Entries used to carry a FIRST
+-- set for exactly that reason, and keeping it out of this class was worth a
+-- large constant; it is now out of the environment altogether (see
+-- "PEG.Type"), so the same discipline is cheap to keep and worth keeping.
+--
+-- Better still is not to search at all: 'PEG.Syntax.ntw' takes the witness
+-- rather than deriving it, which is what a quasi-quoter emits, since a splice
+-- knows every rule's position.
 module PEG.Member
   ( Member (..)
   , KnownMember (..)
@@ -41,7 +45,7 @@
 -- | @'Member' s env a@ witnesses that @env@ binds the name @s@ to a rule
 -- returning @a@, and records /where/ in @env@ that binding is.
 data Member (s :: Symbol) (env :: Env) (a :: Type) where
-  Here  :: Member s ('(s, 'EnvEntry ty a) ': rest) a
+  Here  :: Member s ('(s, 'EnvEntry a) ': rest) a
   There :: Member s rest a -> Member s (e ': rest) a
 
 class KnownMember (s :: Symbol) (env :: Env) (a :: Type) where
@@ -62,9 +66,9 @@
 class KnownMemberStep (o :: Ordering) (s :: Symbol) (env :: Env) (a :: Type) where
   memberStep :: Proxy o -> Member s env a
 
--- The entry is taken apart in the instance head, so @ty@ is bound by
--- matching and never has to be threaded through the class.
-instance (s ~ t) => KnownMemberStep 'EQ s ('(t, 'EnvEntry ty a) ': rest) a where
+-- The entry is taken apart in the instance head, so the result type is bound
+-- by matching and never has to be threaded through the class.
+instance (s ~ t) => KnownMemberStep 'EQ s ('(t, 'EnvEntry a) ': rest) a where
   memberStep _ = Here
 
 instance KnownMember s rest a => KnownMemberStep 'LT s ('(t, e) ': rest) a where
diff --git a/src/PEG/Parse.hs b/src/PEG/Parse.hs
--- a/src/PEG/Parse.hs
+++ b/src/PEG/Parse.hs
@@ -132,20 +132,20 @@
   }
 
 -- | Run a grammar with 'defaultOpts'.
-parse :: Stream s => Grammar s env ty a -> s -> Result s a
+parse :: Stream s => Grammar s env a -> s -> Result s a
 parse = parseWith defaultOpts
 {-# INLINABLE parse #-}
-{-# SPECIALIZE parse :: Grammar String env ty a -> String -> Result String a #-}
-{-# SPECIALIZE parse :: Grammar T.Text env ty a -> T.Text -> Result T.Text a #-}
+{-# SPECIALIZE parse :: Grammar String env a -> String -> Result String a #-}
+{-# SPECIALIZE parse :: Grammar T.Text env a -> T.Text -> Result T.Text a #-}
 {-# SPECIALIZE parse
-      :: Grammar B.ByteString env ty a -> B.ByteString -> Result B.ByteString a #-}
+      :: Grammar B.ByteString env a -> B.ByteString -> Result B.ByteString a #-}
 
 -- | Run a grammar with custom 'Opts'.
 --
 -- Partially applying this to the options and the grammar yields a compiled
 -- parser; see the note at the top of this module.
-parseWith :: forall s env ty a.
-             Stream s => Opts -> Grammar s env ty a -> s -> Result s a
+parseWith :: forall s env a.
+             Stream s => Opts -> Grammar s env a -> s -> Result s a
 parseWith opts g = run
   where
     step = compileGrammar (optTabWidth opts) g
@@ -156,11 +156,11 @@
       (# | (# a, st #) #) -> OK a (takeS (stOff st) input) (stInput st)
 {-# INLINABLE parseWith #-}
 {-# SPECIALIZE parseWith
-      :: Opts -> Grammar String env ty a -> String -> Result String a #-}
+      :: Opts -> Grammar String env a -> String -> Result String a #-}
 {-# SPECIALIZE parseWith
-      :: Opts -> Grammar T.Text env ty a -> T.Text -> Result T.Text a #-}
+      :: Opts -> Grammar T.Text env a -> T.Text -> Result T.Text a #-}
 {-# SPECIALIZE parseWith
-      :: Opts -> Grammar B.ByteString env ty a
+      :: Opts -> Grammar B.ByteString env a
       -> B.ByteString -> Result B.ByteString a #-}
 
 --------------------------------------------------------------------------------
@@ -174,7 +174,7 @@
   CNil  :: CRules s env '[]
   CCons :: Step s a
         -> CRules s env rest
-        -> CRules s env ('(n, 'EnvEntry ty a) ': rest)
+        -> CRules s env ('(n, 'EnvEntry a) ': rest)
 
 clookup :: Member n defs a -> CRules s env defs -> Step s a
 clookup Here      (CCons f _)    = f
@@ -185,8 +185,8 @@
 -- The traversal resolves every non-terminal reference to the corresponding
 -- compiled rule, so at parse time a non-terminal costs one indirect call
 -- instead of a walk down the rule list.
-compileGrammar :: forall s env ty a.
-                  Stream s => Int -> Grammar s env ty a -> Step s a
+compileGrammar :: forall s env a.
+                  Stream s => Int -> Grammar s env a -> Step s a
 compileGrammar tw (Grammar rules start) = compileE tw table start
   where
     table :: CRules s env env
@@ -201,11 +201,11 @@
 -- per-character path stops being allocation-free.  Callers using another
 -- stream should mark their own monomorphic parser bindings INLINABLE.
 {-# SPECIALIZE compileGrammar
-      :: Int -> Grammar String env ty a -> Step String a #-}
+      :: Int -> Grammar String env a -> Step String a #-}
 {-# SPECIALIZE compileGrammar
-      :: Int -> Grammar T.Text env ty a -> Step T.Text a #-}
+      :: Int -> Grammar T.Text env a -> Step T.Text a #-}
 {-# SPECIALIZE compileGrammar
-      :: Int -> Grammar B.ByteString env ty a -> Step B.ByteString a #-}
+      :: Int -> Grammar B.ByteString env a -> Step B.ByteString a #-}
 
 -- | Does this class avoid the two characters whose column advance is not
 -- simply @+1@?  When it does, the column after a matched run is the column
@@ -213,8 +213,8 @@
 simpleCS :: CharSet -> Bool
 simpleCS cs = not (memberCS '\n' cs) && not (memberCS '\t' cs)
 
-compileE :: forall s env ty a.
-            Stream s => Int -> CRules s env env -> PExp s env ty a -> Step s a
+compileE :: forall s env a.
+            Stream s => Int -> CRules s env env -> PExp s env a -> Step s a
 compileE tw table = comp
   where
     -- Select the stream operations once per compiled grammar.  Leaving them
@@ -228,7 +228,7 @@
     !packS   = packString    :: String -> s
     !emptyS  = packS []
 
-    comp :: forall t b. PExp s env t b -> Step s b
+    comp :: forall b. PExp s env b -> Step s b
 
     comp (Pure x) = \_ st -> (# | (# x, st #) #)
 
@@ -245,10 +245,14 @@
     comp (Span  cs) = spanChunk (\c -> memberCS c cs) (simpleCS cs) False
     comp (Span1 cs) = spanChunk (\c -> memberCS c cs) (simpleCS cs) True
 
-    -- 'ty' and 'a' come from the constructor's own equality
-    -- @Lookup n env ~ 'EnvEntry ty a@, so no type family has to be reduced
+    -- 'a' comes from the constructor's own equality
+    -- @Lookup n env ~ 'EnvEntry a@, so no type family has to be reduced
     -- here at all.
     comp (NT @n _) = clookup (member @n @env) table
+
+    -- The witness came with the reference, so there is no search at all:
+    -- neither here nor, more to the point, in the type checker.
+    comp (NTW _ w) = clookup w table
 
     -- Neither this nor 'Map' below allocates: the intermediate results travel
     -- in registers, so a quasi-quoted rule of @n@ items costs @n@ calls and
diff --git a/src/PEG/QQ.hs b/src/PEG/QQ.hs
--- a/src/PEG/QQ.hs
+++ b/src/PEG/QQ.hs
@@ -28,390 +28,99 @@
 module PEG.QQ
   ( pegExpr
   , pegRules
+  , pegGrammar
   ) where
 
 import Control.Monad              (foldM)
-import Data.List                  (nub)
+import Data.List                  (elemIndex, nub)
 import Language.Haskell.TH        (Exp (..), Pat (..), Q)
 import qualified Language.Haskell.TH      as TH
 import Language.Haskell.TH.Quote  (QuasiQuoter (..))
 
 import PEG
-import PEG.QQ.HsExp (parseHsExp)
-
-data Def = Def String PExpr
-  deriving Show
-
-data Item = Item (Maybe String) PExpr
-  deriving Show
-
-data PExpr
-  = EChoice  [PExpr]
-  | ESeq     [Item] (Maybe String)
-  | EAnd     PExpr
-  | ENot     PExpr
-  | EOpt     PExpr
-  | EStar    PExpr
-  | EPlus    PExpr
-  | EChar    Char
-  | EString  String
-  | EClass   Bool [(Char,Char)]   -- ^ 'True' when the class is negated.
-  | EDot
-  | ENT      String
-  | EIndent  RelS PExpr
-  | EPos     RelS PExpr
-  | EAlign   PExpr
-  deriving Show
-
-data RelS
-  = RGt
-  | RGe
-  | REq
-  | RAny
-  | ROffset Int
-  | RNamed  String
-  deriving Show
-
-type P a = String -> Either String (a, String)
-
-errorAt :: String -> String -> Either String a
-errorAt msg s = Left $ msg ++ " at: " ++ show (take 30 s)
-
-spaces :: String -> String
-spaces []         = []
-spaces ('#':xs)   = spaces (drop 1 (dropWhile (/= '\n') xs))
-spaces (c:xs)
-  | c == ' ' || c == '\t' || c == '\n' || c == '\r' = spaces xs
-  | otherwise = c:xs
-
-tok :: String -> P ()
-tok t s = case stripPrefix t (spaces s) of
-  Just r  -> Right ((), r)
-  Nothing -> errorAt ("expected " ++ show t) s
-  where
-    stripPrefix [] xs                 = Just xs
-    stripPrefix (p:ps) (x:xs) | p==x  = stripPrefix ps xs
-    stripPrefix _ _                   = Nothing
-
-ident :: P String
-ident s0 = case spaces s0 of
-  (c:xs) | isIdStart c ->
-    let (rest, leftover) = span isIdCont xs
-    in Right (c:rest, leftover)
-  s -> errorAt "expected identifier" s
-  where
-    isIdStart c = c == '_' || (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
-    isIdCont c  = isIdStart c || (c >= '0' && c <= '9')
-
-charLit :: P Char
-charLit s0 = case spaces s0 of
-  ('\'':xs) -> do (c, r1) <- escChar '\'' xs
-                  case r1 of
-                    ('\'':r2) -> Right (c, r2)
-                    _         -> errorAt "expected closing '" r1
-  s         -> errorAt "expected character literal" s
-
-strLit :: P String
-strLit s0 = case spaces s0 of
-  ('"':xs) -> loop xs
-  s        -> errorAt "expected string literal" s
-  where
-    loop ('"':r) = Right ("", r)
-    loop r0      = do (c, r1) <- escChar '"' r0
-                      (cs, r2) <- loop r1
-                      pure (c:cs, r2)
-
-escChar :: Char -> P Char
-escChar _ ('\\':e:xs) = case e of
-  'n'  -> Right ('\n', xs)
-  't'  -> Right ('\t', xs)
-  'r'  -> Right ('\r', xs)
-  '\\' -> Right ('\\', xs)
-  '\'' -> Right ('\'', xs)
-  '"'  -> Right ('"',  xs)
-  '['  -> Right ('[',  xs)
-  ']'  -> Right (']',  xs)
-  '0'  -> Right ('\0', xs)
-  '^'  -> Right ('^',  xs)
-  _    -> errorAt ("unknown escape \\" ++ [e]) xs
-escChar stopC (c:xs)
-  | c == stopC = errorAt "unexpected close quote" (c:xs)
-  | otherwise  = Right (c, xs)
-escChar _ [] = Left "unexpected end of input in literal"
-
--- | A character class.  A leading @^@ negates it, as in POSIX; write
--- @[\\^]@ for a class containing the caret itself.
-classLit :: P (Bool, [(Char, Char)])
-classLit s0 = case spaces s0 of
-  ('[':'^':xs) -> do
-    (rs, r) <- loop xs
-    if null rs
-      then errorAt "empty negated character class" s0
-      else Right ((True, rs), r)
-  ('[':xs)     -> do
-    (rs, r) <- loop xs
-    Right ((False, rs), r)
-  s            -> errorAt "expected character class" s
-  where
-    loop (']':r) = Right ([], r)
-    loop []      = Left "unterminated character class"
-    loop r0      = do
-      (c1, r1) <- escChar ']' r0
-      case r1 of
-        ('-':']':r2) -> pure ([(c1, c1), ('-', '-')], r2)
-        ('-':r2) ->
-          do (c2, r3) <- escChar ']' r2
-             (rs, r4) <- loop r3
-             pure ((c1, c2) : rs, r4)
-        _ ->
-          do (rs, r2) <- loop r1
-             pure ((c1, c1) : rs, r2)
-
-actionLit :: P String
-actionLit s0 = case spaces s0 of
-  ('{':xs) -> go (1 :: Int) ' ' [] xs
-  s        -> errorAt "expected a semantic action" s
-  where
-    go _ _ _ [] = Left "unterminated semantic action: missing '}'"
-    go n prev acc s = case s of
-      ('{':'-':r) -> do
-        (com, r') <- blockComment (1 :: Int) r
-        go n '}' (revApp ("{-" ++ com) acc) r'
-      ('"':r) -> do
-        (str, r') <- literalBody '"' r
-        go n '"' (revApp ('"' : str) acc) r'
-      ('\'':r) | not (isIdChar prev) -> do
-        (ch, r') <- literalBody '\'' r
-        go n '\'' (revApp ('\'' : ch) acc) r'
-      ('{':r) -> go (n + 1) '{' ('{' : acc) r
-      ('}':r) | n == 1    -> Right (reverse acc, r)
-              | otherwise -> go (n - 1) '}' ('}' : acc) r
-      (c:_) | c `elem` symChars ->
-        let (sym, r) = span (`elem` symChars) s
-        in if all (== '-') sym && length sym >= 2
-             then let (line, r') = span (/= '\n') r
-                  in go n '\n' (revApp (sym ++ line) acc) r'
-             else go n (last sym) (revApp sym acc) r
-      (c:r) -> go n c (c : acc) r
-
-    isIdChar c = c == '_' || c == '\''
-              || (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
-              || (c >= '0' && c <= '9')
-
-    literalBody _ [] = Left "unterminated literal in a semantic action"
-    literalBody q ('\\':c:r)     = do (b, r') <- literalBody q r
-                                      Right ('\\' : c : b, r')
-    literalBody q (c:r) | c == q = Right ([c], r)
-    literalBody q (c:r)          = do (b, r') <- literalBody q r
-                                      Right (c : b, r')
-
-    blockComment _ []              = Left "unterminated {- -} comment in a semantic action"
-    blockComment k ('-':'}':r)
-      | k == 1                     = Right ("-}", r)
-      | otherwise                  = do (c, r') <- blockComment (k - 1) r
-                                        Right ("-}" ++ c, r')
-    blockComment k ('{':'-':r)     = do (c, r') <- blockComment (k + 1) r
-                                        Right ("{-" ++ c, r')
-    blockComment k (c:r)           = do (c', r') <- blockComment k r
-                                        Right (c : c', r')
-
-    revApp xs acc = reverse xs ++ acc
-
-    symChars = "!#$%&*+./<=>?@\\^|-~:"
-
-parseExpr :: P PExpr
-parseExpr s0 = do
-  (e1, s1) <- parseSeq s0
-  loop [e1] s1
-  where
-    loop acc s = case tok "/" s of
-      Right (_, s') -> do (e, s'') <- parseSeq s'
-                          loop (e:acc) s''
-      Left _        -> case reverse acc of
-        [x] -> Right (x, s)
-        xs  -> Right (EChoice xs, s)
-
-parseSeq :: P PExpr
-parseSeq s0 = loop [] s0
-  where
-    loop acc s = case parseLabelled s of
-      Right (it, s') -> loop (it:acc) s'
-      Left _         -> case actionLit s of
-        Right (act, s') -> Right (ESeq (reverse acc) (Just act), s')
-        Left _          -> Right (ESeq (reverse acc) Nothing,    s)
-
-parseLabelled :: P Item
-parseLabelled s = case label s of
-  Just (l, s1) -> do (e, s2) <- parsePrefix s1
-                     pure (Item (Just l) e, s2)
-  Nothing      -> do (e, s1) <- parsePrefix s
-                     pure (Item Nothing e, s1)
-  where
-    label s' = case ident s' of
-      Right (name, s1) -> case tok ":" s1 of
-        Right (_, s2) -> Just (name, s2)
-        Left _        -> Nothing
-      Left _ -> Nothing
-
-parsePrefix :: P PExpr
-parsePrefix s = case tok "&" s of
-  Right (_, s') -> do (e, s'') <- parseSuffix s'; pure (EAnd e, s'')
-  Left _        -> case tok "!" s of
-    Right (_, s') -> do (e, s'') <- parseSuffix s'; pure (ENot e, s'')
-    Left _        -> parseSuffix s
-
-parseSuffix :: P PExpr
-parseSuffix s = do
-  (p, s1) <- parsePrimary s
-  loop p s1
-  where
-    loop p s1 = case tok "?" s1 of
-      Right (_, s2) -> loop (EOpt p) s2
-      Left _ -> case tok "*" s1 of
-        Right (_, s2) -> loop (EStar p) s2
-        Left _ -> case tok "+" s1 of
-          Right (_, s2) -> loop (EPlus p) s2
-          Left _ -> case indented EIndent "^" p s1 of
-            Right (p', s2) -> loop p' s2
-            Left _ -> case indented EPos "_" p s1 of
-              Right (p', s2) -> loop p' s2
-              Left _         -> Right (p, s1)
-
-    indented con marker p s1 = do
-      (_, s2) <- tok marker s1
-      (r, s3) <- parseRel s2
-      pure (con r p, s3)
-
-parseRel :: P RelS
-parseRel s = case tok ">=" s of
-  Right (_, s1) -> Right (RGe, s1)
-  Left _ -> case tok ">" s of
-    Right (_, s1) -> Right (RGt, s1)
-    Left _ -> case tok "=" s of
-      Right (_, s1) -> Right (REq, s1)
-      Left _ -> case tok "~" s of
-        Right (_, s1) -> Right (RAny, s1)
-        Left _ -> case tok "@" s of
-          Right (_, s1) -> do (name, s2) <- ident s1
-                              pure (RNamed name, s2)
-          Left _ -> case tok "+" s of
-            Right (_, s1) -> case span isDigit (spaces s1) of
-              ([], _)     -> errorAt "expected a number after '+'" s1
-              (ds, s2)    -> Right (ROffset (read ds), s2)
-            Left _ -> errorAt "expected an indentation relation" s
-  where
-    isDigit c = c >= '0' && c <= '9'
-
-parsePrimary :: P PExpr
-parsePrimary s =
-  case tok "(" s of
-    Right (_, s1) -> do (e, s2) <- parseExpr s1
-                        (_, s3) <- tok ")" s2
-                        pure (e, s3)
-    Left _ -> case parseAlign s of
-     Right r -> Right r
-     Left _ -> case tok "." s of
-      Right (_, s1) -> Right (EDot, s1)
-      Left _ -> case charLit s of
-        Right (c, s1) -> Right (EChar c, s1)
-        Left _ -> case strLit s of
-          Right (cs, s1) -> Right (EString cs, s1)
-          Left _ -> case classLit s of
-            Right ((neg, rs), s1) -> Right (EClass neg rs, s1)
-            Left _ -> case ident s of
-              Right (name, s1) ->
-                case tok "<-" s1 of
-                  Right _  -> errorAt "definition where expression expected" s
-                  Left _   -> Right (ENT name, s1)
-              Left _ -> errorAt "expected primary expression" s
-
-parseAlign :: P PExpr
-parseAlign s = do
-  (_, s1) <- tok "|" s
-  (e, s2) <- parseExpr s1
-  if isEmptyExpr e
-    then errorAt "empty alignment: write |e| with a non-empty e" s
-    else do (_, s3) <- tok "|" s2
-            pure (EAlign e, s3)
-  where
-    isEmptyExpr (ESeq [] Nothing) = True
-    isEmptyExpr _                 = False
+import PEG.Analysis  (Diagnostic (..), World (..), analyse, analyseWith,
+                      renderDiagnostic, spannable)
+import PEG.QQ.HsExp  (parseHsExp, parseHsType)
+import PEG.QQ.Syntax (Def (..), Directive (..), Item (..), PExpr (..),
+                      RelS (..), parseDirectives, parseExpr, parseGrammar,
+                      spaces)
 
-parseGrammar :: P [Def]
-parseGrammar s0 = loop [] s0
+-- | Translate a DSL expression, given a way to emit a reference to a
+-- non-terminal.
+--
+-- The two quasi-quoters differ in exactly that: 'pegRules' emits
+-- @nt \@"name"@, which makes GHC search the environment, while 'pegGrammar'
+-- knows every rule's position and emits @ntw \@"name" witness@, which does
+-- not.  Everything else about the translation is shared, so the two cannot
+-- drift.
+translateExprWith :: (String -> Q Exp) -> PExpr -> Q Exp
+translateExprWith ntRef = go
   where
-    loop acc s = case ident s of
-      Left _ -> case spaces s of
-        [] -> Right (reverse acc, "")
-        s' -> errorAt "expected definition or end of input" s'
-      Right (name, s1) -> do
-        (_, s2)  <- tok "<-" s1
-        (e, s3)  <- parseExpr s2
-        loop (Def name e : acc) s3
+    go (EChar c) =
+      [| Term c |]
+    go EDot =
+      [| AnyChar |]
+    go (ENT name) = ntRef name
+    go (EString str)
+      | null str  = [| pureP "" |]
+      | otherwise = [| stringNE str |]
+    go (EClass neg rs)
+      -- A character class becomes a single 'Sat' node holding a compact
+      -- 'PEG.CharSet.CharSet'.  Expanding it into a chain of ordered choices, as
+      -- an earlier version did, made matching one character of @[a-zA-Z0-9_]@
+      -- cost 63 parser steps.
+      | neg       = [| notCharClass rs |]
+      | otherwise = [| charClass rs |]
+    go (EAnd e)  = do
+      e' <- go e
+      [| Not (Not $(pure e')) |]
+    go (ENot e)  = do
+      e' <- go e
+      [| Not $(pure e') |]
+    go (EOpt e)  = do
+      e' <- go e
+      [| opt $(pure e') |]
+    -- A repetition of a single character -- @[a-z]*@, @','+@, @.*@ -- compiles to
+    -- one 'PEG.Syntax.Span' node and produces a /chunk of the input stream/: a
+    -- 'Data.Text.Text' slice rather than a @['Char']@.  Only a bare class, literal
+    -- or dot qualifies; a wrapper such as @[a-z]^>*@ changes the meaning of each
+    -- iteration, so those keep the generic 'Star'.
+    go (EStar (EClass neg rs))
+      | neg       = [| spanOf (notInRanges rs) |]
+      | otherwise = [| spanOf (fromRanges rs) |]
+    go (EStar (EChar c)) = [| spanOf (singletonCS c) |]
+    go (EStar EDot)      = [| spanOf anyCS |]
+    go (EPlus (EClass neg rs))
+      | neg       = [| spanOf1 (notInRanges rs) |]
+      | otherwise = [| spanOf1 (fromRanges rs) |]
+    go (EPlus (EChar c)) = [| spanOf1 (singletonCS c) |]
+    go (EPlus EDot)      = [| spanOf1 anyCS |]
+    go (EStar e) = do
+      e' <- go e
+      [| Star $(pure e') |]
+    go (EPlus e) = do
+      e' <- go e
+      [| plus $(pure e') |]
+    go (EIndent r e) = do
+      e' <- go e
+      [| Indent $(translateRel r) $(pure e') |]
+    go (EPos r e) = do
+      e' <- go e
+      [| Position $(translateRel r) $(pure e') |]
+    go (EAlign e) = do
+      e' <- go e
+      [| Align $(pure e') |]
+    go (EChoice es) = case es of
+      []       -> fail "QQ: empty choice (should be impossible)"
+      (e:rest) -> do
+        e'    <- go e
+        rest' <- mapM go rest
+        foldM (\acc x -> [| $(pure acc) .||. $(pure x) |]) e' rest'
+    go (ESeq items act) = translateSeqWith ntRef items act
 
-translateExpr :: PExpr -> Q Exp
-translateExpr (EChar c) =
-  [| Term c |]
-translateExpr EDot =
-  [| AnyChar |]
-translateExpr (ENT name) =
-  pure $ TH.AppTypeE (TH.VarE 'nt) (TH.LitT (TH.StrTyLit name))
-translateExpr (EString s)
-  | null s    = [| pureP "" |]
-  | otherwise = [| stringNE s |]
-translateExpr (EClass neg rs)
-  -- A character class becomes a single 'Sat' node holding a compact
-  -- 'PEG.CharSet.CharSet'.  Expanding it into a chain of ordered choices, as
-  -- an earlier version did, made matching one character of @[a-zA-Z0-9_]@
-  -- cost 63 parser steps.
-  | neg       = [| notCharClass rs |]
-  | otherwise = [| charClass rs |]
-translateExpr (EAnd e)  = do
-  e' <- translateExpr e
-  [| Not (Not $(pure e')) |]
-translateExpr (ENot e)  = do
-  e' <- translateExpr e
-  [| Not $(pure e') |]
-translateExpr (EOpt e)  = do
-  e' <- translateExpr e
-  [| opt $(pure e') |]
--- A repetition of a single character -- @[a-z]*@, @','+@, @.*@ -- compiles to
--- one 'PEG.Syntax.Span' node and produces a /chunk of the input stream/: a
--- 'Data.Text.Text' slice rather than a @['Char']@.  Only a bare class, literal
--- or dot qualifies; a wrapper such as @[a-z]^>*@ changes the meaning of each
--- iteration, so those keep the generic 'Star'.
-translateExpr (EStar (EClass neg rs))
-  | neg       = [| spanOf (notInRanges rs) |]
-  | otherwise = [| spanOf (fromRanges rs) |]
-translateExpr (EStar (EChar c)) = [| spanOf (singletonCS c) |]
-translateExpr (EStar EDot)      = [| spanOf anyCS |]
-translateExpr (EPlus (EClass neg rs))
-  | neg       = [| spanOf1 (notInRanges rs) |]
-  | otherwise = [| spanOf1 (fromRanges rs) |]
-translateExpr (EPlus (EChar c)) = [| spanOf1 (singletonCS c) |]
-translateExpr (EPlus EDot)      = [| spanOf1 anyCS |]
-translateExpr (EStar e) = do
-  e' <- translateExpr e
-  [| Star $(pure e') |]
-translateExpr (EPlus e) = do
-  e' <- translateExpr e
-  [| plus $(pure e') |]
-translateExpr (EIndent r e) = do
-  e' <- translateExpr e
-  [| Indent $(translateRel r) $(pure e') |]
-translateExpr (EPos r e) = do
-  e' <- translateExpr e
-  [| Position $(translateRel r) $(pure e') |]
-translateExpr (EAlign e) = do
-  e' <- translateExpr e
-  [| Align $(pure e') |]
-translateExpr (EChoice es) = case es of
-  []       -> fail "QQ: empty choice (should be impossible)"
-  (e:rest) -> do
-    e'    <- translateExpr e
-    rest' <- mapM translateExpr rest
-    foldM (\acc x -> [| $(pure acc) .||. $(pure x) |]) e' rest'
-translateExpr (ESeq items act) = translateSeq items act
+-- | Emit @nt \@"name"@: the environment is searched by the type checker.
+ntByName :: String -> Q Exp
+ntByName name = pure (TH.AppTypeE (TH.VarE 'nt) (TH.LitT (TH.StrTyLit name)))
 
 translateRel :: RelS -> Q Exp
 translateRel RGt          = [| gtR |]
@@ -421,8 +130,8 @@
 translateRel (ROffset n)  = [| offsetR n |]
 translateRel (RNamed nm)  = pure (TH.VarE (TH.mkName nm))
 
-translateSeq :: [Item] -> Maybe String -> Q Exp
-translateSeq items act = do
+translateSeqWith :: (String -> Q Exp) -> [Item] -> Maybe String -> Q Exp
+translateSeqWith ntRef items act = do
   let labels = [ l | Item (Just l) _ <- items ]
   case duplicates labels of
     (l:_) -> fail ("QQ: the label " ++ show l
@@ -433,7 +142,7 @@
     Just src -> case parseHsExp src of
       Right e  -> pure e
       Left err -> fail ("QQ: in the semantic action {" ++ src ++ "}: " ++ err)
-  es <- mapM (\(Item _ e) -> translateExpr e) items
+  es <- mapM (\(Item _ e) -> translateExprWith ntRef e) items
   case es of
     []       -> [| pureP $(pure body) |]
     (e:rest) -> do
@@ -450,11 +159,11 @@
 
     duplicates xs = [ x | x <- nub xs, length (filter (== x) xs) > 1 ]
 
-translateRules :: [Def] -> Q Exp
-translateRules [] = [| RNil |]
-translateRules (Def name expr : rest) = do
-  body  <- translateExpr expr
-  rest' <- translateRules rest
+translateRules :: (String -> Q Exp) -> [Def] -> Q Exp
+translateRules _ [] = [| RNil |]
+translateRules ntRef (Def name _ expr : rest) = do
+  body  <- translateExprWith ntRef expr
+  rest' <- translateRules ntRef rest
   let nameProxy = TH.AppTypeE (TH.ConE 'Name) (TH.LitT (TH.StrTyLit name))
   [| RCons $(pure nameProxy) $(pure body) $(pure rest') |]
 
@@ -474,7 +183,7 @@
 pegExprExp src = case parseExpr src of
   Left err     -> fail ("pegExpr: parse error: " ++ err)
   Right (e, rest) -> case spaces rest of
-    []  -> translateExpr e
+    []  -> translateExprWith ntByName e
     leftover -> fail ("pegExpr: unconsumed input: " ++ show (take 30 leftover))
 
 -- | Quasi-quoter for a set of named PEG rules.
@@ -505,4 +214,288 @@
 pegRulesExp :: String -> Q Exp
 pegRulesExp src = case parseGrammar src of
   Left err -> fail ("pegRules: parse error: " ++ err)
-  Right (defs, _) -> translateRules defs
+  Right (defs, _) ->
+    -- Left recursion, a nullable repetition and a duplicate rule, reported
+    -- here because nothing else reports them any more: the FIRST sets that
+    -- @Acyclic@ used to check are no longer in the types.  The block is
+    -- analysed 'Open' because it may be only part of a rule set — see
+    -- 'PEG.Analysis.World' — so a cycle that closes across two blocks is
+    -- caught by neither this nor GHC.  'pegGrammar' has no such gap.
+    case analyseWith Open defs of
+      Left ds -> fail ("pegRules:\n" ++ unlines
+                         -- six spaces, so the body lines up under the bullet
+                         -- GHC puts in front of the first line
+                         [ "      " ++ l | d <- ds, l <- lines (renderDiagnostic d) ])
+      Right _ -> translateRules ntByName defs
+
+--------------------------------------------------------------------------------
+-- pegGrammar: a whole grammar, environment included
+--------------------------------------------------------------------------------
+
+-- | Quasi-quoter for a complete grammar.
+--
+-- Unlike 'pegRules', which is one part of a rule set and can be combined with
+-- another, this owns the whole grammar.  Two things follow from that.
+--
+-- It knows every rule's position in the environment, so it emits
+-- 'PEG.Syntax.ntw' and the membership proof rather than @nt@ and a
+-- 'PEG.Member.KnownMember' search.  That is worth about 2.6x on the compile
+-- time of a 64-rule grammar; see @bench-compile/@.
+--
+-- And it knows the whole grammar is in front of it, so a reference to a name
+-- no rule defines is an error at the splice rather than a type error later.
+--
+-- == In expression position
+--
+-- @
+-- arith :: Stream s => Grammar s ArithEnv _ Exp
+-- arith = [pegGrammar|
+--           %start expr
+--           expr   \<- t:term ts:(o:[+-] u:term)* { foldl addOp t ts }
+--           term   \<- ...
+--         |]
+-- @
+--
+-- == In declaration position
+--
+-- Give each rule its result type and the environment need not be written at
+-- all — the quasi-quoter declares it, along with the grammar and its
+-- signature:
+--
+-- @
+-- [pegGrammar|
+--   %name  arith
+--   %start expr
+--   expr   :: Exp \<- t:term ts:(o:[+-] u:term)* { foldl addOp t ts }
+--   term   :: Exp \<- ...
+-- |]
+-- @
+--
+-- declares @type ArithEnv s@, @arith :: Stream s => Grammar s (ArithEnv s) Exp@
+-- and @arith@ itself.  An entry of the environment is a rule's name and the
+-- type it returns; the type is the one thing the grammar does not determine,
+-- which is what the annotations are for.
+--
+-- == Directives
+--
+-- [@%start@] Required.  The start expression: a non-terminal's name, or any
+--            PEG expression over the grammar's rules.
+-- [@%name@]  Required in declaration position: the name to bind the grammar
+--            to.
+-- [@%env@]   The name of the generated environment synonym.  Defaults to the
+--            grammar's name, capitalised, with @Env@ appended.
+-- [@%stream@] The stream type.  Defaults to a variable @s@ with a
+--            'PEG.Stream.Stream' constraint.
+-- [@%result@] The grammar's result type, for the rare start expression whose
+--            type cannot be read off the rules — one with a semantic action
+--            of its own.
+pegGrammar :: QuasiQuoter
+pegGrammar = QuasiQuoter
+  { quoteExp  = pegGrammarExp
+  , quoteDec  = pegGrammarDec
+  , quotePat  = \_ -> fail "pegGrammar: cannot be used as a pattern"
+  , quoteType = \_ -> fail "pegGrammar: cannot be used as a type"
+  }
+
+-- | A grammar that has been parsed and checked: the pieces both forms need.
+--
+-- The analysis's own result is not among them.  It used to be — the FIRST
+-- sets it computes were written into the environment — and now that entries
+-- carry only a result type, running it is entirely a matter of the
+-- diagnostics it raises.  It is still run, and it is now the only thing that
+-- rejects a left-recursive grammar; see "PEG.Grammar".
+data GrammarSrc = GrammarSrc
+  { gsDirs  :: [Directive]
+  , gsDefs  :: [Def]
+  , gsStart :: PExpr
+  }
+
+gsNames :: GrammarSrc -> [String]
+gsNames gs = [ n | Def n _ _ <- gsDefs gs ]
+
+-- | Parse the header, the rules and the start expression, and run the
+-- analysis over all of them.
+parseGrammarSrc :: String -> Q GrammarSrc
+parseGrammarSrc src = do
+  (dirs, afterDirs) <- orFail (parseDirectives src)
+  -- A mistyped directive is silent otherwise: @%strt expr@ would be reported
+  -- as a missing %start, which points at the wrong thing.
+  case [ k | Directive k _ <- dirs, k `notElem` knownDirectives ] of
+    []    -> pure ()
+    (k:_) -> fail ("pegGrammar: unknown directive %" ++ k
+                     ++ "\n      known directives are "
+                     ++ unwords [ '%' : d | d <- knownDirectives ])
+  (defs, leftover)  <- orFail (parseGrammar afterDirs)
+  case spaces leftover of
+    [] -> pure ()
+    r  -> fail ("pegGrammar: unconsumed input: " ++ show (take 30 r))
+  startSrc <- case directive "start" dirs of
+    Just v  -> pure v
+    Nothing -> fail "pegGrammar: no %start directive"
+  (start0, startRest) <- orFail (parseExpr startSrc)
+  let start = normaliseStart start0
+  case spaces startRest of
+    [] -> pure ()
+    r  -> fail ("pegGrammar: unconsumed input in %start: " ++ show (take 30 r))
+  -- The start expression is a rule body in every way that matters here, so it
+  -- is checked with the others: a name it references and no rule defines is
+  -- reported the same way.
+  case analyse (Def "%start" Nothing start : defs) of
+    Left ds  -> fail ("pegGrammar:\n" ++ unlines
+                        [ "      " ++ l
+                        | d <- ds, l <- lines (renderDiagnostic (unstart d)) ])
+    Right _  -> pure ()
+  pure (GrammarSrc dirs defs start)
+  where
+    orFail = either (\e -> fail ("pegGrammar: parse error: " ++ e)) pure
+
+    -- The start expression is not a rule, so it should not be named as one.
+    unstart (LeftRecursive n p)  = LeftRecursive (rename n) (map rename p)
+    unstart (NullableStar n)     = NullableStar (rename n)
+    unstart (UndefinedNT n ns)   = UndefinedNT n (filter (/= "%start") ns)
+    unstart (DuplicateRule n)    = DuplicateRule (rename n)
+    rename n = if n == "%start" then "the start expression" else n
+
+-- | @%start expr@ means the expression @expr@, not a one-item sequence whose
+-- value is discarded.
+--
+-- Inside a rule, @r \<- term@ with neither a label nor an action does return
+-- @()@ — that is the DSL's rule and it stays.  But a start expression is not
+-- a rule: it is the @(nt \@"expr")@ that used to be written out by hand next
+-- to the rule set, and that returned the rule's value.  A start with a label
+-- or an action of its own is left alone; only a lone unlabelled item is
+-- unwrapped.
+normaliseStart :: PExpr -> PExpr
+normaliseStart (ESeq [Item Nothing e] Nothing) = e
+normaliseStart e                               = e
+
+knownDirectives :: [String]
+knownDirectives = ["start", "name", "env", "stream", "result"]
+
+directive :: String -> [Directive] -> Maybe String
+directive k ds = case [ v | Directive k' v <- ds, k' == k ] of
+  (v:_) -> Just v
+  []    -> Nothing
+
+-- | Emit @ntw \@"name" (There (... Here))@: the proof instead of the search.
+ntByWitness :: [String] -> String -> Q Exp
+ntByWitness names name = case elemIndex name names of
+  Nothing -> fail ("pegGrammar: undefined non-terminal: " ++ name)
+  Just k  -> pure (TH.AppE (TH.AppTypeE (TH.VarE 'ntw)
+                                        (TH.LitT (TH.StrTyLit name)))
+                           (witness k))
+  where
+    witness 0 = TH.ConE 'Here
+    witness k = TH.AppE (TH.ConE 'There) (witness (k - 1))
+
+pegGrammarExp :: String -> Q Exp
+pegGrammarExp src = do
+  gs <- parseGrammarSrc src
+  let ntRef = ntByWitness (gsNames gs)
+  rules <- translateRules ntRef (gsDefs gs)
+  start <- translateExprWith ntRef (gsStart gs)
+  [| Grammar $(pure rules) $(pure start) |]
+
+pegGrammarDec :: String -> Q [TH.Dec]
+pegGrammarDec src = do
+  gs <- parseGrammarSrc src
+  gname <- case directive "name" (gsDirs gs) of
+    Just v  -> pure (TH.mkName v)
+    Nothing -> fail "pegGrammar: no %name directive, which declaring a \
+                    \grammar needs"
+  let baseName = maybe "" id (directive "name" (gsDirs gs))
+      envName  = TH.mkName (maybe (capitalise baseName ++ "Env") id
+                                  (directive "env" (gsDirs gs)))
+      streamV  = TH.mkName "s"
+  streamT <- case directive "stream" (gsDirs gs) of
+    Nothing -> pure (TH.VarT streamV)
+    Just t  -> either (\e -> fail ("pegGrammar: in %stream: " ++ e)) pure
+                      (parseHsType t)
+  anns <- mapM (resultAnnotation gname) (gsDefs gs)
+  let envRhs = promotedList [ envEntry n ty | (n, ty) <- anns ]
+  startRes <- case directive "result" (gsDirs gs) of
+    Just t  -> either (\e -> fail ("pegGrammar: in %result: " ++ e)) pure
+                      (parseHsType t)
+    Nothing -> case resultTypeOf streamT anns (gsStart gs) of
+      Just t  -> pure t
+      Nothing -> fail "pegGrammar: cannot tell what the start expression \
+                      \returns.\n  It has a semantic action of its own; state \
+                      \its type with %result."
+  let envApplied = TH.AppT (TH.ConT envName) streamT
+      grammarTy  = foldl TH.AppT (TH.ConT ''Grammar)
+                     [streamT, envApplied, startRes]
+      sigTy = case directive "stream" (gsDirs gs) of
+        Just _  -> grammarTy
+        Nothing -> TH.ForallT [TH.PlainTV streamV TH.SpecifiedSpec]
+                              [TH.AppT (TH.ConT ''Stream) (TH.VarT streamV)]
+                              grammarTy
+  body <- pegGrammarExp src
+  pure [ TH.TySynD envName [TH.PlainTV streamV TH.BndrReq] envRhs
+       , TH.SigD gname sigTy
+       , TH.FunD gname [TH.Clause [] (TH.NormalB body) []]
+       ]
+  where
+    capitalise []     = []
+    capitalise (c:cs) = toUpper c : cs
+    toUpper c = if c >= 'a' && c <= 'z' then toEnum (fromEnum c - 32) else c
+
+-- | A rule's declared result type, which declaring an environment needs.
+resultAnnotation :: TH.Name -> Def -> Q (String, TH.Type)
+resultAnnotation gname (Def n ann _) = case ann of
+  Nothing  -> fail ("pegGrammar: the rule " ++ n ++ " has no result type.\n\
+                    \  Declaring " ++ show gname ++ " means writing the \
+                    \environment down, and a rule's\n  result type is the one \
+                    \thing the grammar does not say: write\n    " ++ n
+                    ++ " :: T <- ...")
+  Just src -> case parseHsType src of
+    Left e  -> fail ("pegGrammar: in the result type of " ++ n ++ ": " ++ e)
+    Right t -> pure (n, t)
+
+-- | What the start expression returns, read off the rules' declared types.
+--
+-- This follows @translateSeqWith@: a sequence with no semantic action returns
+-- its labelled items, one of them bare and several as a tuple.  A sequence
+-- /with/ an action returns whatever the action does, which is Haskell and so
+-- not knowable here — hence the 'Maybe', and the @%result@ directive.
+resultTypeOf :: TH.Type -> [(String, TH.Type)] -> PExpr -> Maybe TH.Type
+resultTypeOf streamT anns = go
+  where
+    go (ENT n)       = lookup n anns
+    go (EChar _)     = Just (TH.ConT ''Char)
+    go EDot          = Just (TH.ConT ''Char)
+    go (EClass _ _)  = Just (TH.ConT ''Char)
+    go (EString _)   = Just (TH.ConT ''String)
+    go (EAnd _)      = Just (TH.TupleT 0)
+    go (ENot _)      = Just (TH.TupleT 0)
+    go (EOpt e)      = TH.AppT (TH.ConT ''Maybe) <$> go e
+    go (EStar e)     = rep e
+    go (EPlus e)     = rep e
+    go (EIndent _ e) = go e
+    go (EPos _ e)    = go e
+    go (EAlign e)    = go e
+    go (EChoice es)  = firstJust (map go es)
+    go (ESeq _ (Just _)) = Nothing
+    go (ESeq items Nothing) = case [ e | Item (Just _) e <- items ] of
+      []  -> Just (TH.TupleT 0)
+      [e] -> go e
+      es  -> foldl TH.AppT (TH.TupleT (length es)) <$> mapM go es
+
+    rep e | spannable e = Just streamT
+          | otherwise   = TH.AppT TH.ListT <$> go e
+
+    firstJust xs = case [ x | Just x <- xs ] of
+      (x:_) -> Just x
+      []    -> Nothing
+
+--------------------------------------------------------------------------------
+-- Building the environment's type
+--------------------------------------------------------------------------------
+
+promotedList :: [TH.Type] -> TH.Type
+promotedList = foldr (\x acc -> TH.AppT (TH.AppT TH.PromotedConsT x) acc)
+                     TH.PromotedNilT
+
+envEntry :: String -> TH.Type -> TH.Type
+envEntry n res =
+  TH.AppT (TH.AppT (TH.PromotedTupleT 2) (TH.LitT (TH.StrTyLit n)))
+          (TH.AppT (TH.PromotedT 'EnvEntry) res)
diff --git a/src/PEG/QQ/HsExp.hs b/src/PEG/QQ/HsExp.hs
--- a/src/PEG/QQ/HsExp.hs
+++ b/src/PEG/QQ/HsExp.hs
@@ -8,6 +8,7 @@
 -- @base@ and @template-haskell@.
 module PEG.QQ.HsExp
   ( parseHsExp
+  , parseHsType
   ) where
 
 import Data.Char           (isAlpha, isAlphaNum, isDigit, isHexDigit,
@@ -199,6 +200,21 @@
   in (c ++ n, r)
 
 type P a = [Tok] -> Either String (a, [Tok])
+
+-- | Parse a type: what a @rule :: T@ annotation carries.  The grammar is the
+-- one 'pType' already accepted inside an expression's @::@ annotation —
+-- application, functions, lists and tuples — so nothing new is parsed here,
+-- only reached from a new entry point.
+parseHsType :: String -> Either String Type
+parseHsType src = do
+  toks <- lexHs src
+  case toks of
+    [] -> Left "empty type annotation"
+    _  -> do
+      (t, rest) <- pType toks
+      case rest of
+        [] -> Right t
+        _  -> Left ("unconsumed input in type " ++ atTok rest)
 
 parseHsExp :: String -> Either String Exp
 parseHsExp src = do
diff --git a/src/PEG/QQ/Syntax.hs b/src/PEG/QQ/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/PEG/QQ/Syntax.hs
@@ -0,0 +1,381 @@
+-- | The concrete syntax of the grammar DSL: its abstract syntax tree and the
+-- recursive-descent parser that produces it.
+--
+-- This is split out of "PEG.QQ" so that the tree has two consumers rather
+-- than one.  "PEG.QQ" translates it to Template Haskell; "PEG.Analysis"
+-- computes nullability, FIRST sets and the well-formedness diagnostics from
+-- it, at splice time, without the type checker being involved.
+module PEG.QQ.Syntax
+  ( Def (..)
+  , Item (..)
+  , PExpr (..)
+  , RelS (..)
+  , Directive (..)
+  , P
+  , parseGrammar
+  , parseDirectives
+  , parseExpr
+  , spaces
+  ) where
+
+-- | One rule: its name, the source of its @:: T@ result-type annotation if it
+-- has one, and its body.
+--
+-- The annotation is what lets 'PEG.QQ.pegGrammar' write the environment down:
+-- the nullability and FIRST set of a rule can be computed from the grammar,
+-- but its result type cannot — that comes from the Haskell in its semantic
+-- action, which GHC types long after the splice has run.
+data Def = Def String (Maybe String) PExpr
+  deriving Show
+
+-- | A @%key value@ line in the header of a grammar: @%start@, @%name@,
+-- @%env@, @%stream@, @%result@.  The value is the rest of the line.
+data Directive = Directive String String
+  deriving Show
+
+data Item = Item (Maybe String) PExpr
+  deriving Show
+
+data PExpr
+  = EChoice  [PExpr]
+  | ESeq     [Item] (Maybe String)
+  | EAnd     PExpr
+  | ENot     PExpr
+  | EOpt     PExpr
+  | EStar    PExpr
+  | EPlus    PExpr
+  | EChar    Char
+  | EString  String
+  | EClass   Bool [(Char,Char)]   -- ^ 'True' when the class is negated.
+  | EDot
+  | ENT      String
+  | EIndent  RelS PExpr
+  | EPos     RelS PExpr
+  | EAlign   PExpr
+  deriving Show
+
+data RelS
+  = RGt
+  | RGe
+  | REq
+  | RAny
+  | ROffset Int
+  | RNamed  String
+  deriving Show
+
+type P a = String -> Either String (a, String)
+
+errorAt :: String -> String -> Either String a
+errorAt msg s = Left $ msg ++ " at: " ++ show (take 30 s)
+
+spaces :: String -> String
+spaces []         = []
+spaces ('#':xs)   = spaces (drop 1 (dropWhile (/= '\n') xs))
+spaces (c:xs)
+  | c == ' ' || c == '\t' || c == '\n' || c == '\r' = spaces xs
+  | otherwise = c:xs
+
+tok :: String -> P ()
+tok t s = case stripPrefix t (spaces s) of
+  Just r  -> Right ((), r)
+  Nothing -> errorAt ("expected " ++ show t) s
+  where
+    stripPrefix [] xs                 = Just xs
+    stripPrefix (p:ps) (x:xs) | p==x  = stripPrefix ps xs
+    stripPrefix _ _                   = Nothing
+
+ident :: P String
+ident s0 = case spaces s0 of
+  (c:xs) | isIdStart c ->
+    let (rest, leftover) = span isIdCont xs
+    in Right (c:rest, leftover)
+  s -> errorAt "expected identifier" s
+  where
+    isIdStart c = c == '_' || (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
+    isIdCont c  = isIdStart c || (c >= '0' && c <= '9')
+
+charLit :: P Char
+charLit s0 = case spaces s0 of
+  ('\'':xs) -> do (c, r1) <- escChar '\'' xs
+                  case r1 of
+                    ('\'':r2) -> Right (c, r2)
+                    _         -> errorAt "expected closing '" r1
+  s         -> errorAt "expected character literal" s
+
+strLit :: P String
+strLit s0 = case spaces s0 of
+  ('"':xs) -> loop xs
+  s        -> errorAt "expected string literal" s
+  where
+    loop ('"':r) = Right ("", r)
+    loop r0      = do (c, r1) <- escChar '"' r0
+                      (cs, r2) <- loop r1
+                      pure (c:cs, r2)
+
+escChar :: Char -> P Char
+escChar _ ('\\':e:xs) = case e of
+  'n'  -> Right ('\n', xs)
+  't'  -> Right ('\t', xs)
+  'r'  -> Right ('\r', xs)
+  '\\' -> Right ('\\', xs)
+  '\'' -> Right ('\'', xs)
+  '"'  -> Right ('"',  xs)
+  '['  -> Right ('[',  xs)
+  ']'  -> Right (']',  xs)
+  '0'  -> Right ('\0', xs)
+  '^'  -> Right ('^',  xs)
+  _    -> errorAt ("unknown escape \\" ++ [e]) xs
+escChar stopC (c:xs)
+  | c == stopC = errorAt "unexpected close quote" (c:xs)
+  | otherwise  = Right (c, xs)
+escChar _ [] = Left "unexpected end of input in literal"
+
+-- | A character class.  A leading @^@ negates it, as in POSIX; write
+-- @[\\^]@ for a class containing the caret itself.
+classLit :: P (Bool, [(Char, Char)])
+classLit s0 = case spaces s0 of
+  ('[':'^':xs) -> do
+    (rs, r) <- loop xs
+    if null rs
+      then errorAt "empty negated character class" s0
+      else Right ((True, rs), r)
+  ('[':xs)     -> do
+    (rs, r) <- loop xs
+    Right ((False, rs), r)
+  s            -> errorAt "expected character class" s
+  where
+    loop (']':r) = Right ([], r)
+    loop []      = Left "unterminated character class"
+    loop r0      = do
+      (c1, r1) <- escChar ']' r0
+      case r1 of
+        ('-':']':r2) -> pure ([(c1, c1), ('-', '-')], r2)
+        ('-':r2) ->
+          do (c2, r3) <- escChar ']' r2
+             (rs, r4) <- loop r3
+             pure ((c1, c2) : rs, r4)
+        _ ->
+          do (rs, r2) <- loop r1
+             pure ((c1, c1) : rs, r2)
+
+actionLit :: P String
+actionLit s0 = case spaces s0 of
+  ('{':xs) -> go (1 :: Int) ' ' [] xs
+  s        -> errorAt "expected a semantic action" s
+  where
+    go _ _ _ [] = Left "unterminated semantic action: missing '}'"
+    go n prev acc s = case s of
+      ('{':'-':r) -> do
+        (com, r') <- blockComment (1 :: Int) r
+        go n '}' (revApp ("{-" ++ com) acc) r'
+      ('"':r) -> do
+        (str, r') <- literalBody '"' r
+        go n '"' (revApp ('"' : str) acc) r'
+      ('\'':r) | not (isIdChar prev) -> do
+        (ch, r') <- literalBody '\'' r
+        go n '\'' (revApp ('\'' : ch) acc) r'
+      ('{':r) -> go (n + 1) '{' ('{' : acc) r
+      ('}':r) | n == 1    -> Right (reverse acc, r)
+              | otherwise -> go (n - 1) '}' ('}' : acc) r
+      (c:_) | c `elem` symChars ->
+        let (sym, r) = span (`elem` symChars) s
+        in if all (== '-') sym && length sym >= 2
+             then let (line, r') = span (/= '\n') r
+                  in go n '\n' (revApp (sym ++ line) acc) r'
+             else go n (last sym) (revApp sym acc) r
+      (c:r) -> go n c (c : acc) r
+
+    isIdChar c = c == '_' || c == '\''
+              || (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
+              || (c >= '0' && c <= '9')
+
+    literalBody _ [] = Left "unterminated literal in a semantic action"
+    literalBody q ('\\':c:r)     = do (b, r') <- literalBody q r
+                                      Right ('\\' : c : b, r')
+    literalBody q (c:r) | c == q = Right ([c], r)
+    literalBody q (c:r)          = do (b, r') <- literalBody q r
+                                      Right (c : b, r')
+
+    blockComment _ []              = Left "unterminated {- -} comment in a semantic action"
+    blockComment k ('-':'}':r)
+      | k == 1                     = Right ("-}", r)
+      | otherwise                  = do (c, r') <- blockComment (k - 1) r
+                                        Right ("-}" ++ c, r')
+    blockComment k ('{':'-':r)     = do (c, r') <- blockComment (k + 1) r
+                                        Right ("{-" ++ c, r')
+    blockComment k (c:r)           = do (c', r') <- blockComment k r
+                                        Right (c : c', r')
+
+    revApp xs acc = reverse xs ++ acc
+
+    symChars = "!#$%&*+./<=>?@\\^|-~:"
+
+parseExpr :: P PExpr
+parseExpr s0 = do
+  (e1, s1) <- parseSeq s0
+  loop [e1] s1
+  where
+    loop acc s = case tok "/" s of
+      Right (_, s') -> do (e, s'') <- parseSeq s'
+                          loop (e:acc) s''
+      Left _        -> case reverse acc of
+        [x] -> Right (x, s)
+        xs  -> Right (EChoice xs, s)
+
+parseSeq :: P PExpr
+parseSeq s0 = loop [] s0
+  where
+    loop acc s = case parseLabelled s of
+      Right (it, s') -> loop (it:acc) s'
+      Left _         -> case actionLit s of
+        Right (act, s') -> Right (ESeq (reverse acc) (Just act), s')
+        Left _          -> Right (ESeq (reverse acc) Nothing,    s)
+
+parseLabelled :: P Item
+parseLabelled s = case label s of
+  Just (l, s1) -> do (e, s2) <- parsePrefix s1
+                     pure (Item (Just l) e, s2)
+  Nothing      -> do (e, s1) <- parsePrefix s
+                     pure (Item Nothing e, s1)
+  where
+    label s' = case ident s' of
+      Right (name, s1) -> case tok ":" s1 of
+        Right (_, s2) -> Just (name, s2)
+        Left _        -> Nothing
+      Left _ -> Nothing
+
+parsePrefix :: P PExpr
+parsePrefix s = case tok "&" s of
+  Right (_, s') -> do (e, s'') <- parseSuffix s'; pure (EAnd e, s'')
+  Left _        -> case tok "!" s of
+    Right (_, s') -> do (e, s'') <- parseSuffix s'; pure (ENot e, s'')
+    Left _        -> parseSuffix s
+
+parseSuffix :: P PExpr
+parseSuffix s = do
+  (p, s1) <- parsePrimary s
+  loop p s1
+  where
+    loop p s1 = case tok "?" s1 of
+      Right (_, s2) -> loop (EOpt p) s2
+      Left _ -> case tok "*" s1 of
+        Right (_, s2) -> loop (EStar p) s2
+        Left _ -> case tok "+" s1 of
+          Right (_, s2) -> loop (EPlus p) s2
+          Left _ -> case indented EIndent "^" p s1 of
+            Right (p', s2) -> loop p' s2
+            Left _ -> case indented EPos "_" p s1 of
+              Right (p', s2) -> loop p' s2
+              Left _         -> Right (p, s1)
+
+    indented con marker p s1 = do
+      (_, s2) <- tok marker s1
+      (r, s3) <- parseRel s2
+      pure (con r p, s3)
+
+parseRel :: P RelS
+parseRel s = case tok ">=" s of
+  Right (_, s1) -> Right (RGe, s1)
+  Left _ -> case tok ">" s of
+    Right (_, s1) -> Right (RGt, s1)
+    Left _ -> case tok "=" s of
+      Right (_, s1) -> Right (REq, s1)
+      Left _ -> case tok "~" s of
+        Right (_, s1) -> Right (RAny, s1)
+        Left _ -> case tok "@" s of
+          Right (_, s1) -> do (name, s2) <- ident s1
+                              pure (RNamed name, s2)
+          Left _ -> case tok "+" s of
+            Right (_, s1) -> case span isDigit (spaces s1) of
+              ([], _)     -> errorAt "expected a number after '+'" s1
+              (ds, s2)    -> Right (ROffset (read ds), s2)
+            Left _ -> errorAt "expected an indentation relation" s
+  where
+    isDigit c = c >= '0' && c <= '9'
+
+parsePrimary :: P PExpr
+parsePrimary s =
+  case tok "(" s of
+    Right (_, s1) -> do (e, s2) <- parseExpr s1
+                        (_, s3) <- tok ")" s2
+                        pure (e, s3)
+    Left _ -> case parseAlign s of
+     Right r -> Right r
+     Left _ -> case tok "." s of
+      Right (_, s1) -> Right (EDot, s1)
+      Left _ -> case charLit s of
+        Right (c, s1) -> Right (EChar c, s1)
+        Left _ -> case strLit s of
+          Right (cs, s1) -> Right (EString cs, s1)
+          Left _ -> case classLit s of
+            Right ((neg, rs), s1) -> Right (EClass neg rs, s1)
+            Left _ -> case ident s of
+              Right (name, s1) ->
+                case tok "<-" s1 of
+                  Right _  -> errorAt "definition where expression expected" s
+                  Left _   -> Right (ENT name, s1)
+              Left _ -> errorAt "expected primary expression" s
+
+parseAlign :: P PExpr
+parseAlign s = do
+  (_, s1) <- tok "|" s
+  (e, s2) <- parseExpr s1
+  if isEmptyExpr e
+    then errorAt "empty alignment: write |e| with a non-empty e" s
+    else do (_, s3) <- tok "|" s2
+            pure (EAlign e, s3)
+  where
+    isEmptyExpr (ESeq [] Nothing) = True
+    isEmptyExpr _                 = False
+
+parseGrammar :: P [Def]
+parseGrammar s0 = loop [] s0
+  where
+    loop acc s = case ident s of
+      Left _ -> case spaces s of
+        [] -> Right (reverse acc, "")
+        s' -> errorAt "expected definition or end of input" s'
+      Right (name, s1) -> do
+        (ty, s2) <- resultType s1
+        (_, s3)  <- tok "<-" s2
+        (e, s4)  <- parseExpr s3
+        loop (Def name ty e : acc) s4
+
+    -- @name :: T <- body@.  The annotation runs to the @<-@, which no type
+    -- can contain, so it needs no parsing here: it is handed to
+    -- "PEG.QQ.HsExp" as text.
+    resultType s = case tok "::" s of
+      Left _        -> Right (Nothing, s)
+      Right (_, s1) -> case breakOnArrow (spaces s1) of
+        Nothing        -> errorAt "expected '<-' after a result type" s1
+        Just (ty, s2)
+          | all isSpaceC ty -> errorAt "empty result type" s1
+          | otherwise       -> Right (Just ty, s2)
+
+    breakOnArrow = go []
+      where
+        go _   []             = Nothing
+        go acc r@('<':'-':_)  = Just (reverse acc, r)
+        go acc (c:cs)         = go (c:acc) cs
+
+    isSpaceC c = c == ' ' || c == '\t' || c == '\n' || c == '\r'
+
+-- | Consume the @%key value@ lines a grammar may start with.
+--
+-- Only the header is scanned, and only before the first rule, so a @%@ inside
+-- a semantic action is never mistaken for a directive.
+parseDirectives :: P [Directive]
+parseDirectives = loop []
+  where
+    loop acc s = case spaces s of
+      ('%':rest) ->
+        let (key, r1)  = span isKeyChar rest
+            (val, r2)  = span (/= '\n') r1
+        in if null key
+             then errorAt "expected a directive name after '%'" s
+             else loop (Directive key (trim val) : acc) r2
+      s' -> Right (reverse acc, s')
+
+    isKeyChar c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
+    trim = dropWhile isSpaceC . reverse . dropWhile isSpaceC . reverse
+    isSpaceC c = c == ' ' || c == '\t' || c == '\r'
diff --git a/src/PEG/Syntax.hs b/src/PEG/Syntax.hs
--- a/src/PEG/Syntax.hs
+++ b/src/PEG/Syntax.hs
@@ -12,10 +12,10 @@
 -- | The PEG expression GADT and combinator API.
 --
 -- 'PExp' is the core type: a GADT indexed by the input stream, the grammar
--- environment, the 'PEG.Type.Ty' of the expression (nullability + FIRST set),
--- and the Haskell result type.  Combinators like '<*>.' and '.||.' propagate
--- type information at the kind level so that 'PEG.Grammar.Acyclic' can be
--- checked without running the parser.
+-- environment, and the Haskell result type.  Every non-terminal reference is
+-- checked against the environment, so @nt \@\"expr\"@ is a type error unless
+-- the grammar has a rule called @expr@, and it has whatever type that rule
+-- has.
 --
 -- The first parameter, @s@, is the stream the expression consumes; see
 -- "PEG.Stream".  It appears in the type because a character class produces a
@@ -24,10 +24,36 @@
 --
 -- Most users will not build 'PExp' values directly; instead they use the
 -- quasi-quoter in "PEG.QQ".
+--
+-- == What is no longer in the index
+--
+-- A 'PExp' used to carry a fourth index, its nullability and FIRST set, from
+-- which @PEG.Grammar.Acyclic@ derived a type error for a left-recursive
+-- grammar.  Both are still computed and left recursion is still rejected, by
+-- "PEG.Analysis" when the grammar is spliced rather than by GHC on every
+-- compilation that mentions it; "PEG.Type" says what that cost and what it
+-- buys, and "PEG.Grammar" says what it gives up.
+--
+-- One consequence shows up here rather than there.  'Star' used to demand a
+-- non-nullable argument, so that @e*@ on an @e@ matching the empty string was
+-- a type error; now nothing in the type stops it, and it is "PEG.Analysis"
+-- that reports it.  A 'Star' built by hand over a nullable expression will
+-- loop at run time.
+--
+-- The other consequence is that a combinator over expressions is now an
+-- ordinary polymorphic function.  What had to be written
+--
+-- @
+-- lexeme :: PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a
+-- @
+--
+-- is now @PExp s env a -> PExp s env a@, and composes without the caller
+-- having to get a nesting of type families right.
 module PEG.Syntax
   ( Name (..)
   , PExp (..)
   , nt
+  , ntw
   , sat
   , charClass
   , notCharClass
@@ -46,10 +72,6 @@
   , plus
   , oneOf
   , stringNE
-  , SeqTy
-  , ChoiceTy
-  , NTTy
-  , NTGo
   ) where
 
 import Data.Kind    (Type)
@@ -65,43 +87,6 @@
 -- | A singleton witness for a non-terminal name @n@.
 data Name (n :: Symbol) = Name
 
--- | The 'Ty' of a sequence @e1 e2@.
---
--- Written as a projective type synonym rather than a type family so that it
--- reduces to a @'MkTy'@ head even when its operands are still abstract.  That
--- is what lets a polymorphic combinator such as
---
--- @
--- lexeme :: PExp s env ty a -> PExp s env (SeqTy ty ('MkTy 'True '[])) a
--- @
---
--- compose without the caller having to get the nesting of 'SeqTy' exactly
--- right.  The cost it used to carry — an exponential blow-up as the operands
--- get duplicated across the right-hand side — came from 'Union' and
--- 'ConsIfAbsent', not from here; see "PEG.TyLevel".
-type SeqTy t1 t2 =
-  'MkTy (And (Nullable t1) (Nullable t2))
-        (Union (First t1) (If (Nullable t1) (First t2) '[]))
-
--- | The 'Ty' of an ordered choice @e1 \/ e2@.
-type ChoiceTy t1 t2 =
-  'MkTy (Or  (Nullable t1) (Nullable t2))
-        (Union (First t1) (First t2))
-
--- | The 'Ty' of a non-terminal reference @n@ looked up in @env@.
-type NTTy n env = NTGo n (TyOf (Lookup n env))
-
--- | The 'Ty' of a reference to a non-terminal named @n@ whose own 'Ty' is
--- @t@.
---
--- 'NT' and 'nt' are stated in terms of this rather than 'NTTy' so that the
--- environment is searched /once/ per occurrence, by the constructor's
--- @Lookup n env ~ 'EnvEntry ty a@ equality.  Naming @Lookup n env@ twice, as
--- an expansion of 'NTTy' does, doubles the cost of what profiling shows to be
--- the dominant term in checking a large grammar.
-type family NTGo (n :: Symbol) (t :: Ty) :: Ty where
-  NTGo n ('MkTy nu f) = 'MkTy nu (ConsIfAbsent n f)
-
 -- | A typed PEG expression over the stream @s@.
 --
 -- Constructors correspond to the standard PEG operators:
@@ -122,61 +107,85 @@
 -- * 'Indent' — require the next token to satisfy an indentation relation
 -- * 'Position'— set the column relation for tokens inside the sub-expression
 -- * 'Align'  — require the next token to be aligned with the current position
-data PExp (s :: Type) (env :: Env) (ty :: Ty) (a :: Type) where
-  Pure     :: a -> PExp s env ('MkTy 'True '[]) a
-  Term     :: Char -> PExp s env ('MkTy 'False '[]) Char
+data PExp (s :: Type) (env :: Env) (a :: Type) where
+  Pure     :: a -> PExp s env a
+  Term     :: Char -> PExp s env Char
   -- | Match one character of a class.  This is what a character class such as
   -- @[a-zA-Z0-9_]@ compiles to: a single bit test instead of a chain of
   -- ordered choices.
-  Sat      :: !CharSet -> PExp s env ('MkTy 'False '[]) Char
-  -- | Match a string literal.  The string must be non-empty (the 'Ty' index
-  -- claims the expression is not nullable); use 'pureP' @""@ otherwise.
+  Sat      :: !CharSet -> PExp s env Char
+  -- | Match a string literal.  The string must be non-empty; use 'pureP' @""@
+  -- otherwise.
   --
   -- The result is the literal itself, so it is shared rather than sliced out
   -- of the input.
-  Str      :: String -> PExp s env ('MkTy 'False '[]) String
+  Str      :: String -> PExp s env String
   -- | Match the longest run of characters belonging to a class, possibly
   -- empty — what @[a-z]*@ compiles to.  The result is a chunk of the input
   -- stream, so on 'Data.Text.Text' this is a slice and costs no copy.
-  Span     :: !CharSet -> PExp s env ('MkTy 'True  '[]) s
+  Span     :: !CharSet -> PExp s env s
   -- | As 'Span', but the run must be non-empty: @[a-z]+@.
-  Span1    :: !CharSet -> PExp s env ('MkTy 'False '[]) s
-  AnyChar  :: PExp s env ('MkTy 'False '[]) Char
+  Span1    :: !CharSet -> PExp s env s
+  AnyChar  :: PExp s env Char
   -- The environment is looked up /once/, by the equality below, and the
-  -- result is bound to the rigid variables @ty@ and @a@.  Passing
-  -- @TyOf (Lookup n env)@ straight to 'KnownMember' instead makes GHC
-  -- re-reduce the lookup at every step of the instance chain that walks
-  -- @env@, which costs @O(|env|^2)@ per non-terminal occurrence.
-  NT       :: forall n ty s env a.
+  -- result is bound to the rigid variable @a@.  Passing @ResOf (Lookup n
+  -- env)@ straight to 'KnownMember' instead makes GHC re-reduce the lookup at
+  -- every step of the instance chain that walks @env@, which costs
+  -- @O(|env|^2)@ per non-terminal occurrence.
+  NT       :: forall n s env a.
               ( KnownSymbol n
-              , Lookup n env ~ 'EnvEntry ty a
+              , Lookup n env ~ 'EnvEntry a
               , KnownMember n env a
               )
            => Name n
-           -> PExp s env (NTGo n ty) a
-  Seq      :: PExp s env t1 (a -> b)
-           -> PExp s env t2 a
-           -> PExp s env (SeqTy t1 t2) b
-  Choice   :: PExp s env t1 a
-           -> PExp s env t2 a
-           -> PExp s env (ChoiceTy t1 t2) a
-  Star     :: PExp s env ('MkTy 'False f) a
-           -> PExp s env ('MkTy 'True  f) [a]
-  Not      :: PExp s env ('MkTy n f) a
-           -> PExp s env ('MkTy 'True f) ()
+           -> PExp s env a
+  -- | As 'NT', but the proof that the rule is in the environment is supplied
+  -- rather than searched for.
+  --
+  -- The @Lookup@ equality is kept, so this is not a weaker claim than 'NT':
+  -- @a@ still comes from the environment, and a witness that points at a
+  -- different rule does not type-check.  What is gone is the 'KnownMember'
+  -- instance chain, which walks the environment one entry at a time for every
+  -- occurrence of every non-terminal.  On a 64-rule grammar that chain is
+  -- about three quarters of what resolving a reference costs; see
+  -- @bench-compile/@.
+  --
+  -- A splice knows each rule's position and so can write the witness down.
+  -- Hand-written grammars have nothing to gain here and should keep using
+  -- 'nt'.
+  NTW      :: forall n s env a.
+              ( KnownSymbol n
+              , Lookup n env ~ 'EnvEntry a
+              )
+           => Name n
+           -> Member n env a
+           -> PExp s env a
+  Seq      :: PExp s env (a -> b)
+           -> PExp s env a
+           -> PExp s env b
+  Choice   :: PExp s env a
+           -> PExp s env a
+           -> PExp s env a
+  -- | Kleene star.  The argument must not match the empty string, or the
+  -- parser will not terminate; that is checked by "PEG.Analysis" when the
+  -- grammar is spliced, and not at all when a 'Star' is built by hand.
+  Star     :: PExp s env a
+           -> PExp s env [a]
+  Not      :: PExp s env a
+           -> PExp s env ()
   Map      :: (a -> b)
-           -> PExp s env ty a
-           -> PExp s env ty b
+           -> PExp s env a
+           -> PExp s env b
   Indent   :: Rel n
-           -> PExp s env ty a
-           -> PExp s env ty a
+           -> PExp s env a
+           -> PExp s env a
   Position :: Rel n
-           -> PExp s env ty a
-           -> PExp s env ty a
-  Align    :: PExp s env ty a
-           -> PExp s env ty a
+           -> PExp s env a
+           -> PExp s env a
+  Align    :: PExp s env a
+           -> PExp s env a
 
-instance Functor (PExp s env ty) where
+instance Functor (PExp s env) where
   fmap = Map
 
 -- | Reference a non-terminal by name using a type application:
@@ -185,102 +194,114 @@
 -- The name is deliberately the /first/ quantified variable, so that
 -- @nt \@\"expr\"@ keeps working: the stream and environment are recovered by
 -- unification.
-nt :: forall n env s ty a.
+nt :: forall n env s a.
       ( KnownSymbol n
-      , Lookup n env ~ 'EnvEntry ty a
+      , Lookup n env ~ 'EnvEntry a
       , KnownMember n env a
       )
-   => PExp s env (NTGo n ty) a
+   => PExp s env a
 nt = NT (Name :: Name n)
 
+-- | Reference a non-terminal by name, supplying the membership proof:
+-- @ntw \@"ruleName" (There Here)@.
+--
+-- This is what a generated grammar emits; see 'NTW'.
+ntw :: forall n env s a.
+       ( KnownSymbol n
+       , Lookup n env ~ 'EnvEntry a
+       )
+    => Member n env a
+    -> PExp s env a
+ntw = NTW (Name :: Name n)
+
 -- | Succeed without consuming any input.
-pureP :: a -> PExp s env ('MkTy 'True '[]) a
+pureP :: a -> PExp s env a
 pureP = Pure
 
 -- | Apply a function to the result of an expression.
-fmapP :: (a -> b) -> PExp s env ty a -> PExp s env ty b
+fmapP :: (a -> b) -> PExp s env a -> PExp s env b
 fmapP = Map
 
 -- | Require the sub-expression to satisfy the given column relation.
-indent :: Rel n -> PExp s env ty a -> PExp s env ty a
+indent :: Rel n -> PExp s env a -> PExp s env a
 indent = Indent
 
 -- | Override the token mode for the sub-expression.
-position :: Rel n -> PExp s env ty a -> PExp s env ty a
+position :: Rel n -> PExp s env a -> PExp s env a
 position = Position
 
 -- | Require the sub-expression to start at the current alignment column.
-align :: PExp s env ty a -> PExp s env ty a
+align :: PExp s env a -> PExp s env a
 align = Align
 
 -- | Infix synonym for 'fmapP'.
-(<$>.) :: (a -> b) -> PExp s env ty a -> PExp s env ty b
+(<$>.) :: (a -> b) -> PExp s env a -> PExp s env b
 (<$>.) = Map
 infixl 4 <$>.
 
 -- | Infix sequential composition.
-(<*>.) :: PExp s env t1 (a -> b)
-       -> PExp s env t2 a
-       -> PExp s env (SeqTy t1 t2) b
+(<*>.) :: PExp s env (a -> b)
+       -> PExp s env a
+       -> PExp s env b
 (<*>.) = Seq
 infixl 4 <*>.
 
 -- | Sequence two expressions, discarding the result of the first.
-(.>>.) :: PExp s env t1 a
-       -> PExp s env t2 b
-       -> PExp s env (SeqTy t1 t2) b
+(.>>.) :: PExp s env a
+       -> PExp s env b
+       -> PExp s env b
 e1 .>>. e2 = Map (\_ b -> b) e1 <*>. e2
 infixl 6 .>>.
 
 -- | Infix ordered choice (@e1 \/ e2@): try @e1@; if it fails, try @e2@.
-(.||.) :: PExp s env t1 a -> PExp s env t2 a -> PExp s env (ChoiceTy t1 t2) a
+(.||.) :: PExp s env a -> PExp s env a -> PExp s env a
 (.||.) = Choice
 infixl 5 .||.
 
 -- | Optional match: @opt e = (Just \<$\>. e) .||. pureP Nothing@.
-opt :: PExp s env t a
-    -> PExp s env (ChoiceTy t ('MkTy 'True '[])) (Maybe a)
+opt :: PExp s env a -> PExp s env (Maybe a)
 opt e = (Just <$>. e) .||. pureP Nothing
 
 -- | One-or-more: @plus e = (:) \<$\>. e \<*\>. Star e@.
 --
+-- As for 'Star', @e@ must not match the empty string.
+--
 -- For a single character class, prefer 'spanOf1': it matches the whole run in
 -- one scan and returns a chunk of the stream instead of a list.
-plus :: PExp s env ('MkTy 'False f) a
-     -> PExp s env (SeqTy ('MkTy 'False f) ('MkTy 'True f)) [a]
+plus :: PExp s env a -> PExp s env [a]
 plus e = (:) <$>. e <*>. Star e
 
 -- | Match any character of the given set.
-sat :: CharSet -> PExp s env ('MkTy 'False '[]) Char
+sat :: CharSet -> PExp s env Char
 sat = Sat
 
 -- | Match any character inside one of the given inclusive ranges.
--- This is the representation the quasi-quoter emits for @[a-z0-9]@ and
+-- This is the representation the quasi-quoter emits for @[a-z]@ and
 -- friends.
-charClass :: [(Char, Char)] -> PExp s env ('MkTy 'False '[]) Char
+charClass :: [(Char, Char)] -> PExp s env Char
 charClass = Sat . CS.fromRanges
 
 -- | Match any character /outside/ the given inclusive ranges.
 -- The quasi-quoter emits this for @[^\"]@.
-notCharClass :: [(Char, Char)] -> PExp s env ('MkTy 'False '[]) Char
+notCharClass :: [(Char, Char)] -> PExp s env Char
 notCharClass = Sat . CS.notInRanges
 
 -- | Match the longest run of characters of the set, possibly empty.  The
 -- result is a chunk of the input stream.
-spanOf :: CharSet -> PExp s env ('MkTy 'True '[]) s
+spanOf :: CharSet -> PExp s env s
 spanOf = Span
 
 -- | Match a non-empty run of characters of the set.
-spanOf1 :: CharSet -> PExp s env ('MkTy 'False '[]) s
+spanOf1 :: CharSet -> PExp s env s
 spanOf1 = Span1
 
 -- | Match any character in the given list. The list must be non-empty.
-oneOf :: [Char] -> PExp s env ('MkTy 'False '[]) Char
+oneOf :: [Char] -> PExp s env Char
 oneOf []  = error "PEG.Syntax.oneOf: empty character class"
 oneOf [c] = Term c
 oneOf cs  = Sat (CS.fromList cs)
 
 -- | Match an exact string literal. The string must be non-empty.
-stringNE :: String -> PExp s env ('MkTy 'False '[]) String
+stringNE :: String -> PExp s env String
 stringNE [] = error "PEG.Syntax.stringNE: empty string"
 stringNE s  = Str s
diff --git a/src/PEG/TyLevel.hs b/src/PEG/TyLevel.hs
--- a/src/PEG/TyLevel.hs
+++ b/src/PEG/TyLevel.hs
@@ -4,134 +4,46 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- | Type-level utilities: boolean logic, symbol equality, set operations,
--- and environment lookup.
---
--- These type families are used internally to compute the FIRST sets and
--- nullability of PEG expressions at the kind level, enabling the
--- 'PEG.Grammar.Acyclic' constraint to be resolved at compile time.
---
--- == Representation of FIRST sets
---
--- A FIRST set is a @['Symbol']@ kept /strictly sorted/ by 'CmpSymbol'.
--- Sortedness is the whole point: it makes the representation canonical (one
--- set, one type), so 'Union' is a single-pass merge and 'Elem' can stop at
--- the first symbol greater than the one it is looking for.
---
--- == Why the families are written this way
+-- | Looking a non-terminal up in the grammar environment.
 --
--- Every clause below mentions each of its arguments — and in particular each
--- recursive call — /exactly once/ on the right-hand side.  This is not a
--- style choice.  A clause such as
+-- This is the only type-level computation the library still does, and it is
+-- the hot path: there is one lookup per occurrence of every non-terminal in
+-- the grammar, so it is written to do as little as possible per entry
+-- scanned.
 --
--- @
--- ConsIfAbsent x xs = If (Elem x xs) xs (x ': xs)   -- DON'T
--- @
+-- == What used to be here
 --
--- mentions @xs@ three times, and @xs@ is normally an unreduced application
--- of 'Union'.  GHC therefore has three copies of the pending computation to
--- reduce, each of which triples again one level down: a union of two sets of
--- size @n@ costs @3^n@ reductions rather than @n@.  Dispatching on an
--- already-computed 'Ordering' in a separate family keeps every right-hand
--- side linear in its arguments.
+-- Sorted-set machinery — 'Union', membership, insertion — over the FIRST sets
+-- that environment entries used to carry, together with the boolean families
+-- that combined their nullability.  Those sets now live in "PEG.Analysis",
+-- which computes them at splice time; see "PEG.Type" for why they left the
+-- types.  What remains is the search, and with the sets gone it is a search
+-- over an environment that is linear in the size of the grammar rather than
+-- quadratic.
 module PEG.TyLevel
-  ( If
-  , And
-  , Or
-  , SymEq
-  , Elem
-  , Union
-  , ConsIfAbsent
-  , Lookup
+  ( Lookup
   , Names
   ) where
 
-import GHC.TypeLits (CmpSymbol, ErrorMessage (..), Symbol, TypeError)
+import GHC.TypeLits (ErrorMessage (..), Symbol, TypeError)
 
 import PEG.Type
 
-type family If (c :: Bool) (t :: k) (e :: k) :: k where
-  If 'True  t _ = t
-  If 'False _ e = e
-
-type family And (a :: Bool) (b :: Bool) :: Bool where
-  And 'True  b = b
-  And 'False _ = 'False
-
-type family Or (a :: Bool) (b :: Bool) :: Bool where
-  Or 'True  _ = 'True
-  Or 'False b = b
-
-type family SymEq (a :: Symbol) (b :: Symbol) :: Bool where
-  SymEq a b = IsEQ (CmpSymbol a b)
-
-type family IsEQ (o :: Ordering) :: Bool where
-  IsEQ 'EQ = 'True
-  IsEQ _   = 'False
-
--- | Is @x@ a member of the sorted set @xs@?
---
--- Stops as soon as it reaches a symbol greater than @x@, so a miss costs
--- half a scan on average rather than a full one.
-type family Elem (x :: Symbol) (xs :: [Symbol]) :: Bool where
-  Elem _ '[]       = 'False
-  Elem x (y ': ys) = ElemGo (CmpSymbol x y) x ys
-
-type family ElemGo (o :: Ordering) (x :: Symbol) (ys :: [Symbol]) :: Bool where
-  ElemGo 'EQ _ _  = 'True
-  ElemGo 'LT _ _  = 'False
-  ElemGo 'GT x ys = Elem x ys
-
--- | Insert @x@ into the sorted set @xs@, keeping it sorted and duplicate-free.
-type family ConsIfAbsent (x :: Symbol) (xs :: [Symbol]) :: [Symbol] where
-  ConsIfAbsent x '[]       = '[x]
-  ConsIfAbsent x (y ': ys) = InsGo (CmpSymbol x y) x y ys
-
-type family InsGo (o :: Ordering) (x :: Symbol) (y :: Symbol)
-                  (ys :: [Symbol]) :: [Symbol] where
-  InsGo 'LT x y ys = x ': y ': ys
-  InsGo 'EQ _ y ys = y ': ys
-  InsGo 'GT x y ys = y ': ConsIfAbsent x ys
-
--- | Union of two sorted sets: a single merge pass, @O(|xs| + |ys|)@.
---
--- The merge nests one type-family reduction per element of the result, so a
--- FIRST set of more than about a hundred non-terminals runs into GHC's
--- default reduction limit and reports @Reduction stack overflow@.  That is a
--- limit, not a slowdown: @-freduction-depth=0@ lifts it, and a union of two
--- 128-element sets then takes about 0.3 s.
-type family Union (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
-  Union '[]       ys        = ys
-  Union (x ': xs) '[]       = x ': xs
-  Union (x ': xs) (y ': ys) = MergeGo (CmpSymbol x y) x xs y ys
-
-type family MergeGo (o :: Ordering) (x :: Symbol) (xs :: [Symbol])
-                    (y :: Symbol) (ys :: [Symbol]) :: [Symbol] where
-  MergeGo 'LT x xs y ys = x ': Union xs (y ': ys)
-  MergeGo 'EQ x xs _ ys = x ': Union xs ys
-  MergeGo 'GT x xs y ys = y ': Union (x ': xs) ys
-
 -- | Look up a non-terminal's entry in the environment.
 --
--- This is the hot path: there is one lookup per occurrence of every
--- non-terminal in the grammar, so it is written to do as little as possible
--- per entry scanned.
---
 -- Two things matter.  The search proper ('LookupMb') carries only the tail it
 -- still has to scan — threading the /whole/ environment through it so the
 -- not-found case could name the available non-terminals costs a traversal of
--- that environment at every step, and an environment of @n@ rules is itself
--- @O(n^2)@ type nodes because every rule carries a FIRST set.  The
--- environment is therefore named once, in 'Found', which only reduces after
--- the search has finished.
+-- that environment at every step.  The environment is therefore named once,
+-- in 'Found', which only reduces after the search has finished; measured
+-- against a variant that does not name it at all, the good error message
+-- costs about 5%.
 --
 -- And the match is on a /non-linear/ pattern — @s@ appears twice in the
 -- second clause — rather than on @CmpSymbol s t@ dispatched through a helper
 -- family.  GHC decides the clause by syntactic equality and by apartness for
 -- the fall-through, which is one type-family reduction per entry instead of
--- two.  (The trick is @Data.Type.Map@'s, from @type-level-sets@.)  It costs
--- nothing here: unlike 'Elem', this search has no sortedness to exploit, so
--- there was never a third case to short-circuit on.
+-- two.  (The trick is @Data.Type.Map@'s, from @type-level-sets@.)
 type family Lookup (s :: Symbol) (env :: Env) :: EnvEntry where
   Lookup s env = Found s env (LookupMb s env)
 
@@ -147,6 +59,7 @@
     TypeError ('Text "Undefined non-terminal: " ':<>: 'ShowType s
          ':$$: 'Text "Available non-terminals: " ':<>: 'ShowType (Names env))
 
+-- | The names an environment defines, for the message above.
 type family Names (env :: Env) :: [Symbol] where
   Names '[]               = '[]
   Names ('(s, _) ': rest) = s ': Names rest
diff --git a/src/PEG/Type.hs b/src/PEG/Type.hs
--- a/src/PEG/Type.hs
+++ b/src/PEG/Type.hs
@@ -3,52 +3,55 @@
 {-# LANGUAGE TypeFamilies   #-}
 {-# LANGUAGE TypeOperators  #-}
 
--- | Type-level representation of PEG type information.
+-- | The grammar environment: what a non-terminal's name is bound to.
 --
--- Each non-terminal carries a 'Ty': a pair of its /nullability/
--- (can it match the empty string?) and its /FIRST set/ (which non-terminal
--- names can appear at the head of a derivation?).
--- Both pieces of information are tracked as type-level data and used by the
--- 'PEG.Grammar.Acyclic' constraint to reject left-recursive grammars at
--- compile time.
+-- An environment maps each non-terminal's name to the Haskell type its rule
+-- returns, and to nothing else.  A reference to a non-terminal is checked
+-- against it — @nt \@\"expr\"@ is a type error unless @expr@ is a rule, and it
+-- has whatever type @expr@'s rule has — which is the whole of what the
+-- environment is for.
+--
+-- == What used to be here
+--
+-- Entries used to carry a 'Ty' as well: the rule's nullability and its FIRST
+-- set, the set of non-terminals that can begin a derivation of it.  That is
+-- what made left recursion a type error, by way of a @PEG.Grammar.Acyclic@
+-- constraint that checked no rule was in its own FIRST set.
+--
+-- It was also, measurably, the whole cost of compiling a large grammar.  A
+-- FIRST set grows with the grammar, so an environment of @n@ rules was
+-- @O(n^2)@ type nodes, and each of the @2n@ reference constraints in the
+-- rules had to be solved against it: 64 rules cost GHC 15 s, and the same
+-- environment with a payload nothing reads at all was 15x an environment
+-- without one.  Not reducing the FIRST-set arithmetic was worth nothing by
+-- comparison — it was never the arithmetic, only the size.  See
+-- @bench-compile/@.
+--
+-- Nullability and FIRST sets are still computed, and left recursion is still
+-- rejected before a parser can be built from a left-recursive grammar — by
+-- "PEG.Analysis", at splice time, once, in milliseconds, with the offending
+-- rule and its cycle named.  What changed is that GHC no longer recomputes
+-- them on every compilation of every module that mentions the grammar.  The
+-- cost of that trade is real and is stated in "PEG.Grammar": a 'Rules' value
+-- assembled by hand, without going through a quasi-quoter, is no longer
+-- checked for left recursion by anything.
 module PEG.Type
-  ( Ty (..)
-  , Nullable
-  , First
-  , EnvEntry (..)
+  ( EnvEntry (..)
   , Env
-  , TyOf
   , ResOf
   ) where
 
 import Data.Kind    (Type)
 import GHC.TypeLits (Symbol)
 
--- | A PEG type: nullability flag and FIRST set.
---
--- @'MkTy' n fs@ means the expression may match the empty string iff @n ~ 'True@,
--- and the set of non-terminal names that can begin a derivation is @fs@.
-data Ty = MkTy Bool [Symbol]
-
--- | Extract the nullability flag from a 'Ty'.
-type family Nullable (t :: Ty) :: Bool where
-  Nullable ('MkTy n _) = n
-
--- | Extract the FIRST set (list of non-terminal names) from a 'Ty'.
-type family First (t :: Ty) :: [Symbol] where
-  First ('MkTy _ f) = f
-
--- | An entry in the grammar environment: a 'Ty' paired with its result type.
-data EnvEntry = EnvEntry Ty Type
+-- | An entry in the grammar environment: the type a rule's semantic action
+-- produces.
+data EnvEntry = EnvEntry Type
 
 -- | A grammar environment: a type-level association list mapping non-terminal
 -- names ('Symbol') to their 'EnvEntry'.
 type Env = [(Symbol, EnvEntry)]
 
--- | Extract the 'Ty' from an 'EnvEntry'.
-type family TyOf (e :: EnvEntry) :: Ty where
-  TyOf ('EnvEntry t _) = t
-
 -- | Extract the result type from an 'EnvEntry'.
 type family ResOf (e :: EnvEntry) :: Type where
-  ResOf ('EnvEntry _ a) = a
+  ResOf ('EnvEntry a) = a
diff --git a/tests/Analysis.hs b/tests/Analysis.hs
new file mode 100644
--- /dev/null
+++ b/tests/Analysis.hs
@@ -0,0 +1,483 @@
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE QuasiQuotes      #-}
+{-# LANGUAGE TemplateHaskell  #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators    #-}
+-- | Checks "PEG.Analysis" against what its results are supposed to mean.
+--
+-- == Why this is the whole guarantee now
+--
+-- It did not use to be.  Environment entries carried their FIRST sets as
+-- type-level data and @Acyclic@ checked them, so every grammar that compiled
+-- was a grammar GHC had agreed with, and this module only had to cover the
+-- cases GHC could not see.  Entries no longer carry them — "PEG.Type" says
+-- why — so nothing recomputes what "PEG.Analysis" concludes.  A left-recursive
+-- grammar it accepts is a parser that loops.
+--
+-- So the analysis is checked here against a separate statement of what its
+-- two results mean, written to be obvious rather than fast:
+--
+-- * a rule is nullable iff it is in the least fixpoint of "can match the
+--   empty string";
+-- * @FIRST(r)@ is the set of non-terminals reachable from @r@ under the
+--   one-step head relation — @m@ is a head of @r@ when @m@ can be the first
+--   non-terminal a derivation of @r@ reaches without any other non-terminal
+--   being entered first.
+--
+-- The second is the definition left recursion is stated in terms of: @r@ is
+-- left-recursive exactly when @r@ is reachable from itself.  "PEG.Analysis"
+-- computes it a different way — it propagates whole FIRST sets through
+-- 'PEG.Analysis.seqTy' and 'PEG.Analysis.choiceTy' as it iterates, over
+-- sorted sets merged pairwise — so the two agreeing is worth something.
+--
+-- They are compared over every grammar in @examples/@ and over a few hundred
+-- generated ones, which is what covers the shapes the examples happen not to
+-- have.
+--
+-- What is also checked here:
+--
+-- * The diagnostics, which no example can exercise, because an example that
+--   triggered one would not compile.
+-- * The /shape/ of what 'PEG.QQ.pegGrammar' generates, against a literal
+--   written out below, and that the grammar it generates parses.
+--
+-- Result types are not compared against the analysis — it does not compute
+-- them, and cannot: they come from the Haskell semantic actions, which GHC
+-- types long after the splice has run.
+module Main (main) where
+
+import Control.Monad (forM, unless)
+import Data.List     (isPrefixOf, nub, sort, union)
+import System.Exit   (exitFailure)
+
+import Data.Proxy    (Proxy (..))
+
+import PEG
+import PEG.QQ        (pegGrammar)
+import PEG.Analysis  (Diagnostic (..), Ty (..), analyse, renderDiagnostic)
+import PEG.QQ.Syntax (Def (..), Item (..), PExpr (..), parseDirectives,
+                      parseGrammar)
+
+exampleFiles :: [FilePath]
+exampleFiles =
+  [ "examples/Arith.hs"
+  , "examples/Layout.hs"
+  , "examples/Patterns.hs"
+  , "examples/Compat.hs"
+  ]
+
+main :: IO ()
+main = do
+  results <- concat <$> mapM checkFile exampleFiles
+  let failures = [ msg | Left msg <- results ]
+      checked  = length [ () | Right () <- results ]
+  mapM_ putStrLn failures
+  putStrLn ("PEG.Analysis: " ++ show checked ++ " grammars in examples/ agree\
+            \ with the specification")
+  unless (null failures) exitFailure
+  -- The examples are half the point of this test; a refactor that stops
+  -- finding them must fail rather than pass vacuously.
+  unless (checked + length failures >= 7) $ do
+    putStrLn "PEG.Analysis: expected at least 7 grammars in examples/, \
+             \found fewer"
+    exitFailure
+  let generated = [ checkDefs ("generated/" ++ show i) g
+                  | (i, g) <- zip [0 :: Int ..] generatedGrammars ]
+      genBad    = [ msg | Left msg <- generated ]
+  mapM_ putStrLn (take 5 genBad)
+  putStrLn ("PEG.Analysis: " ++ show (length generated - length genBad)
+              ++ " of " ++ show (length generated)
+              ++ " generated grammars agree with the specification"
+              ++ " (" ++ show recursive ++ " left-recursive rules, "
+              ++ show withHeads ++ " with a non-empty FIRST set)")
+  unless (null genBad) exitFailure
+  -- Agreement is easy to reach vacuously: a generator that stopped emitting
+  -- references would make every FIRST set empty and every grammar pass.  The
+  -- corpus has to keep containing both answers.
+  unless (recursive >= 20 && withHeads >= 20) $ do
+    putStrLn "PEG.Analysis: the generated corpus has gone degenerate"
+    exitFailure
+  let checks = standaloneChecks ++ [witnessCheck] ++ generatedChecks
+  mapM_ report checks
+  unless (all (\(_, ok) -> ok) checks) exitFailure
+  where
+    report (name, ok) =
+      putStrLn ((if ok then "ok   " else "FAIL ") ++ name)
+
+    -- Coverage of the generated corpus, measured through the specification
+    -- rather than the analysis, so that it says what the corpus contains and
+    -- not what the code under test thinks it contains.
+    recursive = length [ () | g <- generatedGrammars
+                            , (n, Ty _ f) <- specEnv g, n `elem` f ]
+    withHeads = length [ () | g <- generatedGrammars
+                            , any (\(_, Ty _ f) -> not (null f)) (specEnv g) ]
+
+--------------------------------------------------------------------------------
+-- The specification: what nullability and a FIRST set mean
+--------------------------------------------------------------------------------
+
+-- | The least fixpoint of "can match the empty string", over the rules.
+--
+-- Iterated over the whole system from "nothing is nullable" until it stops
+-- changing, which is the definition rather than a way of computing it
+-- quickly.
+specNullable :: [Def] -> [(String, Bool)]
+specNullable defs = fix [ (n, False) | Def n _ _ <- defs ]
+  where
+    fix m = let m' = [ (n, nu m e) | Def n _ e <- defs ]
+            in if m' == m then m else fix m'
+
+    nu m = go
+      where
+        go (EChar _)      = False
+        go EDot           = False
+        go (EClass _ _)   = False
+        go (EString s)    = null s
+        go (ENT n)        = maybe False id (lookup n m)
+        go (EAnd _)       = True          -- a lookahead consumes nothing
+        go (ENot _)       = True
+        go (EOpt _)       = True
+        go (EStar _)      = True
+        go (EPlus e)      = go e
+        go (EIndent _ e)  = go e
+        go (EPos _ e)     = go e
+        go (EAlign e)     = go e
+        go (EChoice es)   = any go es
+        go (ESeq its _)   = all (\(Item _ e) -> go e) its
+
+-- | The one-step head relation: the non-terminals that a derivation of this
+-- expression can reach first, without entering any other non-terminal on the
+-- way.
+--
+-- A sequence contributes the heads of its first item, and those of the second
+-- as well when the first can match the empty string, and so on.
+specHeads :: [(String, Bool)] -> PExpr -> [String]
+specHeads nulls = go
+  where
+    nullableOf = specNullableOf nulls
+
+    go (EChar _)     = []
+    go EDot          = []
+    go (EClass _ _)  = []
+    go (EString _)   = []
+    go (ENT n)       = [n]
+    go (EAnd e)      = go e
+    go (ENot e)      = go e
+    go (EOpt e)      = go e
+    go (EStar e)     = go e
+    go (EPlus e)     = go e
+    go (EIndent _ e) = go e
+    go (EPos _ e)    = go e
+    go (EAlign e)    = go e
+    go (EChoice es)  = foldl' union [] (map go es)
+    go (ESeq its _)  = seqHeads [ e | Item _ e <- its ]
+
+    seqHeads []     = []
+    seqHeads (e:es) | nullableOf e = go e `union` seqHeads es
+                    | otherwise    = go e
+
+-- | Whether an expression is nullable, given the rules' nullability.
+specNullableOf :: [(String, Bool)] -> PExpr -> Bool
+specNullableOf nulls = go
+  where
+    go (EChar _)     = False
+    go EDot          = False
+    go (EClass _ _)  = False
+    go (EString s)   = null s
+    go (ENT n)       = maybe False id (lookup n nulls)
+    go (EAnd _)      = True
+    go (ENot _)      = True
+    go (EOpt _)      = True
+    go (EStar _)     = True
+    go (EPlus e)     = go e
+    go (EIndent _ e) = go e
+    go (EPos _ e)    = go e
+    go (EAlign e)    = go e
+    go (EChoice es)  = any go es
+    go (ESeq its _)  = all (\(Item _ e) -> go e) its
+
+-- | The environment the analysis is supposed to produce: nullability as
+-- above, and each rule's FIRST set as everything reachable from it under
+-- 'specHeads'.
+specEnv :: [Def] -> [(String, Ty)]
+specEnv defs =
+  [ (n, Ty (specNullableOf nulls e) (sort (reach (heads e)))) | Def n _ e <- defs ]
+  where
+    nulls = specNullable defs
+    heads = specHeads nulls
+
+    bodyOf n = case [ e | Def m _ e <- defs, m == n ] of
+                 (e:_) -> Just e
+                 []    -> Nothing
+
+    -- Transitive closure by worklist.  A name the grammar does not define
+    -- contributes itself and nothing further, which is how the analysis
+    -- treats it too.
+    reach = grow []
+      where
+        grow seen []     = seen
+        grow seen (x:xs)
+          | x `elem` seen = grow seen xs
+          | otherwise     = grow (x : seen)
+                                 (maybe [] heads (bodyOf x) ++ xs)
+
+--------------------------------------------------------------------------------
+-- Comparing the analysis against it
+--------------------------------------------------------------------------------
+
+-- | Check one grammar, whatever the analysis makes of it.
+--
+-- The two must agree on left recursion — the analysis reports it exactly when
+-- a rule is reachable from itself — and, when there is none, on the whole
+-- environment.
+checkDefs :: String -> [Def] -> Either String ()
+checkDefs what defs
+  | not (null dups) = Right ()   -- a duplicate rule makes 'specEnv' meaningless
+  | otherwise = case analyse defs of
+      Left ds
+        | not (null [ () | LeftRecursive _ _ <- ds ]) ->
+            if null selfReaching
+              then Left (what ++ ": analyse reports left recursion, the \
+                                 \specification finds no cycle")
+              else Right ()
+        | otherwise -> Right ()  -- other diagnostics are checked separately
+      Right env
+        | not (null selfReaching) ->
+            Left (what ++ ": analyse accepted a grammar whose rules "
+                    ++ show selfReaching ++ " reach themselves")
+        | normalise env == normalise spec -> Right ()
+        | otherwise -> Left (unlines
+            ([ what ++ ": the analysis and the specification disagree" ]
+             ++ [ "  " ++ n ++ ": analysed " ++ show got
+                          ++ ", specified " ++ show want
+                | (n, got) <- normalise env
+                , Just want <- [lookup n (normalise spec)]
+                , got /= want ]))
+  where
+    spec  = specEnv defs
+    names = [ n | Def n _ _ <- defs ]
+    dups  = [ n | n <- nub names, length (filter (== n) names) > 1 ]
+    selfReaching = [ n | (n, Ty _ f) <- spec, n `elem` f ]
+
+    -- Compared as plain pairs: the analysis keeps its sets sorted and the
+    -- specification builds them with 'union', so ordering is not the claim.
+    normalise :: [(String, Ty)] -> [(String, (Bool, [String]))]
+    normalise = sort . map (\(n, Ty nu f) -> (n, (nu, sort (nub f))))
+
+checkFile :: FilePath -> IO [Either String ()]
+checkFile path = do
+  src <- readFile path
+  let blocks = [ (b, False) | b <- extractBlocks "[pegRules|" src ]
+                 ++ [ (b, True) | b <- extractBlocks "[pegGrammar|" src ]
+  forM (zip [1 :: Int ..] blocks) $ \(i, (block, hasDirectives)) ->
+    pure $ do
+      body <- if hasDirectives
+                then fmap snd (left ("directives: " ++) (parseDirectives block))
+                else Right block
+      (defs, _) <- left ("parse error: " ++) (parseGrammar body)
+      left ((path ++ " (" ++ show i ++ "): ") ++) (checkDefs path defs)
+  where
+    left f = either (Left . f) Right
+
+--------------------------------------------------------------------------------
+-- Generated grammars, to cover the shapes the examples happen not to have
+--------------------------------------------------------------------------------
+
+-- | A few hundred small grammars, built deterministically so a failure can be
+-- reproduced by index.
+--
+-- The shapes are chosen to make heads interesting: nullable prefixes, so that
+-- a sequence's second item contributes; optionals and stars, which are
+-- nullable but keep their operand's heads; and references both forwards and
+-- backwards, so that some of these are left-recursive and some are not.
+generatedGrammars :: [[Def]]
+generatedGrammars = [ grammarFrom seed | seed <- take 400 seeds ]
+  where
+    seeds = iterate (\x -> (x * 1103515245 + 12345) `mod` 2147483648) 1
+
+grammarFrom :: Int -> [Def]
+grammarFrom seed0 = snd (foldl' rule (seed0, []) [0 .. n - 1])
+  where
+    n     = 2 + seed0 `mod` 4
+    names = [ "r" ++ show i | i <- [0 .. n - 1] ]
+
+    rule (seed, acc) i =
+      let (e, seed') = expr seed 2
+      in (seed', acc ++ [Def (names !! i) Nothing e])
+
+    next seed = (seed `div` 65536 `mod` 32768, (seed * 1103515245 + 12345)
+                                                 `mod` 2147483648)
+
+    -- A term, at the given remaining depth.  At depth zero only leaves.
+    expr seed depth =
+      let (k, seed') = next seed
+      in case (if depth <= (0 :: Int) then k `mod` 3 else k `mod` 9) of
+           0 -> (EChar 'x', seed')
+           1 -> (EClass False [('a', 'z')], seed')
+           2 -> (ENT (names !! (k `mod` n)), seed')
+           3 -> let (e, s') = expr seed' (depth - 1) in (EOpt e, s')
+           4 -> let (e, s') = expr seed' (depth - 1) in (EStar e, s')
+           5 -> let (e, s') = expr seed' (depth - 1) in (ENot e, s')
+           6 -> let (a, s1) = expr seed' (depth - 1)
+                    (b, s2) = expr s1 (depth - 1)
+                in (EChoice [a, b], s2)
+           7 -> let (a, s1) = expr seed' (depth - 1)
+                    (b, s2) = expr s1 (depth - 1)
+                in (ESeq [Item Nothing a, Item Nothing b] Nothing, s2)
+           _ -> let (a, s1) = expr seed' (depth - 1)
+                in (ESeq [Item Nothing (EOpt a)
+                         , Item Nothing (ENT (names !! (k `mod` n)))]
+                         Nothing, s1)
+
+--------------------------------------------------------------------------------
+-- Standalone cases: the diagnostics, which no example can exercise because an
+-- example that triggered one would not compile.
+--------------------------------------------------------------------------------
+
+standaloneChecks :: [(String, Bool)]
+standaloneChecks =
+  [ ("left recursion is reported with its cycle",
+      case run "expr <- e:expr '+' t:term / t:term\nterm <- ds:[0-9]+" of
+        Left [LeftRecursive "expr" path] -> path == ["expr", "expr"]
+        _                                -> False)
+  , ("indirect left recursion reports one cycle, not one per rule",
+      case run "a <- x:b\nb <- y:c\nc <- z:a" of
+        Left [LeftRecursive n path] -> n `elem` ["a", "b", "c"]
+                                         && length path == 4
+                                         && take 1 path == take 1 (reverse path)
+        _                           -> False)
+  , ("a nullable repetition is reported",
+      case run "a <- xs:b*\nb <- c:'x'?" of
+        Left [NullableStar "a"] -> True
+        _                       -> False)
+  , ("an undefined non-terminal is reported",
+      case run "a <- x:missing" of
+        Left [UndefinedNT "missing" ["a"]] -> True
+        _                                  -> False)
+  , ("a duplicate rule is reported",
+      case run "a <- 'x'\na <- 'y'" of
+        Left [DuplicateRule "a"] -> True
+        _                        -> False)
+  , ("a right-recursive grammar is accepted",
+      case run "a <- 'x' r:a / 'y'" of
+        Right env -> lookup "a" env == Just (Ty False [])
+        _         -> False)
+  , ("a class repetition is a Span, not a Star",
+      case run "a <- xs:[a-z]*" of
+        Right env -> lookup "a" env == Just (Ty True [])
+        _         -> False)
+  , ("a nullable head propagates the next item's FIRST set",
+      case run "a <- w:ws n:b\nws <- [ ]*\nb <- 'x'" of
+        Right env -> lookup "a" env == Just (Ty False ["b", "ws"])
+        _         -> False)
+  , ("the reported cycle names every rule on it",
+      case run "a <- x:b\nb <- y:c\nc <- z:a" of
+        Left [LeftRecursive _ path] -> sort (nub path) == ["a", "b", "c"]
+        _                           -> False)
+  , ("renderDiagnostic says which rule",
+      case run "expr <- e:expr '+' t:term / t:term\nterm <- ds:[0-9]+" of
+        Left [d] -> "expr" `isInfix` renderDiagnostic d
+        _        -> False)
+  ]
+  where
+    run src = case parseGrammar src of
+      Left err        -> Left [UndefinedNT ("parse error: " ++ err) []]
+      Right (defs, _) -> analyse defs
+    isInfix needle hay = any (needle `isPrefixOf`) (suffixes hay)
+    suffixes xs = xs : case xs of { [] -> []; (_:r) -> suffixes r }
+
+--------------------------------------------------------------------------------
+-- 'ntw': a reference that carries its own membership proof
+--------------------------------------------------------------------------------
+
+-- The environment's order is the rule chain's order, which is what makes
+-- @There Here@ name @digits@.  A witness that named the wrong rule would not
+-- compile: 'NTW' keeps the @Lookup@ equality that ties the two together.
+type NtwEnv =
+  '[ '("pair"  , 'EnvEntry (Int, Int))
+   , '("digits", 'EnvEntry Int)
+   ]
+
+digitsCount :: PExp String NtwEnv Int
+digitsCount = fmapP (length . chunkToString) (spanOf1 (fromRanges [('0', '9')]))
+
+ntwGrammar :: Grammar String NtwEnv (Int, Int)
+ntwGrammar =
+  Grammar
+    (RCons (Name @"pair")
+           ((,) <$>. ntw @"digits" (There Here)
+                <*>. (Term ',' .>>. ntw @"digits" (There Here)))
+       (RCons (Name @"digits") digitsCount RNil))
+    (ntw @"pair" Here)
+
+--------------------------------------------------------------------------------
+-- What pegGrammar generates
+--------------------------------------------------------------------------------
+
+[pegGrammar|
+  %name  tiny
+  %env   TinyEnv
+  %start pair
+
+  pair   :: (Int, Int) <- a:digits ',' b:digits
+  digits :: Int        <- ds:[0-9]+ { length (chunkToString ds) }
+|]
+
+-- The environment a reader would have written for that grammar.  GHC has
+-- already agreed that the generated one is well-formed — it type-checked
+-- @tiny@ — so what this pins down is that it is also the /expected/ one: same
+-- rules, same order, same spelling.
+type ExpectedTinyEnv s =
+  '[ '("pair"  , 'EnvEntry (Int, Int))
+   , '("digits", 'EnvEntry Int)
+   ]
+
+sameEnv :: forall (a :: Env) (b :: Env). (a ~ b) => Proxy a -> Proxy b -> ()
+sameEnv _ _ = ()
+
+generatedEnvIsExpected :: ()
+generatedEnvIsExpected =
+  sameEnv (Proxy :: Proxy (TinyEnv String))
+          (Proxy :: Proxy (ExpectedTinyEnv String))
+
+generatedChecks :: [(String, Bool)]
+generatedChecks =
+  [ ("pegGrammar generates the expected environment",
+      generatedEnvIsExpected == ())
+  , ("a generated grammar parses",
+      case parse tiny "12,345" of
+        OK r _ rest -> r == (2, 3) && rest == ""
+        Fail        -> False)
+  ]
+
+witnessCheck :: (String, Bool)
+witnessCheck =
+  ( "ntw parses through the witness it was given"
+  , case parse ntwGrammar "12,345" of
+      OK r _ rest -> r == (2, 3) && rest == ""
+      Fail        -> False )
+
+--------------------------------------------------------------------------------
+-- Extracting the grammars from an example's source
+--------------------------------------------------------------------------------
+
+-- | Every @[pegRules| ... |]@ (or @[pegGrammar| ... |]@) block, in order of
+-- appearance.
+extractBlocks :: String -> String -> [String]
+extractBlocks open = go
+  where
+    go s = case breakOn open s of
+      Nothing   -> []
+      Just rest -> let (body, after) = breakClose rest in body : go after
+    breakClose s = case breakOn "|]" s of
+      Nothing   -> (s, "")
+      Just rest -> (take (length s - length rest - 2) s, rest)
+
+-- | The input just past the first occurrence of the needle, if any.
+breakOn :: String -> String -> Maybe String
+breakOn needle = go
+  where
+    go [] = Nothing
+    go s@(_:cs)
+      | needle `isPrefixOf` s = Just (drop (length needle) s)
+      | otherwise             = go cs
diff --git a/typed-peg.cabal b/typed-peg.cabal
--- a/typed-peg.cabal
+++ b/typed-peg.cabal
@@ -1,12 +1,14 @@
 cabal-version:      3.0
 name:               typed-peg
-version:            0.2.0.0
+version:            0.3.0.0
 synopsis:           Type-safe PEG parser combinators
 description:
   A library for building Parsing Expression Grammars parsers
-  with compile-time safety guarantees. Grammar non-terminals are
-  indexed by their nullability and FIRST sets at the type level,
-  making left-recursive grammars a type error.
+  with compile-time safety guarantees. Non-terminal references are
+  checked at the type level against an environment binding each rule
+  to the type it returns; left recursion, a repetition that cannot
+  consume input, an undefined non-terminal and a duplicate rule are
+  reported when the grammar is spliced, naming the rule.
   .
   A quasi-quoter (@PEG.QQ@) allows writing grammars in a concrete
   DSL syntax. Indentation-sensitive parsing is supported natively
@@ -59,6 +61,7 @@
   hs-source-dirs:  src
   exposed-modules:
     PEG
+    PEG.Analysis
     PEG.CharSet
     PEG.Grammar
     PEG.Indent
@@ -66,6 +69,7 @@
     PEG.Parse
     PEG.QQ
     PEG.QQ.HsExp
+    PEG.QQ.Syntax
     PEG.Semantics.Simple
     PEG.Stream
     PEG.Syntax
@@ -87,6 +91,16 @@
       base
     , bytestring
     , text
+    , typed-peg
+
+test-suite typed-peg-analysis
+  import:          common-opts
+  type:            exitcode-stdio-1.0
+  hs-source-dirs:  tests
+  main-is:         Analysis.hs
+  other-extensions: TemplateHaskell, QuasiQuotes
+  build-depends:
+      base
     , typed-peg
 
 benchmark typed-peg-bench