- Migrated structure analysis to stdlib.

- Added an easy way to report information in exceptions.

10 files changed, 1453 insertions, 41 deletions

diff --git a/stdlib/source/lux/control/exception.lux b/stdlib/source/lux/control/exception.lux
index b515f6c6b..d866c153e 100644
--- a/stdlib/source/lux/control/exception.lux
+++ b/stdlib/source/lux/control/exception.lux
@@ -4,8 +4,9 @@
                 ["p" parser])
        (data ["e" error]
              [maybe]
+             [product]
              [text "text/" Monoid<Text>]
-             (coll [list "list/" Functor<List>]))
+             (coll [list "list/" Functor<List> Fold<List>]))
        [macro]
        (macro [code]
               ["s" syntax #+ syntax: Syntax]
@@ -99,3 +100,22 @@
                                            ((~! text/compose) (~ g!descriptor)
                                             (~ (maybe.default (' "") body))))})))))
       )))
+
+(def: #export (report' entries)
+  (-> (List [Text Text]) Text)
+  (let [largest-header-size (|> entries
+                                (list/map (|>> product.left text.size))
+                                (list/fold n/max +0))]
+    (|> entries
+        (list/map (function (_ [header message])
+                    (let [padding (|> " "
+                                      (list.repeat (n/- (text.size header)
+                                                        largest-header-size))
+                                      (text.join-with ""))]
+                      ($_ text/compose padding header ": " message))))
+        (text.join-with "\n"))))
+
+(syntax: #export (report {entries (p.many (s.tuple (p.seq s.any s.any)))})
+  (wrap (list (` (report' (list (~+ (|> entries
+                                        (list/map (function (_ [header message])
+                                                    (` [(~ header) (~ message)])))))))))))
diff --git a/stdlib/source/lux/data/coll/dictionary/plist.lux b/stdlib/source/lux/data/coll/dictionary/plist.lux
new file mode 100644
index 000000000..e9e08107a
--- /dev/null
+++ b/stdlib/source/lux/data/coll/dictionary/plist.lux
@@ -0,0 +1,62 @@
+(.module:
+  lux
+  (lux (data [text "text/" Eq<Text>])))
+
+(type: #export (PList a)
+  (List [Text a]))
+
+(def: #export (get key properties)
+  (All [a] (-> Text (PList a) (Maybe a)))
+  (case properties
+    #.Nil
+    #.None
+
+    (#.Cons [k' v'] properties')
+    (if (text/= key k')
+      (#.Some v')
+      (get key properties'))))
+
+(def: #export (contains? key properties)
+  (All [a] (-> Text (PList a) Bool))
+  (case (get key properties)
+    (#.Some _)
+    true
+
+    #.None
+    false))
+
+(def: #export (put key val properties)
+  (All [a] (-> Text a (PList a) (PList a)))
+  (case properties
+    #.Nil
+    (list [key val])
+
+    (#.Cons [k' v'] properties')
+    (if (text/= key k')
+      (#.Cons [key val]
+              properties')
+      (#.Cons [k' v']
+              (put key val properties')))))
+
+(def: #export (update key f properties)
+  (All [a] (-> Text (-> a a) (PList a) (PList a)))
+  (case properties
+    #.Nil
+    #.Nil
+
+    (#.Cons [k' v'] properties')
+    (if (text/= key k')
+      (#.Cons [k' (f v')] properties')
+      (#.Cons [k' v'] (update key f properties')))))
+
+(def: #export (remove key properties)
+  (All [a] (-> Text (PList a) (PList a)))
+  (case properties
+    #.Nil
+    properties
+
+    (#.Cons [k' v'] properties')
+    (if (text/= key k')
+      properties'
+      (#.Cons [k' v']
+              (remove key properties')))))
diff --git a/stdlib/source/lux/lang.lux b/stdlib/source/lux/lang.lux
index c4a4e2db3..9f164b719 100644
--- a/stdlib/source/lux/lang.lux
+++ b/stdlib/source/lux/lang.lux
@@ -9,6 +9,9 @@
        [macro]
        (macro ["s" syntax #+ syntax:])))
 
+(type: #export Eval
+  (-> Type Code (Meta Top)))
+
 (def: #export (fail message)
   (All [a] (-> Text (Meta a)))
   (do macro.Monad<Meta>
diff --git a/stdlib/source/lux/lang/analysis.lux b/stdlib/source/lux/lang/analysis.lux
index 46927bae1..6b2ba097d 100644
--- a/stdlib/source/lux/lang/analysis.lux
+++ b/stdlib/source/lux/lang/analysis.lux
@@ -48,10 +48,12 @@
   (#Constant Ident)
   (#Special (Special Text)))
 
-## Variants get analysed as binary sum types for the sake of semantic
-## simplicity.
-## This is because you can encode a variant of any size using just
-## binary sums by nesting them.
+(type: #export Variant
+  {#lefts Nat
+   #right? Bool
+   #value Analysis})
+
+(type: #export Tuple (List Analysis))
 
 (do-template [<name> <tag>]
   [(def: <name>
@@ -71,8 +73,8 @@
   (let [identity (#Function (list) (#Variable (#Local +1)))]
     (#Apply value identity)))
 
-(def: #export (sum tag size temp value)
-  (-> Tag Nat Register Analysis Analysis)
+(def: #export (sum size tag value)
+  (-> Nat Tag Analysis Analysis)
   (if (last? size tag)
     (if (n/= +1 tag)
       (..right value)
@@ -88,8 +90,8 @@
                  value)
                (list.n/range +0 tag))))
 
-(def: #export (tuple members)
-  (-> (List Analysis) Analysis)
+(def: #export (product members)
+  (-> Tuple Analysis)
   (case (list.reverse members)
     #.Nil
     (#Primitive #Unit)
@@ -107,3 +109,35 @@
 
 (type: #export Analyser
   (-> Code (Meta Analysis)))
+
+(def: #export (tuple analysis)
+  (-> Analysis Tuple)
+  (case analysis
+    (#Structure (#Product left right))
+    (#.Cons left (tuple right))
+
+    _
+    (list analysis)))
+
+(def: #export (variant analysis)
+  (-> Analysis (Maybe Variant))
+  (loop [lefts +0
+         variantA analysis]
+    (case variantA
+      (#Structure (#Sum (#.Left valueA)))
+      (case valueA
+        (#Structure (#Sum _))
+        (recur (inc lefts) valueA)
+
+        _
+        (#.Some {#lefts lefts
+                 #right? false
+                 #value valueA}))
+      
+      (#Structure (#Sum (#.Right valueA)))
+      (#.Some {#lefts lefts
+               #right? true
+               #value valueA})
+
+      _
+      #.None)))
diff --git a/stdlib/source/lux/lang/analysis/expression.lux b/stdlib/source/lux/lang/analysis/expression.lux
new file mode 100644
index 000000000..a22e3d32b
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/expression.lux
@@ -0,0 +1,125 @@
+(.module:
+  lux
+  (lux (control [monad #+ do]
+                ["ex" exception #+ exception:])
+       (data ["e" error]
+             [product]
+             text/format)
+       [macro]
+       [lang #+ Eval]
+       (lang [type]
+             (type ["tc" check])
+             [".L" analysis #+ Analysis Analyser]
+             (analysis [".A" type]
+                       [".A" primitive]
+                       [".A" structure]
+                       ## [".A" function]
+                       ## [".A" reference]
+                       )
+             ## [".L" macro]
+             ## [".L" extension]
+             )))
+
+(exception: #export (macro-expansion-failed {message Text})
+  message)
+
+(do-template [<name>]
+  [(exception: #export (<name> {code Code})
+     (%code code))]
+
+  [macro-call-must-have-single-expansion]
+  [unrecognized-syntax]
+  )
+
+(def: #export (analyser eval)
+  (-> Eval Analyser)
+  (: (-> Code (Meta Analysis))
+     (function (analyse code)
+       (do macro.Monad<Meta>
+         [expectedT macro.expected-type]
+         (let [[cursor code'] code]
+           ## The cursor must be set in the compiler for the sake
+           ## of having useful error messages.
+           (lang.with-cursor cursor
+             (case code'
+               (^template [<tag> <analyser>]
+                 (<tag> value)
+                 (<analyser> value))
+               ([#.Bool primitiveA.bool]
+                [#.Nat  primitiveA.nat]
+                [#.Int  primitiveA.int]
+                [#.Deg  primitiveA.deg]
+                [#.Frac primitiveA.frac]
+                [#.Text primitiveA.text])
+
+               (^template [<tag> <analyser>]
+                 (^ (#.Form (list& [_ (<tag> tag)]
+                                   values)))
+                 (case values
+                   (#.Cons value #.Nil)
+                   (<analyser> analyse tag value)
+
+                   _
+                   (<analyser> analyse tag (` [(~+ values)]))))
+               ([#.Nat structureA.sum]
+                [#.Tag structureA.tagged-sum])
+
+               (#.Tag tag)
+               (structureA.tagged-sum analyse tag (' []))
+
+               (^ (#.Tuple (list)))
+               primitiveA.unit
+
+               (^ (#.Tuple (list singleton)))
+               (analyse singleton)
+
+               (^ (#.Tuple elems))
+               (structureA.product analyse elems)
+
+               (^ (#.Record pairs))
+               (structureA.record analyse pairs)
+
+               ## (#.Symbol reference)
+               ## (referenceA.analyse-reference reference)
+
+               ## (^ (#.Form (list& [_ (#.Text proc-name)] proc-args)))
+               ## (do macro.Monad<Meta>
+               ##   [procedure (extensionL.find-analysis proc-name)]
+               ##   (procedure analyse eval proc-args))
+
+               ## (^ (#.Form (list& func args)))
+               ## (do macro.Monad<Meta>
+               ##   [[funcT funcA] (typeA.with-inference
+               ##                    (analyse func))]
+               ##   (case funcA
+               ##     [_ (#.Symbol def-name)]
+               ##     (do @
+               ##       [?macro (lang.with-error-tracking
+               ##                 (macro.find-macro def-name))]
+               ##       (case ?macro
+               ##         (#.Some macro)
+               ##         (do @
+               ##           [expansion (: (Meta (List Code))
+               ##                         (function (_ compiler)
+               ##                           (case (macroL.expand macro args compiler)
+               ##                             (#e.Error error)
+               ##                             ((lang.throw macro-expansion-failed error) compiler)
+
+               ##                             output
+               ##                             output)))]
+               ##           (case expansion
+               ##             (^ (list single))
+               ##             (analyse single)
+
+               ##             _
+               ##             (lang.throw macro-call-must-have-single-expansion code)))
+
+               ##         _
+               ##         (functionA.analyse-apply analyse funcT funcA args)))
+
+               ##     _
+               ##     (functionA.analyse-apply analyse funcT funcA args)))
+
+               _
+               (lang.throw unrecognized-syntax code)
+               )))))))
diff --git a/stdlib/source/lux/lang/analysis/inference.lux b/stdlib/source/lux/lang/analysis/inference.lux
new file mode 100644
index 000000000..732a8e6e3
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/inference.lux
@@ -0,0 +1,256 @@
+(.module:
+  lux
+  (lux (control [monad #+ do]
+                ["ex" exception #+ exception:])
+       (data [maybe]
+             [text]
+             text/format
+             (coll [list "list/" Functor<List>]))
+       [macro "macro/" Monad<Meta>]
+       [lang]
+       (lang [type]
+             (type ["tc" check])
+             [analysis #+ Analysis Analyser]
+             (analysis [".A" type]))))
+
+(exception: #export (variant-tag-out-of-bounds {size Nat} {tag analysis.Tag} {type Type})
+  (ex.report ["Tag" (%n tag)]
+             ["Variant size" (%n size)]
+             ["Variant type" (%type type)]))
+
+(exception: #export (cannot-infer {type Type} {args (List Code)})
+  (ex.report ["Type" (%type type)]
+             ["Arguments" (|> args
+                              list.enumerate
+                              (list/map (function (_ [idx argC])
+                                          (format "\n  " (%n idx) " " (%code argC))))
+                              (text.join-with ""))]))
+
+(exception: #export (cannot-infer-argument {inferred Type} {argument Code})
+  (ex.report ["Inferred Type" (%type inferred)]
+             ["Argument" (%code argument)]))
+
+(exception: #export (smaller-variant-than-expected {expected Nat} {actual Nat})
+  (ex.report ["Expected" (%i (.int expected))]
+             ["Actual" (%i (.int actual))]))
+
+(do-template [<name>]
+  [(exception: #export (<name> {type Type})
+     (%type type))]
+
+  [not-a-variant-type]
+  [not-a-record-type]
+  [invalid-type-application]
+  )
+
+(def: (replace-bound bound-idx replacementT type)
+  (-> Nat Type Type Type)
+  (case type
+    (#.Primitive name params)
+    (#.Primitive name (list/map (replace-bound bound-idx replacementT) params))
+
+    (^template [<tag>]
+      (<tag> left right)
+      (<tag> (replace-bound bound-idx replacementT left)
+             (replace-bound bound-idx replacementT right)))
+    ([#.Sum]
+     [#.Product]
+     [#.Function]
+     [#.Apply])
+    
+    (#.Bound idx)
+    (if (n/= bound-idx idx)
+      replacementT
+      type)
+
+    (^template [<tag>]
+      (<tag> env quantified)
+      (<tag> (list/map (replace-bound bound-idx replacementT) env)
+             (replace-bound (n/+ +2 bound-idx) replacementT quantified)))
+    ([#.UnivQ]
+     [#.ExQ])
+    
+    _
+    type))
+
+(def: new-named-type
+  (Meta Type)
+  (do macro.Monad<Meta>
+    [[_module _line _column] macro.cursor
+     [ex-id exT] (typeA.with-env tc.existential)]
+    (wrap (#.Primitive (format "{New Type @ " (%t _module)
+                               "," (%n _line)
+                               "," (%n _column)
+                               "} " (%n ex-id))
+                       (list)))))
+
+## Type-inference works by applying some (potentially quantified) type
+## to a sequence of values.
+## Function types are used for this, although inference is not always
+## done for function application (alternative uses may be records and
+## tagged variants).
+## But, so long as the type being used for the inference can be treated
+## as a function type, this method of inference should work.
+(def: #export (general analyse inferT args)
+  (-> Analyser Type (List Code) (Meta [Type (List Analysis)]))
+  (case args
+    #.Nil
+    (do macro.Monad<Meta>
+      [_ (typeA.infer inferT)]
+      (wrap [inferT (list)]))
+    
+    (#.Cons argC args')
+    (case inferT
+      (#.Named name unnamedT)
+      (general analyse unnamedT args)
+
+      (#.UnivQ _)
+      (do macro.Monad<Meta>
+        [[var-id varT] (typeA.with-env tc.var)]
+        (general analyse (maybe.assume (type.apply (list varT) inferT)) args))
+
+      (#.ExQ _)
+      (do macro.Monad<Meta>
+        [[var-id varT] (typeA.with-env tc.var)
+         output (general analyse
+                         (maybe.assume (type.apply (list varT) inferT))
+                         args)
+         bound? (typeA.with-env
+                  (tc.bound? var-id))
+         _ (if bound?
+             (wrap [])
+             (do @
+               [newT new-named-type]
+               (typeA.with-env
+                 (tc.check varT newT))))]
+        (wrap output))
+
+      (#.Apply inputT transT)
+      (case (type.apply (list inputT) transT)
+        (#.Some outputT)
+        (general analyse outputT args)
+
+        #.None
+        (lang.throw invalid-type-application inferT))
+
+      ## Arguments are inferred back-to-front because, by convention,
+      ## Lux functions take the most important arguments *last*, which
+      ## means that the most information for doing proper inference is
+      ## located in the last arguments to a function call.
+      ## By inferring back-to-front, a lot of type-annotations can be
+      ## avoided in Lux code, since the inference algorithm can piece
+      ## things together more easily.
+      (#.Function inputT outputT)
+      (do macro.Monad<Meta>
+        [[outputT' args'A] (general analyse outputT args')
+         argA (lang.with-stacked-errors
+                (function (_ _)
+                  (ex.construct cannot-infer-argument [inputT argC]))
+                (typeA.with-type inputT
+                  (analyse argC)))]
+        (wrap [outputT' (list& argA args'A)]))
+
+      (#.Var infer-id)
+      (do macro.Monad<Meta>
+        [?inferT' (typeA.with-env (tc.read infer-id))]
+        (case ?inferT'
+          (#.Some inferT')
+          (general analyse inferT' args)
+
+          _
+          (lang.throw cannot-infer [inferT args])))
+
+      _
+      (lang.throw cannot-infer [inferT args]))
+    ))
+
+## Turns a record type into the kind of function type suitable for inference.
+(def: #export (record inferT)
+  (-> Type (Meta Type))
+  (case inferT
+    (#.Named name unnamedT)
+    (record unnamedT)
+
+    (^template [<tag>]
+      (<tag> env bodyT)
+      (do macro.Monad<Meta>
+        [bodyT+ (record bodyT)]
+        (wrap (<tag> env bodyT+))))
+    ([#.UnivQ]
+     [#.ExQ])
+
+    (#.Apply inputT funcT)
+    (case (type.apply (list inputT) funcT)
+      (#.Some outputT)
+      (record outputT)
+
+      #.None
+      (lang.throw invalid-type-application inferT))
+
+    (#.Product _)
+    (macro/wrap (type.function (type.flatten-tuple inferT) inferT))
+
+    _
+    (lang.throw not-a-record-type inferT)))
+
+## Turns a variant type into the kind of function type suitable for inference.
+(def: #export (variant tag expected-size inferT)
+  (-> Nat Nat Type (Meta Type))
+  (loop [depth +0
+         currentT inferT]
+    (case currentT
+      (#.Named name unnamedT)
+      (do macro.Monad<Meta>
+        [unnamedT+ (recur depth unnamedT)]
+        (wrap unnamedT+))
+
+      (^template [<tag>]
+        (<tag> env bodyT)
+        (do macro.Monad<Meta>
+          [bodyT+ (recur (inc depth) bodyT)]
+          (wrap (<tag> env bodyT+))))
+      ([#.UnivQ]
+       [#.ExQ])
+
+      (#.Sum _)
+      (let [cases (type.flatten-variant currentT)
+            actual-size (list.size cases)
+            boundary (dec expected-size)]
+        (cond (or (n/= expected-size actual-size)
+                  (and (n/> expected-size actual-size)
+                       (n/< boundary tag)))
+              (case (list.nth tag cases)
+                (#.Some caseT)
+                (macro/wrap (if (n/= +0 depth)
+                              (type.function (list caseT) currentT)
+                              (let [replace! (replace-bound (|> depth dec (n/* +2)) inferT)]
+                                (type.function (list (replace! caseT))
+                                  (replace! currentT)))))
+
+                #.None
+                (lang.throw variant-tag-out-of-bounds [expected-size tag inferT]))
+              
+              (n/< expected-size actual-size)
+              (lang.throw smaller-variant-than-expected [expected-size actual-size])
+
+              (n/= boundary tag)
+              (let [caseT (type.variant (list.drop boundary cases))]
+                (macro/wrap (if (n/= +0 depth)
+                              (type.function (list caseT) currentT)
+                              (let [replace! (replace-bound (|> depth dec (n/* +2)) inferT)]
+                                (type.function (list (replace! caseT))
+                                  (replace! currentT))))))
+              
+              ## else
+              (lang.throw variant-tag-out-of-bounds [expected-size tag inferT])))
+
+      (#.Apply inputT funcT)
+      (case (type.apply (list inputT) funcT)
+        (#.Some outputT)
+        (variant tag expected-size outputT)
+
+        #.None
+        (lang.throw invalid-type-application inferT))
+
+      _
+      (lang.throw not-a-variant-type inferT))))
diff --git a/stdlib/source/lux/lang/analysis/structure.lux b/stdlib/source/lux/lang/analysis/structure.lux
new file mode 100644
index 000000000..cc185ebe9
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/structure.lux
@@ -0,0 +1,358 @@
+(.module:
+  lux
+  (lux (control [monad #+ do]
+                ["ex" exception #+ exception:])
+       (data [ident]
+             [number]
+             [product]
+             [maybe]
+             (coll [list "list/" Functor<List>]
+                   (dictionary ["dict" unordered #+ Dict]))
+             text/format)
+       [macro]
+       (macro [code])
+       [lang]
+       (lang [type]
+             (type ["tc" check])
+             [analysis #+ Analysis Analyser]
+             (analysis [".A" type]
+                       [".A" primitive]
+                       [".A" inference]))))
+
+(exception: #export (invalid-variant-type {type Type} {tag analysis.Tag} {code Code})
+  (ex.report ["Type" (%type type)]
+             ["Tag" (%n tag)]
+             ["Expression" (%code code)]))
+
+(do-template [<name>]
+  [(exception: #export (<name> {type Type} {members (List Code)})
+     (ex.report ["Type" (%type type)]
+                ["Expression" (%code (` [(~+ members)]))]))]
+
+  [invalid-tuple-type]
+  [cannot-analyse-tuple]
+  )
+
+(exception: #export (not-a-quantified-type {type Type})
+  (%type type))
+
+(do-template [<name>]
+  [(exception: #export (<name> {type Type} {tag analysis.Tag} {code Code})
+     (ex.report ["Type" (%type type)]
+                ["Tag" (%n tag)]
+                ["Expression" (%code code)]))]
+
+  [cannot-analyse-variant]
+  [cannot-infer-numeric-tag]
+  )
+
+(exception: #export (record-keys-must-be-tags {key Code} {record (List [Code Code])})
+  (ex.report ["Key" (%code key)]
+             ["Record" (%code (code.record record))]))
+
+(do-template [<name>]
+  [(exception: #export (<name> {key Ident} {record (List [Ident Code])})
+     (ex.report ["Tag" (%code (code.tag key))]
+                ["Record" (%code (code.record (list/map (function (_ [keyI valC])
+                                                          [(code.tag keyI) valC])
+                                                        record)))]))]
+
+  [cannot-repeat-tag]
+  )
+
+(exception: #export (tag-does-not-belong-to-record {key Ident} {type Type})
+  (ex.report ["Tag" (%code (code.tag key))]
+             ["Type" (%type type)]))
+
+(exception: #export (record-size-mismatch {expected Nat} {actual Nat} {type Type} {record (List [Ident Code])})
+  (ex.report ["Expected" (|> expected .int %i)]
+             ["Actual" (|> actual .int %i)]
+             ["Type" (%type type)]
+             ["Expression" (%code (|> record
+                                      (list/map (function (_ [keyI valueC])
+                                                  [(code.tag keyI) valueC]))
+                                      code.record))]))
+
+(def: #export (sum analyse tag valueC)
+  (-> Analyser Nat Code (Meta Analysis))
+  (do macro.Monad<Meta>
+    [expectedT macro.expected-type]
+    (lang.with-stacked-errors
+      (function (_ _)
+        (ex.construct cannot-analyse-variant [expectedT tag valueC]))
+      (case expectedT
+        (#.Sum _)
+        (let [flat (type.flatten-variant expectedT)
+              type-size (list.size flat)]
+          (case (list.nth tag flat)
+            (#.Some variant-type)
+            (do @
+              [valueA (typeA.with-type variant-type
+                        (analyse valueC))]
+              (wrap (analysis.sum type-size tag valueA)))
+
+            #.None
+            (lang.throw inferenceA.variant-tag-out-of-bounds [type-size tag expectedT])))
+
+        (#.Named name unnamedT)
+        (typeA.with-type unnamedT
+          (sum analyse tag valueC))
+
+        (#.Var id)
+        (do @
+          [?expectedT' (typeA.with-env
+                         (tc.read id))]
+          (case ?expectedT'
+            (#.Some expectedT')
+            (typeA.with-type expectedT'
+              (sum analyse tag valueC))
+
+            _
+            ## Cannot do inference when the tag is numeric.
+            ## This is because there is no way of knowing how many
+            ## cases the inferred sum type would have.
+            (lang.throw cannot-infer-numeric-tag [expectedT tag valueC])
+            ))
+
+        (^template [<tag> <instancer>]
+          (<tag> _)
+          (do @
+            [[instance-id instanceT] (typeA.with-env <instancer>)]
+            (typeA.with-type (maybe.assume (type.apply (list instanceT) expectedT))
+              (sum analyse tag valueC))))
+        ([#.UnivQ tc.existential]
+         [#.ExQ tc.var])
+
+        (#.Apply inputT funT)
+        (case funT
+          (#.Var funT-id)
+          (do @
+            [?funT' (typeA.with-env (tc.read funT-id))]
+            (case ?funT'
+              (#.Some funT')
+              (typeA.with-type (#.Apply inputT funT')
+                (sum analyse tag valueC))
+
+              _
+              (lang.throw invalid-variant-type [expectedT tag valueC])))
+
+          _
+          (case (type.apply (list inputT) funT)
+            #.None
+            (lang.throw not-a-quantified-type funT)
+            
+            (#.Some outputT)
+            (typeA.with-type outputT
+              (sum analyse tag valueC))))
+        
+        _
+        (lang.throw invalid-variant-type [expectedT tag valueC])))))
+
+(def: (typed-product analyse membersC+)
+  (-> Analyser (List Code) (Meta Analysis))
+  (do macro.Monad<Meta>
+    [expectedT macro.expected-type]
+    (loop [expectedT expectedT
+           membersC+ membersC+]
+      (case [expectedT membersC+]
+        ## If the tuple runs out, whatever expression is the last gets
+        ## matched to the remaining type.
+        [tailT (#.Cons tailC #.Nil)]
+        (typeA.with-type tailT
+          (analyse tailC))
+
+        ## If the type and the code are still ongoing, match each
+        ## sub-expression to its corresponding type.
+        [(#.Product leftT rightT) (#.Cons leftC rightC)]
+        (do @
+          [leftA (typeA.with-type leftT
+                   (analyse leftC))
+           rightA (recur rightT rightC)]
+          (wrap (#analysis.Structure (#analysis.Product leftA rightA))))
+
+        ## If, however, the type runs out but there is still enough
+        ## tail, the remaining elements get packaged into another
+        ## tuple.
+        ## The reason for this is that it is assumed that the type of
+        ## the tuple represents the expectations of the user.
+        ## If the type is for a 3-tuple, but a 5-tuple is provided, it
+        ## is assumed that the user intended the following layout:
+        ## [0, 1, [2, 3, 4]]
+        ## but that, for whatever reason, it was written in a flat
+        ## way.
+        [tailT tailC]
+        (|> tailC
+            code.tuple
+            analyse
+            (typeA.with-type tailT)
+            (:: @ map analysis.no-op))))))
+
+(def: #export (product analyse membersC)
+  (-> Analyser (List Code) (Meta Analysis))
+  (do macro.Monad<Meta>
+    [expectedT macro.expected-type]
+    (lang.with-stacked-errors
+      (function (_ _)
+        (ex.construct cannot-analyse-tuple [expectedT membersC]))
+      (case expectedT
+        (#.Product _)
+        (..typed-product analyse membersC)
+
+        (#.Named name unnamedT)
+        (typeA.with-type unnamedT
+          (product analyse membersC))
+
+        (#.Var id)
+        (do @
+          [?expectedT' (typeA.with-env
+                         (tc.read id))]
+          (case ?expectedT'
+            (#.Some expectedT')
+            (typeA.with-type expectedT'
+              (product analyse membersC))
+
+            _
+            ## Must do inference...
+            (do @
+              [membersTA (monad.map @ (|>> analyse typeA.with-inference)
+                                    membersC)
+               _ (typeA.with-env
+                   (tc.check expectedT
+                             (type.tuple (list/map product.left membersTA))))]
+              (wrap (analysis.product (list/map product.right membersTA))))))
+
+        (^template [<tag> <instancer>]
+          (<tag> _)
+          (do @
+            [[instance-id instanceT] (typeA.with-env <instancer>)]
+            (typeA.with-type (maybe.assume (type.apply (list instanceT) expectedT))
+              (product analyse membersC))))
+        ([#.UnivQ tc.existential]
+         [#.ExQ tc.var])
+
+        (#.Apply inputT funT)
+        (case funT
+          (#.Var funT-id)
+          (do @
+            [?funT' (typeA.with-env (tc.read funT-id))]
+            (case ?funT'
+              (#.Some funT')
+              (typeA.with-type (#.Apply inputT funT')
+                (product analyse membersC))
+
+              _
+              (lang.throw invalid-tuple-type [expectedT membersC])))
+
+          _
+          (case (type.apply (list inputT) funT)
+            #.None
+            (lang.throw not-a-quantified-type funT)
+            
+            (#.Some outputT)
+            (typeA.with-type outputT
+              (product analyse membersC))))
+        
+        _
+        (lang.throw invalid-tuple-type [expectedT membersC])
+        ))))
+
+(def: #export (tagged-sum analyse tag valueC)
+  (-> Analyser Ident Code (Meta Analysis))
+  (do macro.Monad<Meta>
+    [tag (macro.normalize tag)
+     [idx group variantT] (macro.resolve-tag tag)
+     expectedT macro.expected-type]
+    (case expectedT
+      (#.Var _)
+      (do @
+        [#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))))
+
+      _
+      (..sum analyse idx valueC))))
+
+## There cannot be any ambiguity or improper syntax when analysing
+## records, so they must be normalized for further analysis.
+## Normalization just means that all the tags get resolved to their
+## canonical form (with their corresponding module identified).
+(def: #export (normalize record)
+  (-> (List [Code Code]) (Meta (List [Ident Code])))
+  (monad.map macro.Monad<Meta>
+             (function (_ [key val])
+               (case key
+                 [_ (#.Tag key)]
+                 (do macro.Monad<Meta>
+                   [key (macro.normalize key)]
+                   (wrap [key val]))
+
+                 _
+                 (lang.throw record-keys-must-be-tags [key record])))
+             record))
+
+## Lux already possesses the means to analyse tuples, so
+## re-implementing the same functionality for records makes no sense.
+## Records, thus, get transformed into tuples by ordering the elements.
+(def: #export (order record)
+  (-> (List [Ident Code]) (Meta [(List Code) Type]))
+  (case record
+    ## empty-record = empty-tuple = unit = []
+    #.Nil
+    (:: macro.Monad<Meta> wrap [(list) Top])
+
+    (#.Cons [head-k head-v] _)
+    (do macro.Monad<Meta>
+      [head-k (macro.normalize head-k)
+       [_ tag-set recordT] (macro.resolve-tag head-k)
+       #let [size-record (list.size record)
+             size-ts (list.size tag-set)]
+       _ (if (n/= size-ts size-record)
+           (wrap [])
+           (lang.throw record-size-mismatch [size-ts size-record recordT record]))
+       #let [tuple-range (list.n/range +0 (dec size-ts))
+             tag->idx (dict.from-list ident.Hash<Ident> (list.zip2 tag-set tuple-range))]
+       idx->val (monad.fold @
+                            (function (_ [key val] idx->val)
+                              (do @
+                                [key (macro.normalize key)]
+                                (case (dict.get key tag->idx)
+                                  #.None
+                                  (lang.throw tag-does-not-belong-to-record [key recordT])
+
+                                  (#.Some idx)
+                                  (if (dict.contains? idx idx->val)
+                                    (lang.throw cannot-repeat-tag [key record])
+                                    (wrap (dict.put idx val idx->val))))))
+                            (: (Dict Nat Code)
+                               (dict.new number.Hash<Nat>))
+                            record)
+       #let [ordered-tuple (list/map (function (_ idx) (maybe.assume (dict.get idx idx->val)))
+                                     tuple-range)]]
+      (wrap [ordered-tuple recordT]))
+    ))
+
+(def: #export (record analyse members)
+  (-> Analyser (List [Code Code]) (Meta Analysis))
+  (do macro.Monad<Meta>
+    [members (normalize members)
+     [membersC recordT] (order members)]
+    (case membersC
+      (^ (list))
+      primitiveA.unit
+      
+      (^ (list singletonC))
+      (analyse singletonC)
+
+      _
+      (do @
+        [expectedT macro.expected-type]
+        (case expectedT
+          (#.Var _)
+          (do @
+            [inferenceT (inferenceA.record recordT)
+             [inferredT membersA] (inferenceA.general analyse inferenceT membersC)]
+            (wrap (analysis.product membersA)))
+
+          _
+          (..product analyse membersC))))))
diff --git a/stdlib/source/lux/lang/module.lux b/stdlib/source/lux/lang/module.lux
new file mode 100644
index 000000000..d5efb1d7e
--- /dev/null
+++ b/stdlib/source/lux/lang/module.lux
@@ -0,0 +1,239 @@
+(.module:
+  lux
+  (lux (control [monad #+ do]
+                ["ex" exception #+ exception:]
+                pipe)
+       (data [text "text/" Eq<Text>]
+             text/format
+             ["e" error]
+             (coll [list "list/" Fold<List> Functor<List>]
+                   (dictionary [plist])))
+       [macro])
+  [//])
+
+(type: #export Tag Text)
+
+(exception: #export (unknown-module {module Text})
+  module)
+
+(exception: #export (cannot-declare-tag-twice {module Text} {tag Text})
+  (format "Module: " module "\n"
+          "   Tag: " tag "\n"))
+
+(do-template [<name>]
+  [(exception: #export (<name> {tags (List Text)} {owner Type})
+     (format "Tags: " (text.join-with " " tags) "\n"
+             "Type: " (%type owner) "\n"))]
+
+  [cannot-declare-tags-for-unnamed-type]
+  [cannot-declare-tags-for-foreign-type]
+  )
+
+(exception: #export (cannot-define-more-than-once {name Ident})
+  (%ident name))
+
+(exception: #export (can-only-change-state-of-active-module {module Text} {state Module-State})
+  (format "       Module: " module "\n"
+          "Desired state: " (case state
+                              #.Active   "Active"
+                              #.Compiled "Compiled"
+                              #.Cached   "Cached") "\n"))
+
+(exception: #export (cannot-set-module-annotations-more-than-once {module Text} {old Code} {new Code})
+  (format "         Module: " module "\n"
+          "Old annotations: " (%code old) "\n"
+          "New annotations: " (%code new) "\n"))
+
+(def: (new hash)
+  (-> Nat Module)
+  {#.module-hash        hash
+   #.module-aliases     (list)
+   #.definitions        (list)
+   #.imports            (list)
+   #.tags               (list)
+   #.types              (list)
+   #.module-annotations #.None
+   #.module-state       #.Active})
+
+(def: #export (set-annotations annotations)
+  (-> Code (Meta Top))
+  (do macro.Monad<Meta>
+    [self-name macro.current-module-name
+     self macro.current-module]
+    (case (get@ #.module-annotations self)
+      #.None
+      (function (_ compiler)
+        (#e.Success [(update@ #.modules
+                              (plist.put self-name (set@ #.module-annotations (#.Some annotations) self))
+                              compiler)
+                     []]))
+      
+      (#.Some old)
+      (//.throw cannot-set-module-annotations-more-than-once [self-name old annotations]))))
+
+(def: #export (import module)
+  (-> Text (Meta Top))
+  (do macro.Monad<Meta>
+    [self-name macro.current-module-name]
+    (function (_ compiler)
+      (#e.Success [(update@ #.modules
+                            (plist.update self-name (update@ #.imports (|>> (#.Cons module))))
+                            compiler)
+                   []]))))
+
+(def: #export (alias alias module)
+  (-> Text Text (Meta Top))
+  (do macro.Monad<Meta>
+    [self-name macro.current-module-name]
+    (function (_ compiler)
+      (#e.Success [(update@ #.modules
+                            (plist.update self-name (update@ #.module-aliases (: (-> (List [Text Text]) (List [Text Text]))
+                                                                                 (|>> (#.Cons [alias module])))))
+                            compiler)
+                   []]))))
+
+(def: #export (exists? module)
+  (-> Text (Meta Bool))
+  (function (_ compiler)
+    (|> compiler
+        (get@ #.modules)
+        (plist.get module)
+        (case> (#.Some _) true #.None false)
+        [compiler] #e.Success)))
+
+(def: #export (define name definition)
+  (-> Text Definition (Meta []))
+  (do macro.Monad<Meta>
+    [self-name macro.current-module-name
+     self macro.current-module]
+    (function (_ compiler)
+      (case (plist.get name (get@ #.definitions self))
+        #.None
+        (#e.Success [(update@ #.modules
+                              (plist.put self-name
+                                         (update@ #.definitions
+                                                  (: (-> (List [Text Definition]) (List [Text Definition]))
+                                                     (|>> (#.Cons [name definition])))
+                                                  self))
+                              compiler)
+                     []])
+
+        (#.Some already-existing)
+        ((//.throw cannot-define-more-than-once [self-name name]) compiler)))))
+
+(def: #export (create hash name)
+  (-> Nat Text (Meta []))
+  (function (_ compiler)
+    (let [module (new hash)]
+      (#e.Success [(update@ #.modules
+                            (plist.put name module)
+                            compiler)
+                   []]))))
+
+(def: #export (with-module hash name action)
+  (All [a] (-> Nat Text (Meta a) (Meta [Module a])))
+  (do macro.Monad<Meta>
+    [_ (create hash name)
+     output (//.with-current-module name
+              action)
+     module (macro.find-module name)]
+    (wrap [module output])))
+
+(do-template [<setter> <asker> <tag>]
+  [(def: #export (<setter> module-name)
+     (-> Text (Meta Top))
+     (function (_ compiler)
+       (case (|> compiler (get@ #.modules) (plist.get module-name))
+         (#.Some module)
+         (let [active? (case (get@ #.module-state module)
+                         #.Active true
+                         _     false)]
+           (if active?
+             (#e.Success [(update@ #.modules
+                                   (plist.put module-name (set@ #.module-state <tag> module))
+                                   compiler)
+                          []])
+             ((//.throw can-only-change-state-of-active-module [module-name <tag>])
+              compiler)))
+
+         #.None
+         ((//.throw unknown-module module-name) compiler))))
+   
+   (def: #export (<asker> module-name)
+     (-> Text (Meta Bool))
+     (function (_ compiler)
+       (case (|> compiler (get@ #.modules) (plist.get module-name))
+         (#.Some module)
+         (#e.Success [compiler
+                      (case (get@ #.module-state module)
+                        <tag> true
+                        _     false)])
+
+         #.None
+         ((//.throw unknown-module module-name) compiler))))]
+
+  [set-active   active?   #.Active]
+  [set-compiled compiled? #.Compiled]
+  [set-cached   cached?   #.Cached]
+  )
+
+(do-template [<name> <tag> <type>]
+  [(def: (<name> module-name)
+     (-> Text (Meta <type>))
+     (function (_ compiler)
+       (case (|> compiler (get@ #.modules) (plist.get module-name))
+         (#.Some module)
+         (#e.Success [compiler (get@ <tag> module)])
+
+         #.None
+         ((//.throw unknown-module module-name) compiler))))]
+
+  [tags  #.tags        (List [Text [Nat (List Ident) Bool Type]])]
+  [types #.types       (List [Text [(List Ident) Bool Type]])]
+  [hash  #.module-hash Nat]
+  )
+
+(def: (ensure-undeclared-tags module-name tags)
+  (-> Text (List Tag) (Meta Top))
+  (do macro.Monad<Meta>
+    [bindings (..tags module-name)
+     _ (monad.map @
+                  (function (_ tag)
+                    (case (plist.get tag bindings)
+                      #.None
+                      (wrap [])
+
+                      (#.Some _)
+                      (//.throw cannot-declare-tag-twice [module-name tag])))
+                  tags)]
+    (wrap [])))
+
+(def: #export (declare-tags tags exported? type)
+  (-> (List Tag) Bool Type (Meta Top))
+  (do macro.Monad<Meta>
+    [self-name macro.current-module-name
+     [type-module type-name] (case type
+                               (#.Named type-ident _)
+                               (wrap type-ident)
+
+                               _
+                               (//.throw cannot-declare-tags-for-unnamed-type [tags type]))
+     _ (ensure-undeclared-tags self-name tags)
+     _ (//.assert cannot-declare-tags-for-foreign-type [tags type]
+                  (text/= self-name type-module))]
+    (function (_ compiler)
+      (case (|> compiler (get@ #.modules) (plist.get self-name))
+        (#.Some module)
+        (let [namespaced-tags (list/map (|>> [self-name]) tags)]
+          (#e.Success [(update@ #.modules
+                                (plist.update self-name
+                                              (|>> (update@ #.tags (function (_ tag-bindings)
+                                                                     (list/fold (function (_ [idx tag] table)
+                                                                                  (plist.put tag [idx namespaced-tags exported? type] table))
+                                                                                tag-bindings
+                                                                                (list.enumerate tags))))
+                                                   (update@ #.types (plist.put type-name [namespaced-tags exported? type]))))
+                                compiler)
+                       []]))
+        #.None
+        ((//.throw unknown-module self-name) compiler)))))
diff --git a/stdlib/test/test/lux/lang/analysis/primitive.lux b/stdlib/test/test/lux/lang/analysis/primitive.lux
index 2e7c2057a..ed9d8bfc6 100644
--- a/stdlib/test/test/lux/lang/analysis/primitive.lux
+++ b/stdlib/test/test/lux/lang/analysis/primitive.lux
@@ -1,24 +1,46 @@
 (.module:
-  lux
+  [lux #- primitive]
   (lux [io]
        (control [monad #+ do]
                 pipe
                 ["ex" exception #+ exception:])
        (data (text format)
              ["e" error])
-       ["r" math/random]
+       ["r" math/random "r/" Monad<Random>]
        [macro]
        (macro [code])
+       [lang]
        (lang [".L" type "type/" Eq<Type>]
              [".L" init]
              [analysis #+ Analysis]
              (analysis [".A" type]
-                       ["/" primitive]))
+                       [".A" expression]))
        test))
 
+(def: analyse (expressionA.analyser (:! lang.Eval [])))
+
+(def: unit
+  (r.Random Code)
+  (r/wrap (' [])))
+
+(def: #export primitive
+  (r.Random [Type Code])
+  (`` ($_ r.either
+          (~~ (do-template [<type> <code-wrapper> <value-gen>]
+                [(r.seq (r/wrap <type>) (r/map <code-wrapper> <value-gen>))]
+
+                [Top  code.tuple (r.list +0 ..unit)]
+                [Bool code.bool  r.bool]
+                [Nat  code.nat   r.nat]
+                [Int  code.int   r.int]
+                [Deg  code.deg   r.deg]
+                [Frac code.frac  r.frac]
+                [Text code.text  (r.unicode +5)]
+                )))))
+
 (exception: (wrong-inference {expected Type} {inferred Type})
-  (format "Expected: " (%type expected) "\n"
-          "Inferred: " (%type inferred) "\n"))
+  (ex.report ["Expected" (%type expected)]
+             ["Inferred" (%type inferred)]))
 
 (def: (infer-primitive expected-type analysis)
   (-> Type (Meta Analysis) (e.Error Analysis))
@@ -34,30 +56,31 @@
              (#e.Error error))))
 
 (context: "Primitives"
-  (<| (times +100)
-      (`` ($_ seq
-              (test "Can analyse unit."
-                    (|> (infer-primitive Top /.unit)
-                        (case> (^ (#e.Success (#analysis.Primitive (#analysis.Unit output))))
-                               (is? [] output)
-
-                               _
-                               false)))
-              (~~ (do-template [<desc> <type> <tag> <random> <analyser>]
-                    [(do @
-                       [sample <random>]
-                       (test (format "Can analyse " <desc> ".")
-                             (|> (infer-primitive <type> (<analyser> sample))
-                                 (case> (#e.Success (#analysis.Primitive (<tag> output)))
-                                        (is? sample output)
-
-                                        _
-                                        false))))]
-
-                    ["bool" Bool #analysis.Bool r.bool /.bool]
-                    ["nat"  Nat  #analysis.Nat  r.nat  /.nat]
-                    ["int"  Int  #analysis.Int  r.int  /.int]
-                    ["deg"  Deg  #analysis.Deg  r.deg  /.deg]
-                    ["frac" Frac #analysis.Frac r.frac /.frac]
-                    ["text" Text #analysis.Text (r.unicode +5) /.text]
-                    ))))))
+  ($_ seq
+      (test "Can analyse unit."
+            (|> (infer-primitive Top (..analyse (' [])))
+                (case> (^ (#e.Success (#analysis.Primitive (#analysis.Unit output))))
+                       (is? [] output)
+
+                       _
+                       false)))
+      (<| (times +100)
+          (`` ($_ seq
+                  (~~ (do-template [<desc> <type> <tag> <random> <constructor>]
+                        [(do @
+                           [sample <random>]
+                           (test (format "Can analyse " <desc> ".")
+                                 (|> (infer-primitive <type> (..analyse (<constructor> sample)))
+                                     (case> (#e.Success (#analysis.Primitive (<tag> output)))
+                                            (is? sample output)
+
+                                            _
+                                            false))))]
+
+                        ["bool" Bool #analysis.Bool r.bool code.bool]
+                        ["nat"  Nat  #analysis.Nat  r.nat  code.nat]
+                        ["int"  Int  #analysis.Int  r.int  code.int]
+                        ["deg"  Deg  #analysis.Deg  r.deg  code.deg]
+                        ["frac" Frac #analysis.Frac r.frac code.frac]
+                        ["text" Text #analysis.Text (r.unicode +5) code.text]
+                        )))))))
diff --git a/stdlib/test/test/lux/lang/analysis/structure.lux b/stdlib/test/test/lux/lang/analysis/structure.lux
new file mode 100644
index 000000000..110717a0a
--- /dev/null
+++ b/stdlib/test/test/lux/lang/analysis/structure.lux
@@ -0,0 +1,292 @@
+(.module:
+  lux
+  (lux [io]
+       (control [monad #+ do]
+                pipe)
+       (data [bool "bool/" Eq<Bool>]
+             ["e" error]
+             [product]
+             [maybe]
+             [text]
+             text/format
+             (coll [list "list/" Functor<List>]
+                   (set ["set" unordered])))
+       ["r" math/random "r/" Monad<Random>]
+       [macro]
+       (macro [code])
+       [lang]
+       (lang [type "type/" Eq<Type>]
+             (type ["tc" check])
+             [".L" module]
+             [".L" init]
+             [".L" analysis #+ Analysis]
+             (analysis [".A" type]
+                       ["/" structure]
+                       [".A" expression]))
+       test)
+  (// ["_." primitive]))
+
+(do-template [<name> <on-success> <on-error>]
+  [(def: <name>
+     (All [a] (-> (Meta a) Bool))
+     (|>> (macro.run (initL.compiler []))
+          (case> (#e.Success _)
+                 <on-success>
+
+                 _
+                 <on-error>)))]
+
+  [check-succeeds true  false]
+  [check-fails    false true]
+  )
+
+(def: analyse (expressionA.analyser (:! lang.Eval [])))
+
+(def: (check-sum' size tag variant)
+  (-> Nat analysisL.Tag analysisL.Variant Bool)
+  (let [variant-tag (if (get@ #analysisL.right? variant)
+                      (inc (get@ #analysisL.lefts variant))
+                      (get@ #analysisL.lefts variant))]
+    (|> size dec (n/= tag)
+        (bool/= (get@ #analysisL.right? variant))
+        (and (n/= tag variant-tag)))))
+
+(def: (check-sum type size tag analysis)
+  (-> Type Nat analysisL.Tag (Meta Analysis) Bool)
+  (|> analysis
+      (typeA.with-type type)
+      (macro.run (initL.compiler []))
+      (case> (^multi (#e.Success sumA)
+                     [(analysisL.variant sumA)
+                      (#.Some variant)])
+             (check-sum' size tag variant)
+
+             _
+             false)))
+
+(def: (tagged module tags type)
+  (All [a] (-> Text (List moduleL.Tag) Type (Meta a) (Meta [Module a])))
+  (|>> (do macro.Monad<Meta>
+         [_ (moduleL.declare-tags tags false type)])
+       (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)
+  (|> analysis
+      (tagged module tags type)
+      (typeA.with-type type)
+      (macro.run (initL.compiler []))
+      (case> (^multi (#e.Success [_ sumA])
+                     [(analysisL.variant sumA)
+                      (#.Some variant)])
+             (check-sum' size tag variant)
+
+             _
+             false)))
+
+(def: (right-size? size)
+  (-> Nat (-> Analysis Bool))
+  (|>> analysisL.tuple list.size (n/= size)))
+
+(def: (check-record-inference module tags type size analysis)
+  (-> Text (List moduleL.Tag) Type Nat (Meta [Type Analysis]) Bool)
+  (|> analysis
+      (tagged module tags type)
+      (macro.run (initL.compiler []))
+      (case> (#e.Success [_ productT productA])
+             (and (type/= type productT)
+                  (right-size? size productA))
+
+             _
+             false)))
+
+(context: "Sums"
+  (<| (times +100)
+      (do @
+        [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+         choice (|> r.nat (:: @ map (n/% size)))
+         primitives (r.list size _primitive.primitive)
+         +choice (|> r.nat (:: @ map (n/% (inc size))))
+         [_ +valueC] _primitive.primitive
+         #let [variantT (type.variant (list/map product.left primitives))
+               [valueT valueC] (maybe.assume (list.nth choice primitives))
+               +size (inc size)
+               +primitives (list.concat (list (list.take choice primitives)
+                                              (list [(#.Bound +1) +valueC])
+                                              (list.drop choice primitives)))
+               [+valueT +valueC] (maybe.assume (list.nth +choice +primitives))
+               +variantT (type.variant (list/map product.left +primitives))]]
+        ($_ seq
+            (test "Can analyse sum."
+                  (check-sum variantT size choice
+                             (/.sum ..analyse choice valueC)))
+            (test "Can analyse sum through bound type-vars."
+                  (|> (do macro.Monad<Meta>
+                        [[_ varT] (typeA.with-env tc.var)
+                         _ (typeA.with-env
+                             (tc.check varT variantT))]
+                        (typeA.with-type varT
+                          (/.sum ..analyse choice valueC)))
+                      (macro.run (initL.compiler []))
+                      (case> (^multi (#e.Success sumA)
+                                     [(analysisL.variant sumA)
+                                      (#.Some variant)])
+                             (check-sum' size choice variant)
+
+                             _
+                             false)))
+            (test "Cannot analyse sum through unbound type-vars."
+                  (|> (do macro.Monad<Meta>
+                        [[_ varT] (typeA.with-env tc.var)]
+                        (typeA.with-type varT
+                          (/.sum ..analyse choice valueC)))
+                      check-fails))
+            (test "Can analyse sum through existential quantification."
+                  (|> (typeA.with-type (type.ex-q +1 +variantT)
+                        (/.sum ..analyse +choice +valueC))
+                      check-succeeds))
+            (test "Can analyse sum through universal quantification."
+                  (let [check-outcome (if (not (n/= choice +choice))
+                                        check-succeeds
+                                        check-fails)]
+                    (|> (typeA.with-type (type.univ-q +1 +variantT)
+                          (/.sum ..analyse +choice +valueC))
+                        check-outcome)))
+            ))))
+
+(context: "Products"
+  (<| (times +100)
+      (do @
+        [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+         primitives (r.list size _primitive.primitive)
+         choice (|> r.nat (:: @ map (n/% size)))
+         [_ +valueC] _primitive.primitive
+         #let [tupleT (type.tuple (list/map product.left primitives))
+               [singletonT singletonC] (|> primitives (list.nth choice) maybe.assume)
+               +primitives (list.concat (list (list.take choice primitives)
+                                              (list [(#.Bound +1) +valueC])
+                                              (list.drop choice primitives)))
+               +tupleT (type.tuple (list/map product.left +primitives))]]
+        ($_ seq
+            (test "Can analyse product."
+                  (|> (typeA.with-type tupleT
+                        (/.product ..analyse (list/map product.right primitives)))
+                      (macro.run (initL.compiler []))
+                      (case> (#e.Success tupleA)
+                             (right-size? size tupleA)
+
+                             _
+                             false)))
+            (test "Can infer product."
+                  (|> (typeA.with-inference
+                        (/.product ..analyse (list/map product.right primitives)))
+                      (macro.run (initL.compiler []))
+                      (case> (#e.Success [_type tupleA])
+                             (and (type/= tupleT _type)
+                                  (right-size? size tupleA))
+
+                             _
+                             false)))
+            (test "Can analyse pseudo-product (singleton tuple)"
+                  (|> (typeA.with-type singletonT
+                        (..analyse (` [(~ singletonC)])))
+                      check-succeeds))
+            (test "Can analyse product through bound type-vars."
+                  (|> (do macro.Monad<Meta>
+                        [[_ varT] (typeA.with-env tc.var)
+                         _ (typeA.with-env
+                             (tc.check varT (type.tuple (list/map product.left primitives))))]
+                        (typeA.with-type varT
+                          (/.product ..analyse (list/map product.right primitives))))
+                      (macro.run (initL.compiler []))
+                      (case> (#e.Success tupleA)
+                             (right-size? size tupleA)
+
+                             _
+                             false)))
+            (test "Can analyse product through existential quantification."
+                  (|> (typeA.with-type (type.ex-q +1 +tupleT)
+                        (/.product ..analyse (list/map product.right +primitives)))
+                      check-succeeds))
+            (test "Cannot analyse product through universal quantification."
+                  (|> (typeA.with-type (type.univ-q +1 +tupleT)
+                        (/.product ..analyse (list/map product.right +primitives)))
+                      check-fails))
+            ))))
+
+(context: "Tagged Sums"
+  (<| (times +100)
+      (do @
+        [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+         tags (|> (r.set text.Hash<Text> size (r.unicode +5)) (:: @ map set.to-list))
+         choice (|> r.nat (:: @ map (n/% size)))
+         other-choice (|> r.nat (:: @ map (n/% size)) (r.filter (|>> (n/= choice) not)))
+         primitives (r.list size _primitive.primitive)
+         module-name (r.unicode +5)
+         type-name (r.unicode +5)
+         #let [varT (#.Bound +1)
+               primitivesT (list/map product.left primitives)
+               [choiceT choiceC] (maybe.assume (list.nth choice primitives))
+               [other-choiceT other-choiceC] (maybe.assume (list.nth other-choice primitives))
+               variantT (type.variant primitivesT)
+               namedT (#.Named [module-name type-name] variantT)
+               named-polyT (|> (type.variant (list.concat (list (list.take choice primitivesT)
+                                                                (list varT)
+                                                                (list.drop (inc choice) primitivesT))))
+                               (type.univ-q +1)
+                               (#.Named [module-name type-name]))
+               choice-tag (maybe.assume (list.nth choice tags))
+               other-choice-tag (maybe.assume (list.nth other-choice tags))]]
+        ($_ seq
+            (test "Can infer tagged sum."
+                  (|> (/.tagged-sum ..analyse [module-name choice-tag] choiceC)
+                      (check-variant module-name tags namedT choice size)))
+            (test "Tagged sums specialize when type-vars get bound."
+                  (|> (/.tagged-sum ..analyse [module-name choice-tag] choiceC)
+                      (check-variant module-name tags named-polyT choice size)))
+            (test "Tagged sum inference retains universal quantification when type-vars are not bound."
+                  (|> (/.tagged-sum ..analyse [module-name other-choice-tag] other-choiceC)
+                      (check-variant module-name tags named-polyT other-choice size)))
+            (test "Can specialize generic tagged sums."
+                  (|> (typeA.with-type variantT
+                        (/.tagged-sum ..analyse [module-name other-choice-tag] other-choiceC))
+                      (check-variant module-name tags named-polyT other-choice size)))
+            ))))
+
+(context: "Records"
+  (<| (times +100)
+      (do @
+        [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+         tags (|> (r.set text.Hash<Text> size (r.unicode +5)) (:: @ map set.to-list))
+         primitives (r.list size _primitive.primitive)
+         module-name (r.unicode +5)
+         type-name (r.unicode +5)
+         choice (|> r.nat (:: @ map (n/% size)))
+         #let [varT (#.Bound +1)
+               tagsC (list/map (|>> [module-name] code.tag) tags)
+               primitivesT (list/map product.left primitives)
+               primitivesC (list/map product.right primitives)
+               tupleT (type.tuple primitivesT)
+               namedT (#.Named [module-name type-name] tupleT)
+               recordC (list.zip2 tagsC primitivesC)
+               named-polyT (|> (type.tuple (list.concat (list (list.take choice primitivesT)
+                                                              (list varT)
+                                                              (list.drop (inc choice) primitivesT))))
+                               (type.univ-q +1)
+                               (#.Named [module-name type-name]))]]
+        ($_ seq
+            (test "Can infer record."
+                  (|> (typeA.with-inference
+                        (/.record ..analyse recordC))
+                      (check-record-inference module-name tags namedT size)))
+            (test "Records specialize when type-vars get bound."
+                  (|> (typeA.with-inference
+                        (/.record ..analyse recordC))
+                      (check-record-inference module-name tags named-polyT size)))
+            (test "Can specialize generic records."
+                  (|> (do macro.Monad<Meta>
+                        [recordA (typeA.with-type tupleT
+                                   (/.record ..analyse recordC))]
+                        (wrap [tupleT recordA]))
+                      (check-record-inference module-name tags named-polyT size)))
+            ))))