- Migrated pattern-matching analysis to stdlib.

7 files changed, 866 insertions, 52 deletions

diff --git a/stdlib/source/lux/lang/analysis.lux b/stdlib/source/lux/lang/analysis.lux
index 223f2fb29..0b48f803d 100644
--- a/stdlib/source/lux/lang/analysis.lux
+++ b/stdlib/source/lux/lang/analysis.lux
@@ -48,24 +48,15 @@
   (#Constant Ident)
   (#Special (Special Text)))
 
-(type: #export Variant
+(type: #export (Variant a)
   {#lefts Nat
    #right? Bool
-   #value Analysis})
+   #value a})
 
-(type: #export Tuple (List Analysis))
+(type: #export (Tuple a) (List a))
 
 (type: #export Application [Analysis (List Analysis)])
 
-(do-template [<name> <tag>]
-  [(def: <name>
-     (-> Analysis Analysis)
-     (|>> <tag> #Sum #Structure))]
-
-  [left #.Left]
-  [right #.Right]
-  )
-
 (def: (last? size tag)
   (-> Nat Tag Bool)
   (n/= (dec size) tag))
@@ -75,35 +66,47 @@
   (let [identity (#Function (list) (#Variable (#Local +1)))]
     (#Apply value identity)))
 
-(def: #export (sum size tag value)
-  (-> Nat Tag Analysis Analysis)
-  (if (last? size tag)
-    (if (n/= +1 tag)
-      (..right value)
-      (list/fold (function.const ..left)
-                 (..right value)
-                 (list.n/range +0 (n/- +2 tag))))
-    (list/fold (function.const ..left)
-               (case value
-                 (#Structure (#Sum _))
-                 (no-op value)
-
-                 _
-                 value)
-               (list.n/range +0 tag))))
-
-(def: #export (product members)
-  (-> Tuple Analysis)
-  (case (list.reverse members)
-    #.Nil
-    (#Primitive #Unit)
-
-    (#.Cons singleton #.Nil)
-    singleton
-
-    (#.Cons last prevs)
-    (list/fold (function (_ left right) (#Structure (#Product left right)))
-               last prevs)))
+(do-template [<name> <type> <structure> <prep-value>]
+  [(def: #export (<name> size tag value)
+     (-> Nat Tag <type> <type>)
+     (let [left (function.const (|>> #.Left #Sum <structure>))
+           right (|>> #.Right #Sum <structure>)]
+       (if (last? size tag)
+         (if (n/= +1 tag)
+           (right value)
+           (list/fold left
+                      (right value)
+                      (list.n/range +0 (n/- +2 tag))))
+         (list/fold left
+                    (case value
+                      (<structure> (#Sum _))
+                      (<prep-value> value)
+
+                      _
+                      value)
+                    (list.n/range +0 tag)))))]
+
+  [sum-analysis Analysis #Structure no-op]
+  [sum-pattern  Pattern  #Complex   id]
+  )
+
+(do-template [<name> <type> <primitive> <structure>]
+  [(def: #export (<name> members)
+     (-> (Tuple <type>) <type>)
+     (case (list.reverse members)
+       #.Nil
+       (<primitive> #Unit)
+
+       (#.Cons singleton #.Nil)
+       singleton
+
+       (#.Cons last prevs)
+       (list/fold (function (_ left right) (<structure> (#Product left right)))
+                  last prevs)))]
+
+  [product-analysis Analysis #Primitive #Structure]
+  [product-pattern  Pattern  #Simple    #Complex]
+  )
 
 (def: #export (apply [func args])
   (-> Application Analysis)
@@ -113,7 +116,7 @@
   (-> Code (Meta Analysis)))
 
 (def: #export (tuple analysis)
-  (-> Analysis Tuple)
+  (-> Analysis (Tuple Analysis))
   (case analysis
     (#Structure (#Product left right))
     (#.Cons left (tuple right))
@@ -122,7 +125,7 @@
     (list analysis)))
 
 (def: #export (variant analysis)
-  (-> Analysis (Maybe Variant))
+  (-> Analysis (Maybe (Variant Analysis)))
   (loop [lefts +0
          variantA analysis]
     (case variantA
diff --git a/stdlib/source/lux/lang/analysis/case.lux b/stdlib/source/lux/lang/analysis/case.lux
new file mode 100644
index 000000000..3140a9d7e
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/case.lux
@@ -0,0 +1,295 @@
+(.module:
+  [lux #- case]
+  (lux (control [monad #+ do]
+                ["ex" exception #+ exception:]
+                [equality #+ Eq])
+       (data [bool]
+             [number]
+             [product]
+             ["e" error]
+             [maybe]
+             [text]
+             text/format
+             (coll [list "list/" Fold<List> Monoid<List> Functor<List>]))
+       [function]
+       [macro]
+       (macro [code])
+       [lang]
+       (lang [type]
+             (type ["tc" check])
+             [".L" scope]
+             [".L" analysis #+ Pattern Analysis Analyser]
+             (analysis [".A" type]
+                       [".A" structure]
+                       (case [".A" coverage])))))
+
+(exception: #export (cannot-match-type-with-pattern {type Type} {pattern Code})
+  (ex.report ["Type" (%type type)]
+             ["Pattern" (%code pattern)]))
+
+(exception: #export (sum-type-has-no-case {case Nat} {type Type})
+  (ex.report ["Case" (%n case)]
+             ["Type" (%type type)]))
+
+(exception: #export (unrecognized-pattern-syntax {pattern Code})
+  (%code pattern))
+
+(exception: #export (cannot-simplify-type-for-pattern-matching {type Type})
+  (%type type))
+
+(do-template [<name>]
+  [(exception: #export (<name> {message Text})
+     message)]
+
+  [cannot-have-empty-branches]
+  [non-exhaustive-pattern-matching]
+  )
+
+(def: (re-quantify envs baseT)
+  (-> (List (List Type)) Type Type)
+  (.case envs
+    #.Nil
+    baseT
+
+    (#.Cons head tail)
+    (re-quantify tail (#.UnivQ head baseT))))
+
+## Type-checking on the input value is done during the analysis of a
+## "case" expression, to ensure that the patterns being used make
+## sense for the type of the input value.
+## Sometimes, that input value is complex, by depending on
+## type-variables or quantifications.
+## This function makes it easier for "case" analysis to properly
+## type-check the input with respect to the patterns.
+(def: (simplify-case-type caseT)
+  (-> Type (Meta Type))
+  (loop [envs (: (List (List Type))
+                 (list))
+         caseT caseT]
+    (.case caseT
+      (#.Var id)
+      (do macro.Monad<Meta>
+        [?caseT' (typeA.with-env
+                   (tc.read id))]
+        (.case ?caseT'
+          (#.Some caseT')
+          (recur envs caseT')
+
+          _
+          (lang.throw cannot-simplify-type-for-pattern-matching caseT)))
+
+      (#.Named name unnamedT)
+      (recur envs unnamedT)
+
+      (#.UnivQ env unquantifiedT)
+      (recur (#.Cons env envs) unquantifiedT)
+
+      (#.ExQ _)
+      (do macro.Monad<Meta>
+        [[ex-id exT] (typeA.with-env
+                       tc.existential)]
+        (recur envs (maybe.assume (type.apply (list exT) caseT))))
+
+      (#.Apply inputT funcT)
+      (.case funcT
+        (#.Var funcT-id)
+        (do macro.Monad<Meta>
+          [funcT' (typeA.with-env
+                    (do tc.Monad<Check>
+                      [?funct' (tc.read funcT-id)]
+                      (.case ?funct'
+                        (#.Some funct')
+                        (wrap funct')
+
+                        _
+                        (tc.throw cannot-simplify-type-for-pattern-matching caseT))))]
+          (recur envs (#.Apply inputT funcT')))
+
+        _
+        (.case (type.apply (list inputT) funcT)
+          (#.Some outputT)
+          (recur envs outputT)
+
+          #.None
+          (lang.throw cannot-simplify-type-for-pattern-matching caseT)))
+
+      (#.Product _)
+      (|> caseT
+          type.flatten-tuple
+          (list/map (re-quantify envs))
+          type.tuple
+          (:: macro.Monad<Meta> wrap))
+
+      _
+      (:: macro.Monad<Meta> wrap (re-quantify envs caseT)))))
+
+(def: (analyse-primitive type inputT cursor output next)
+  (All [a] (-> Type Type Cursor Pattern (Meta a) (Meta [Pattern a])))
+  (lang.with-cursor cursor
+    (do macro.Monad<Meta>
+      [_ (typeA.with-env
+           (tc.check inputT type))
+       outputA next]
+      (wrap [output outputA]))))
+
+## This function handles several concerns at once, but it must be that
+## way because those concerns are interleaved when doing
+## pattern-matching and they cannot be separated.
+## The pattern is analysed in order to get a general feel for what is
+## expected of the input value. This, in turn, informs the
+## type-checking of the input.
+## A kind of "continuation" value is passed around which signifies
+## what needs to be done _after_ analysing a pattern.
+## In general, this is done to analyse the "body" expression
+## associated to a particular pattern _in the context of_ said
+## pattern.
+## The reason why *context* is important is because patterns may bind
+## values to local variables, which may in turn be referenced in the
+## body expressions.
+## That is why the body must be analysed in the context of the
+## pattern, and not separately.
+(def: (analyse-pattern num-tags inputT pattern next)
+  (All [a] (-> (Maybe Nat) Type Code (Meta a) (Meta [Pattern a])))
+  (.case pattern
+    [cursor (#.Symbol ["" name])]
+    (lang.with-cursor cursor
+      (do macro.Monad<Meta>
+        [outputA (scopeL.with-local [name inputT]
+                   next)
+         idx scopeL.next-local]
+        (wrap [(#analysisL.Bind idx) outputA])))
+
+    (^template [<type> <input> <output>]
+      [cursor <input>]
+      (analyse-primitive <type> inputT cursor (#analysisL.Simple <output>) next))
+    ([Bool (#.Bool pattern-value) (#analysisL.Bool pattern-value)]
+     [Nat  (#.Nat pattern-value)  (#analysisL.Nat pattern-value)]
+     [Int  (#.Int pattern-value)  (#analysisL.Int pattern-value)]
+     [Deg  (#.Deg pattern-value)  (#analysisL.Deg pattern-value)]
+     [Frac (#.Frac pattern-value) (#analysisL.Frac pattern-value)]
+     [Text (#.Text pattern-value) (#analysisL.Text pattern-value)]
+     [Top  (#.Tuple #.Nil)        #analysisL.Unit])
+    
+    (^ [cursor (#.Tuple (list singleton))])
+    (analyse-pattern #.None inputT singleton next)
+    
+    [cursor (#.Tuple sub-patterns)]
+    (lang.with-cursor cursor
+      (do macro.Monad<Meta>
+        [inputT' (simplify-case-type inputT)]
+        (.case inputT'
+          (#.Product _)
+          (let [sub-types (type.flatten-tuple inputT')
+                num-sub-types (maybe.default (list.size sub-types)
+                                             num-tags)
+                num-sub-patterns (list.size sub-patterns)
+                matches (cond (n/< num-sub-types num-sub-patterns)
+                              (let [[prefix suffix] (list.split (dec num-sub-patterns) sub-types)]
+                                (list.zip2 (list/compose prefix (list (type.tuple suffix))) sub-patterns))
+
+                              (n/> num-sub-types num-sub-patterns)
+                              (let [[prefix suffix] (list.split (dec num-sub-types) sub-patterns)]
+                                (list.zip2 sub-types (list/compose prefix (list (code.tuple suffix)))))
+                              
+                              ## (n/= num-sub-types num-sub-patterns)
+                              (list.zip2 sub-types sub-patterns))]
+            (do @
+              [[memberP+ thenA] (list/fold (: (All [a]
+                                                (-> [Type Code] (Meta [(List Pattern) a])
+                                                    (Meta [(List Pattern) a])))
+                                              (function (_ [memberT memberC] then)
+                                                (do @
+                                                  [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Meta a) (Meta [Pattern a])))
+                                                                                   analyse-pattern)
+                                                                               #.None memberT memberC then)]
+                                                  (wrap [(list& memberP memberP+) thenA]))))
+                                           (do @
+                                             [nextA next]
+                                             (wrap [(list) nextA]))
+                                           (list.reverse matches))]
+              (wrap [(analysisL.product-pattern memberP+)
+                     thenA])))
+
+          _
+          (lang.throw cannot-match-type-with-pattern [inputT pattern])
+          )))
+
+    [cursor (#.Record record)]
+    (do macro.Monad<Meta>
+      [record (structureA.normalize record)
+       [members recordT] (structureA.order record)
+       _ (typeA.with-env
+           (tc.check inputT recordT))]
+      (analyse-pattern (#.Some (list.size members)) inputT [cursor (#.Tuple members)] next))
+
+    [cursor (#.Tag tag)]
+    (lang.with-cursor cursor
+      (analyse-pattern #.None inputT (` ((~ pattern))) next))
+
+    (^ [cursor (#.Form (list& [_ (#.Nat idx)] values))])
+    (lang.with-cursor cursor
+      (do macro.Monad<Meta>
+        [inputT' (simplify-case-type inputT)]
+        (.case inputT'
+          (#.Sum _)
+          (let [flat-sum (type.flatten-variant inputT')
+                size-sum (list.size flat-sum)
+                num-cases (maybe.default size-sum num-tags)]
+            (.case (list.nth idx flat-sum)
+              (^multi (#.Some case-type)
+                      (n/< num-cases idx))
+              (do macro.Monad<Meta>
+                [[testP nextA] (if (and (n/> num-cases size-sum)
+                                        (n/= (dec num-cases) idx))
+                                 (analyse-pattern #.None
+                                                  (type.variant (list.drop (dec num-cases) flat-sum))
+                                                  (` [(~+ values)])
+                                                  next)
+                                 (analyse-pattern #.None case-type (` [(~+ values)]) next))]
+                (wrap [(analysisL.sum-pattern num-cases idx testP)
+                       nextA]))
+
+              _
+              (lang.throw sum-type-has-no-case [idx inputT])))
+
+          _
+          (lang.throw cannot-match-type-with-pattern [inputT pattern]))))
+
+    (^ [cursor (#.Form (list& [_ (#.Tag tag)] values))])
+    (lang.with-cursor cursor
+      (do macro.Monad<Meta>
+        [tag (macro.normalize tag)
+         [idx group variantT] (macro.resolve-tag tag)
+         _ (typeA.with-env
+             (tc.check inputT variantT))]
+        (analyse-pattern (#.Some (list.size group)) inputT (` ((~ (code.nat idx)) (~+ values))) next)))
+
+    _
+    (lang.throw unrecognized-pattern-syntax pattern)
+    ))
+
+(def: #export (case analyse inputC branches)
+  (-> Analyser Code (List [Code Code]) (Meta Analysis))
+  (.case branches
+    #.Nil
+    (lang.throw cannot-have-empty-branches "")
+
+    (#.Cons [patternH bodyH] branchesT)
+    (do macro.Monad<Meta>
+      [[inputT inputA] (typeA.with-inference
+                         (analyse inputC))
+       outputH (analyse-pattern #.None inputT patternH (analyse bodyH))
+       outputT (monad.map @
+                          (function (_ [patternT bodyT])
+                            (analyse-pattern #.None inputT patternT (analyse bodyT)))
+                          branchesT)
+       outputHC (|> outputH product.left coverageA.determine)
+       outputTC (monad.map @ (|>> product.left coverageA.determine) outputT)
+       _ (.case (monad.fold e.Monad<Error> coverageA.merge outputHC outputTC)
+           (#e.Success coverage)
+           (lang.assert non-exhaustive-pattern-matching ""
+                        (coverageA.exhaustive? coverage))
+
+           (#e.Error error)
+           (lang.fail error))]
+      (wrap (#analysisL.Case inputA [outputH outputT])))))
diff --git a/stdlib/source/lux/lang/analysis/case/coverage.lux b/stdlib/source/lux/lang/analysis/case/coverage.lux
new file mode 100644
index 000000000..da256206f
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/case/coverage.lux
@@ -0,0 +1,322 @@
+(.module:
+  lux
+  (lux (control [monad #+ do]
+                ["ex" exception #+ exception:]
+                equality)
+       (data [bool "bool/" Eq<Bool>]
+             [number]
+             ["e" error "error/" Monad<Error>]
+             [maybe]
+             text/format
+             (coll [list "list/" Fold<List>]
+                   (dictionary ["dict" unordered #+ Dict])))
+       [macro "macro/" Monad<Meta>]
+       [lang]
+       (lang [".L" analysis #+ Pattern Variant])))
+
+(def: cases
+  (-> (Maybe Nat) Nat)
+  (|>> (maybe.default +0)))
+
+(def: (variant sum-side)
+  (-> (Either Pattern Pattern) (Variant Pattern))
+  (loop [lefts +0
+         variantP sum-side]
+    (case variantP
+      (#.Left valueP)
+      (case valueP
+        (#analysisL.Complex (#analysisL.Sum value-side))
+        (recur (inc lefts) value-side)
+
+        _
+        {#analysisL.lefts lefts
+         #analysisL.right? false
+         #analysisL.value valueP})
+      
+      (#.Right valueP)
+      {#analysisL.lefts lefts
+       #analysisL.right? true
+       #analysisL.value valueP})))
+
+## The coverage of a pattern-matching expression summarizes how well
+## all the possible values of an input are being covered by the
+## different patterns involved.
+## Ideally, the pattern-matching has "exhaustive" coverage, which just
+## means that every possible value can be matched by at least 1
+## pattern.
+## Every other coverage is considered partial, and it would be valued
+## as insuficient (since it could lead to runtime errors due to values
+## not being handled by any pattern).
+## The #Partial tag covers arbitrary partial coverages in a general
+## way, while the other tags cover more specific cases for booleans
+## and variants.
+(type: #export #rec Coverage
+  #Partial
+  (#Bool Bool)
+  (#Variant (Maybe Nat) (Dict Nat Coverage))
+  (#Seq Coverage Coverage)
+  (#Alt Coverage Coverage)
+  #Exhaustive)
+
+(def: #export (exhaustive? coverage)
+  (-> Coverage Bool)
+  (case coverage
+    (#Exhaustive _)
+    true
+
+    _
+    false))
+
+(def: #export (determine pattern)
+  (-> Pattern (Meta Coverage))
+  (case pattern
+    (^or (#analysisL.Simple #analysisL.Unit)
+         (#analysisL.Bind _))
+    (macro/wrap #Exhaustive)
+
+    ## Primitive patterns always have partial coverage because there
+    ## are too many possibilities as far as values go.
+    (^template [<tag>]
+      (#analysisL.Simple (<tag> _))
+      (macro/wrap #Partial))
+    ([#analysisL.Nat]
+     [#analysisL.Int]
+     [#analysisL.Deg]
+     [#analysisL.Frac]
+     [#analysisL.Text])
+
+    ## Bools are the exception, since there is only "true" and
+    ## "false", which means it is possible for boolean
+    ## pattern-matching to become exhaustive if complementary parts meet.
+    (#analysisL.Simple (#analysisL.Bool value))
+    (macro/wrap (#Bool value))
+
+    ## Tuple patterns can be exhaustive if there is exhaustiveness for all of
+    ## their sub-patterns.
+    (#analysisL.Complex (#analysisL.Product [left right]))
+    (do macro.Monad<Meta>
+      [left (determine left)
+       right (determine right)]
+      (case right
+        (#Exhaustive _)
+        (wrap left)
+
+        _
+        (wrap (#Seq left right))))
+
+    (#analysisL.Complex (#analysisL.Sum sum-side))
+    (let [[variant-lefts variant-right? variant-value] (variant sum-side)]
+      ## Variant patterns can be shown to be exhaustive if all the possible
+      ## cases are handled exhaustively.
+      (do macro.Monad<Meta>
+        [value-coverage (determine variant-value)
+         #let [variant-idx (if variant-right?
+                             (inc variant-lefts)
+                             variant-lefts)]]
+        (wrap (#Variant (if variant-right?
+                          (#.Some variant-idx)
+                          #.None)
+                        (|> (dict.new number.Hash<Nat>)
+                            (dict.put variant-idx value-coverage))))))))
+
+(def: (xor left right)
+  (-> Bool Bool Bool)
+  (or (and left (not right))
+      (and (not left) right)))
+
+## The coverage checker not only verifies that pattern-matching is
+## exhaustive, but also that there are no redundant patterns.
+## Redundant patterns will never be executed, since there will
+## always be a pattern prior to them that would match the input.
+## Because of that, the presence of redundant patterns is assumed to
+## be a bug, likely due to programmer carelessness.
+(def: redundant-pattern
+  (e.Error Coverage)
+  (e.fail "Redundant pattern."))
+
+(def: (flatten-alt coverage)
+  (-> Coverage (List Coverage))
+  (case coverage
+    (#Alt left right)
+    (list& left (flatten-alt right))
+
+    _
+    (list coverage)))
+
+(struct: _ (Eq Coverage)
+  (def: (= reference sample)
+    (case [reference sample]
+      [#Exhaustive #Exhaustive]
+      true
+
+      [(#Bool sideR) (#Bool sideS)]
+      (bool/= sideR sideS)
+
+      [(#Variant allR casesR) (#Variant allS casesS)]
+      (and (n/= (cases allR)
+                (cases allS))
+           (:: (dict.Eq<Dict> =) = casesR casesS))
+      
+      [(#Seq leftR rightR) (#Seq leftS rightS)]
+      (and (= leftR leftS)
+           (= rightR rightS))
+
+      [(#Alt _) (#Alt _)]
+      (let [flatR (flatten-alt reference)
+            flatS (flatten-alt sample)]
+        (and (n/= (list.size flatR) (list.size flatS))
+             (list.every? (function (_ [coverageR coverageS])
+                            (= coverageR coverageS))
+                          (list.zip2 flatR flatS))))
+
+      _
+      false)))
+
+(open Eq<Coverage> "C/")
+
+## After determining the coverage of each individual pattern, it is
+## necessary to merge them all to figure out if the entire
+## pattern-matching expression is exhaustive and whether it contains
+## redundant patterns.
+(def: #export (merge addition so-far)
+  (-> Coverage Coverage (e.Error Coverage))
+  (case [addition so-far]
+    ## The addition cannot possibly improve the coverage.
+    [_ #Exhaustive]
+    redundant-pattern
+
+    ## The addition completes the coverage.
+    [#Exhaustive _]
+    (error/wrap #Exhaustive)
+
+    [#Partial #Partial]
+    (error/wrap #Partial)
+
+    ## 2 boolean coverages are exhaustive if they compliment one another.
+    (^multi [(#Bool sideA) (#Bool sideSF)]
+            (xor sideA sideSF))
+    (error/wrap #Exhaustive)
+
+    [(#Variant allA casesA) (#Variant allSF casesSF)]
+    (cond (not (n/= (cases allSF) (cases allA)))
+          (e.fail "Variants do not match.")
+
+          (:: (dict.Eq<Dict> Eq<Coverage>) = casesSF casesA)
+          redundant-pattern
+
+          ## else
+          (do e.Monad<Error>
+            [casesM (monad.fold @
+                                (function (_ [tagA coverageA] casesSF')
+                                  (case (dict.get tagA casesSF')
+                                    (#.Some coverageSF)
+                                    (do @
+                                      [coverageM (merge coverageA coverageSF)]
+                                      (wrap (dict.put tagA coverageM casesSF')))
+
+                                    #.None
+                                    (wrap (dict.put tagA coverageA casesSF'))))
+                                casesSF (dict.entries casesA))]
+            (wrap (if (let [case-coverages (dict.values casesM)]
+                        (and (n/= (cases allSF) (list.size case-coverages))
+                             (list.every? exhaustive? case-coverages)))
+                    #Exhaustive
+                    (#Variant allSF casesM)))))
+
+    [(#Seq leftA rightA) (#Seq leftSF rightSF)]
+    (case [(C/= leftSF leftA) (C/= rightSF rightA)]
+      ## There is nothing the addition adds to the coverage.
+      [true true]
+      redundant-pattern
+
+      ## The 2 sequences cannot possibly be merged.
+      [false false]
+      (error/wrap (#Alt so-far addition))
+
+      ## Same prefix
+      [true false]
+      (do e.Monad<Error>
+        [rightM (merge rightA rightSF)]
+        (if (exhaustive? rightM)
+          ## If all that follows is exhaustive, then it can be safely dropped
+          ## (since only the "left" part would influence whether the
+          ## merged coverage is exhaustive or not).
+          (wrap leftSF)
+          (wrap (#Seq leftSF rightM))))
+
+      ## Same suffix
+      [false true]
+      (do e.Monad<Error>
+        [leftM (merge leftA leftSF)]
+        (wrap (#Seq leftM rightA))))
+    
+    ## The left part will always match, so the addition is redundant.
+    (^multi [(#Seq left right) single]
+            (C/= left single))
+    redundant-pattern
+
+    ## The right part is not necessary, since it can always match the left.
+    (^multi [single (#Seq left right)]
+            (C/= left single))
+    (error/wrap single)
+
+    ## When merging a new coverage against one based on Alt, it may be
+    ## that one of the many coverages in the Alt is complementary to
+    ## the new one, so effort must be made to fuse carefully, to match
+    ## the right coverages together.
+    ## If one of the Alt sub-coverages matches the new one, the cycle
+    ## must be repeated, in case the resulting coverage can now match
+    ## other ones in the original Alt.
+    ## This process must be repeated until no further productive
+    ## merges can be done.
+    [_ (#Alt leftS rightS)]
+    (do e.Monad<Error>
+      [#let [fuse-once (: (-> Coverage (List Coverage)
+                              (e.Error [(Maybe Coverage)
+                                        (List Coverage)]))
+                          (function (_ coverage possibilities)
+                            (loop [alts possibilities]
+                              (case alts
+                                #.Nil
+                                (wrap [#.None (list coverage)])
+                                
+                                (#.Cons alt alts')
+                                (case (merge coverage alt)
+                                  (#e.Success altM)
+                                  (case altM
+                                    (#Alt _)
+                                    (do @
+                                      [[success alts+] (recur alts')]
+                                      (wrap [success (#.Cons alt alts+)]))
+
+                                    _
+                                    (wrap [(#.Some altM) alts']))
+                                  
+                                  (#e.Error error)
+                                  (e.fail error))
+                                ))))]
+       [success possibilities] (fuse-once addition (flatten-alt so-far))]
+      (loop [success success
+             possibilities possibilities]
+        (case success
+          (#.Some coverage')
+          (do @
+            [[success' possibilities'] (fuse-once coverage' possibilities)]
+            (recur success' possibilities'))
+          
+          #.None
+          (case (list.reverse possibilities)
+            (#.Cons last prevs)
+            (wrap (list/fold (function (_ left right) (#Alt left right))
+                             last
+                             prevs))
+
+            #.Nil
+            (undefined)))))
+
+    _
+    (if (C/= so-far addition)
+      ## The addition cannot possibly improve the coverage.
+      redundant-pattern
+      ## There are now 2 alternative paths.
+      (error/wrap (#Alt so-far addition)))))
diff --git a/stdlib/source/lux/lang/analysis/structure.lux b/stdlib/source/lux/lang/analysis/structure.lux
index cc185ebe9..8e3611e67 100644
--- a/stdlib/source/lux/lang/analysis/structure.lux
+++ b/stdlib/source/lux/lang/analysis/structure.lux
@@ -89,7 +89,7 @@
             (do @
               [valueA (typeA.with-type variant-type
                         (analyse valueC))]
-              (wrap (analysis.sum type-size tag valueA)))
+              (wrap (analysis.sum-analysis type-size tag valueA)))
 
             #.None
             (lang.throw inferenceA.variant-tag-out-of-bounds [type-size tag expectedT])))
@@ -219,7 +219,7 @@
                _ (typeA.with-env
                    (tc.check expectedT
                              (type.tuple (list/map product.left membersTA))))]
-              (wrap (analysis.product (list/map product.right membersTA))))))
+              (wrap (analysis.product-analysis (list/map product.right membersTA))))))
 
         (^template [<tag> <instancer>]
           (<tag> _)
@@ -268,7 +268,7 @@
         [#let [case-size (list.size group)]
          inferenceT (inferenceA.variant idx case-size variantT)
          [inferredT valueA+] (inferenceA.general analyse inferenceT (list valueC))]
-        (wrap (analysis.sum case-size idx (|> valueA+ list.head maybe.assume))))
+        (wrap (analysis.sum-analysis case-size idx (|> valueA+ list.head maybe.assume))))
 
       _
       (..sum analyse idx valueC))))
@@ -352,7 +352,7 @@
           (do @
             [inferenceT (inferenceA.record recordT)
              [inferredT membersA] (inferenceA.general analyse inferenceT membersC)]
-            (wrap (analysis.product membersA)))
+            (wrap (analysis.product-analysis membersA)))
 
           _
           (..product analyse membersC))))))
diff --git a/stdlib/test/test/lux/lang/analysis/case.lux b/stdlib/test/test/lux/lang/analysis/case.lux
new file mode 100644
index 000000000..9e775f8a3
--- /dev/null
+++ b/stdlib/test/test/lux/lang/analysis/case.lux
@@ -0,0 +1,194 @@
+(.module:
+  lux
+  (lux [io]
+       (control [monad #+ do]
+                pipe)
+       (data [bool "B/" Eq<Bool>]
+             ["R" error]
+             [product]
+             [maybe]
+             [text "T/" Eq<Text>]
+             text/format
+             (coll [list "list/" Monad<List>]
+                   (set ["set" unordered])))
+       ["r" math/random "r/" Monad<Random>]
+       [macro #+ Monad<Meta>]
+       (macro [code])
+       [lang]
+       (lang [type "type/" Eq<Type>]
+             (type ["tc" check])
+             [".L" module]
+             (analysis [".A" type]
+                       ["/" case]))
+       test)
+  (// ["_." primitive]
+      ["_." structure]))
+
+(def: (exhaustive-weaving branchings)
+  (-> (List (List Code)) (List (List Code)))
+  (case branchings
+    #.Nil
+    #.Nil
+
+    (#.Cons head+ #.Nil)
+    (list/map (|>> list) head+)
+
+    (#.Cons head+ tail++)
+    (do list.Monad<List>
+      [tail+ (exhaustive-weaving tail++)
+       head head+]
+      (wrap (#.Cons head tail+)))))
+
+(def: #export (exhaustive-branches allow-literals? variantTC inputC)
+  (-> Bool (List [Code Code]) Code (r.Random (List Code)))
+  (case inputC
+    [_ (#.Bool _)]
+    (r/wrap (list (' true) (' false)))
+
+    (^template [<tag> <gen> <wrapper>]
+      [_ (<tag> _)]
+      (if allow-literals?
+        (do r.Monad<Random>
+          [?sample (r.maybe <gen>)]
+          (case ?sample
+            (#.Some sample)
+            (do @
+              [else (exhaustive-branches allow-literals? variantTC inputC)]
+              (wrap (list& (<wrapper> sample) else)))
+
+            #.None
+            (wrap (list (' _)))))
+        (r/wrap (list (' _)))))
+    ([#.Nat  r.nat          code.nat]
+     [#.Int  r.int          code.int]
+     [#.Deg  r.deg          code.deg]
+     [#.Frac r.frac         code.frac]
+     [#.Text (r.unicode +5) code.text])
+    
+    (^ [_ (#.Tuple (list))])
+    (r/wrap (list (' [])))
+
+    (^ [_ (#.Record (list))])
+    (r/wrap (list (' {})))
+
+    [_ (#.Tuple members)]
+    (do r.Monad<Random>
+      [member-wise-patterns (monad.map @ (exhaustive-branches allow-literals? variantTC) members)]
+      (wrap (|> member-wise-patterns
+                exhaustive-weaving
+                (list/map code.tuple))))
+
+    [_ (#.Record kvs)]
+    (do r.Monad<Random>
+      [#let [ks (list/map product.left kvs)
+             vs (list/map product.right kvs)]
+       member-wise-patterns (monad.map @ (exhaustive-branches allow-literals? variantTC) vs)]
+      (wrap (|> member-wise-patterns
+                exhaustive-weaving
+                (list/map (|>> (list.zip2 ks) code.record)))))
+
+    (^ [_ (#.Form (list [_ (#.Tag _)] _))])
+    (do r.Monad<Random>
+      [bundles (monad.map @
+                          (function (_ [_tag _code])
+                            (do @
+                              [v-branches (exhaustive-branches allow-literals? variantTC _code)]
+                              (wrap (list/map (function (_ pattern) (` ((~ _tag) (~ pattern))))
+                                              v-branches))))
+                          variantTC)]
+      (wrap (list/join bundles)))
+
+    _
+    (r/wrap (list))
+    ))
+
+(def: #export (input variant-tags record-tags primitivesC)
+  (-> (List Code) (List Code) (List Code) (r.Random Code))
+  (r.rec
+   (function (_ input)
+     ($_ r.either
+         (r/map product.right _primitive.primitive)
+         (do r.Monad<Random>
+           [choice (|> r.nat (:: @ map (n/% (list.size variant-tags))))
+            #let [choiceT (maybe.assume (list.nth choice variant-tags))
+                  choiceC (maybe.assume (list.nth choice primitivesC))]]
+           (wrap (` ((~ choiceT) (~ choiceC)))))
+         (do r.Monad<Random>
+           [size (|> r.nat (:: @ map (n/% +3)))
+            elems (r.list size input)]
+           (wrap (code.tuple elems)))
+         (r/wrap (code.record (list.zip2 record-tags primitivesC)))
+         ))))
+
+(def: (branch body pattern)
+  (-> Code Code [Code Code])
+  [pattern body])
+
+(context: "Pattern-matching."
+  ## #seed +9253409297339902486
+  ## #seed +3793366152923578600
+  (<| (seed +5004137551292836565)
+      ## (times +100)
+      (do @
+        [module-name (r.unicode +5)
+         variant-name (r.unicode +5)
+         record-name (|> (r.unicode +5) (r.filter (|>> (T/= variant-name) not)))
+         size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+         variant-tags (|> (r.set text.Hash<Text> size (r.unicode +5)) (:: @ map set.to-list))
+         record-tags (|> (r.set text.Hash<Text> size (r.unicode +5)) (:: @ map set.to-list))
+         primitivesTC (r.list size _primitive.primitive)
+         #let [primitivesT (list/map product.left primitivesTC)
+               primitivesC (list/map product.right primitivesTC)
+               code-tag (|>> [module-name] code.tag)
+               variant-tags+ (list/map code-tag variant-tags)
+               record-tags+ (list/map code-tag record-tags)
+               variantTC (list.zip2 variant-tags+ primitivesC)]
+         inputC (input variant-tags+ record-tags+ primitivesC)
+         [outputT outputC] _primitive.primitive
+         [heterogeneousT heterogeneousC] (|> _primitive.primitive
+                                             (r.filter (|>> product.left (tc.checks? outputT) not)))
+         exhaustive-patterns (exhaustive-branches true variantTC inputC)
+         redundant-patterns (exhaustive-branches false variantTC inputC)
+         redundancy-idx (|> r.nat (:: @ map (n/% (list.size redundant-patterns))))
+         heterogeneous-idx (|> r.nat (:: @ map (n/% (list.size exhaustive-patterns))))
+         #let [exhaustive-branchesC (list/map (branch outputC)
+                                              exhaustive-patterns)
+               non-exhaustive-branchesC (list.take (dec (list.size exhaustive-branchesC))
+                                                   exhaustive-branchesC)
+               redundant-branchesC (<| (list/map (branch outputC))
+                                       list.concat
+                                       (list (list.take redundancy-idx redundant-patterns)
+                                             (list (maybe.assume (list.nth redundancy-idx redundant-patterns)))
+                                             (list.drop redundancy-idx redundant-patterns)))
+               heterogeneous-branchesC (list.concat (list (list.take heterogeneous-idx exhaustive-branchesC)
+                                                          (list (let [[_pattern _body] (maybe.assume (list.nth heterogeneous-idx exhaustive-branchesC))]
+                                                                  [_pattern heterogeneousC]))
+                                                          (list.drop (inc heterogeneous-idx) exhaustive-branchesC)))
+               analyse-pm (|>> (/.case _primitive.analyse inputC)
+                               (typeA.with-type outputT)
+                               lang.with-scope
+                               (do Monad<Meta>
+                                 [_ (moduleL.declare-tags variant-tags false
+                                                          (#.Named [module-name variant-name]
+                                                                   (type.variant primitivesT)))
+                                  _ (moduleL.declare-tags record-tags false
+                                                          (#.Named [module-name record-name]
+                                                                   (type.tuple primitivesT)))])
+                               (moduleL.with-module +0 module-name))]]
+        ($_ seq
+            (test "Will reject empty pattern-matching (no branches)."
+                  (|> (analyse-pm (list))
+                      _structure.check-fails))
+            (test "Can analyse exhaustive pattern-matching."
+                  (|> (analyse-pm exhaustive-branchesC)
+                      _structure.check-succeeds))
+            (test "Will reject non-exhaustive pattern-matching."
+                  (|> (analyse-pm non-exhaustive-branchesC)
+                      _structure.check-fails))
+            (test "Will reject redundant pattern-matching."
+                  (|> (analyse-pm redundant-branchesC)
+                      _structure.check-fails))
+            (test "Will reject pattern-matching if the bodies of the branches do not all have the same type."
+                  (|> (analyse-pm heterogeneous-branchesC)
+                      _structure.check-fails))
+            ))))
diff --git a/stdlib/test/test/lux/lang/analysis/primitive.lux b/stdlib/test/test/lux/lang/analysis/primitive.lux
index ed9d8bfc6..8e4ca6dde 100644
--- a/stdlib/test/test/lux/lang/analysis/primitive.lux
+++ b/stdlib/test/test/lux/lang/analysis/primitive.lux
@@ -17,7 +17,7 @@
                        [".A" expression]))
        test))
 
-(def: analyse (expressionA.analyser (:! lang.Eval [])))
+(def: #export analyse (expressionA.analyser (:! lang.Eval [])))
 
 (def: unit
   (r.Random Code)
diff --git a/stdlib/test/test/lux/lang/analysis/structure.lux b/stdlib/test/test/lux/lang/analysis/structure.lux
index ad6691287..20b911714 100644
--- a/stdlib/test/test/lux/lang/analysis/structure.lux
+++ b/stdlib/test/test/lux/lang/analysis/structure.lux
@@ -19,7 +19,7 @@
              (type ["tc" check])
              [".L" module]
              [".L" init]
-             [".L" analysis #+ Analysis]
+             [".L" analysis #+ Analysis Variant Tag]
              (analysis [".A" type]
                        ["/" structure]
                        [".A" expression]))
@@ -43,7 +43,7 @@
   )
 
 (def: (check-sum' size tag variant)
-  (-> Nat analysisL.Tag analysisL.Variant Bool)
+  (-> Nat Tag (Variant Analysis) Bool)
   (let [variant-tag (if (get@ #analysisL.right? variant)
                       (inc (get@ #analysisL.lefts variant))
                       (get@ #analysisL.lefts variant))]
@@ -52,7 +52,7 @@
         (and (n/= tag variant-tag)))))
 
 (def: (check-sum type size tag analysis)
-  (-> Type Nat analysisL.Tag (Meta Analysis) Bool)
+  (-> Type Nat Tag (Meta Analysis) Bool)
   (|> analysis
       (typeA.with-type type)
       (macro.run (initL.compiler []))
@@ -71,7 +71,7 @@
        (moduleL.with-module +0 module)))
 
 (def: (check-variant module tags type size tag analysis)
-  (-> Text (List moduleL.Tag) Type Nat analysisL.Tag (Meta Analysis) Bool)
+  (-> Text (List moduleL.Tag) Type Nat Tag (Meta Analysis) Bool)
   (|> analysis
       (tagged module tags type)
       (typeA.with-type type)