- Documented the analysis phase.

- Some refactoring.
- Removed singleton variants.

10 files changed, 644 insertions, 509 deletions

diff --git a/new-luxc/source/luxc/analyser.lux b/new-luxc/source/luxc/analyser.lux
index 44fa96081..e79b74f01 100644
--- a/new-luxc/source/luxc/analyser.lux
+++ b/new-luxc/source/luxc/analyser.lux
@@ -41,6 +41,8 @@
   (: (-> Code (Lux la;Analysis))
      (function analyse [ast]
        (let [[cursor ast'] ast]
+         ## The cursor must be set in the compiler for the sake
+         ## of having useful error messages.
          (&;with-cursor cursor
            (case ast'
              (^template [<tag> <analyser>]
@@ -57,6 +59,7 @@
              (^ (#;Tuple (list)))
              &&primitive;analyse-unit
 
+             ## Singleton tuples are equivalent to the element they contain.
              (^ (#;Tuple (list singleton)))
              (analyse singleton)
 
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux
index f3eec6b6b..306618caf 100644
--- a/new-luxc/source/luxc/analyser/case.lux
+++ b/new-luxc/source/luxc/analyser/case.lux
@@ -15,25 +15,25 @@
        (macro [code])
        [type]
        (type ["TC" check]))
-  (luxc ["&" base]
-        (lang ["la" analysis])
-        ["&;" env]
-        (analyser ["&;" common]
-                  ["&;" structure])))
-
-(type: #rec Coverage
-  #PartialC
-  (#BoolC Bool)
-  (#VariantC Nat (D;Dict Nat Coverage))
-  (#SeqC Coverage Coverage)
-  (#AltC Coverage Coverage)
-  #TotalC)
+  (../.. ["&" base]
+         (lang ["la" analysis])
+         ["&;" env])
+  (.. ["&;" common]
+      ["&;" structure])
+  (. ["&&;" coverage]))
 
 (def: (pattern-error type pattern)
   (-> Type Code Text)
   (format "Cannot match this type: " (%type type) "\n"
           "     With this pattern: " (%code pattern)))
 
+## 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 type)
   (-> Type (Lux Type))
   (case type
@@ -60,6 +60,22 @@
     _
     (:: Monad<Lux> wrap type)))
 
+## 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 (Lux a) (Lux [la;Pattern a])))
   (case pattern
@@ -143,10 +159,10 @@
           (&;fail (pattern-error inputT pattern))
           )))
 
-    [cursor (#;Record pairs)]
+    [cursor (#;Record record)]
     (do Monad<Lux>
-      [pairs (&structure;normalize-record pairs)
-       [members recordT] (&structure;order-record pairs)
+      [record (&structure;normalize record)
+       [members recordT] (&structure;order record)
        _ (&;within-type-env
           (TC;check inputT recordT))]
       (analyse-pattern (#;Some (list;size members)) inputT [cursor (#;Tuple members)] next))
@@ -200,240 +216,6 @@
     (&;fail (format "Unrecognized pattern syntax: " (%code pattern)))
     ))
 
-(def: (analyse-branch analyse inputT pattern body)
-  (-> &;Analyser Type Code Code (Lux [la;Pattern la;Analysis]))
-  (analyse-pattern #;None inputT pattern (analyse body)))
-
-(do-template [<name> <tag>]
-  [(def: (<name> coverage)
-     (-> Coverage Bool)
-     (case coverage
-       (<tag> _)
-       true
-
-       _
-       false))]
-
-  [total? #TotalC]
-  [alt?   #AltC]
-  )
-
-(def: (determine-coverage pattern)
-  (-> la;Pattern Coverage)
-  (case pattern
-    (^or (#la;BindP _) (^ (#la;TupleP (list))))
-    #TotalC
-
-    (^ (#la;TupleP (list singleton)))
-    (determine-coverage singleton)
-    
-    (#la;BoolP value)
-    (#BoolC value)
-    
-    (^or (#la;NatP _)  (#la;IntP _)  (#la;DegP _)
-         (#la;RealP _) (#la;CharP _) (#la;TextP _))
-    #PartialC
-    
-    (#la;TupleP subs)
-    (loop [subs subs]
-      (case subs
-        #;Nil
-        #TotalC
-
-        (#;Cons sub subs')
-        (let [post (recur subs')]
-          (if (total? post)
-            (determine-coverage sub)
-            (#SeqC (determine-coverage sub)
-                   post)))))
-    
-    (#la;VariantP tag-id num-tags sub)
-    (#VariantC num-tags
-               (|> (D;new number;Hash<Nat>)
-                   (D;put tag-id (determine-coverage sub))))))
-
-(def: (xor left right)
-  (-> Bool Bool Bool)
-  (or (and left (not right))
-      (and (not left) right)))
-
-(def: redundant-pattern
-  (R;Result Coverage)
-  (R;fail "Redundant pattern."))
-
-(def: (flatten-alt coverage)
-  (-> Coverage (List Coverage))
-  (case coverage
-    (#AltC left right)
-    (list& left (flatten-alt right))
-
-    _
-    (list coverage)))
-
-(struct: _ (Eq Coverage)
-  (def: (= reference sample)
-    (case [reference sample]
-      [#TotalC #TotalC]
-      true
-
-      [(#BoolC sideR) (#BoolC sideS)]
-      (B/= sideR sideS)
-
-      [(#VariantC allR casesR) (#VariantC allS casesS)]
-      (and (n.= allR allS)
-           (:: (D;Eq<Dict> =) = casesR casesS))
-
-      [(#SeqC leftR rightR) (#SeqC leftS rightS)]
-      (and (= leftR leftS)
-           (= rightR rightS))
-
-      [(#AltC _) (#AltC _)]
-      (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/")
-
-(def: (merge-coverages addition so-far)
-  (-> Coverage Coverage (R;Result Coverage))
-  (case [addition so-far]
-    ## The addition cannot possibly improve the coverage.
-    [_ #TotalC]
-    redundant-pattern
-
-    ## The addition completes the coverage.
-    [#TotalC _]
-    (R/wrap #TotalC)
-
-    [#PartialC #PartialC]
-    (R/wrap #PartialC)
-
-    (^multi [(#BoolC sideA) (#BoolC sideSF)]
-            (xor sideA sideSF))
-    (R/wrap #TotalC)
-
-    [(#VariantC allA casesA) (#VariantC allSF casesSF)]
-    (cond (not (n.= allSF allA))
-          (R;fail "Variants do not match.")
-
-          (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA)
-          redundant-pattern
-
-          ## else
-          (do R;Monad<Result>
-            [casesM (foldM @
-                           (function [[tagA coverageA] casesSF']
-                             (case (D;get tagA casesSF')
-                               (#;Some coverageSF)
-                               (do @
-                                 [coverageM (merge-coverages coverageA coverageSF)]
-                                 (wrap (D;put tagA coverageM casesSF')))
-
-                               #;None
-                               (wrap (D;put tagA coverageA casesSF'))))
-                           casesSF (D;entries casesA))]
-            (wrap (if (let [case-coverages (D;values casesM)]
-                        (and (n.= allSF (list;size case-coverages))
-                             (list;every? total? case-coverages)))
-                    #TotalC
-                    (#VariantC allSF casesM)))))
-
-    [(#SeqC leftA rightA) (#SeqC 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]
-      (R/wrap (#AltC so-far addition))
-
-      ## Same prefix
-      [true false]
-      (do R;Monad<Result>
-        [rightM (merge-coverages rightA rightSF)]
-        (if (total? rightM)
-          (wrap leftSF)
-          (wrap (#SeqC leftSF rightM))))
-
-      ## Same suffix
-      [false true]
-      (do R;Monad<Result>
-        [leftM (merge-coverages leftA leftSF)]
-        (wrap (#SeqC leftM rightA))))
-    
-    ## The left part will always match, so the addition is redundant.
-    (^multi [(#SeqC left right) single]
-            (C/= left single))
-    redundant-pattern
-
-    ## The right part is not necessary, since it can always match the left.
-    (^multi [single (#SeqC left right)]
-            (C/= left single))
-    (R/wrap single)
-
-    [_ (#AltC leftS rightS)]
-    (do R;Monad<Result>
-      [#let [fuse-once (: (-> Coverage (List Coverage)
-                              (R;Result [(Maybe Coverage)
-                                         (List Coverage)]))
-                          (function [coverage possibilities]
-                            (loop [alts possibilities]
-                              (case alts
-                                #;Nil
-                                (wrap [#;None (list coverage)])
-                                
-                                (#;Cons alt alts')
-                                (case (merge-coverages coverage alt)
-                                  (#R;Success altM)
-                                  (case altM
-                                    (#AltC _)
-                                    (do @
-                                      [[success alts+] (recur alts')]
-                                      (wrap [success (#;Cons alt alts+)]))
-
-                                    _
-                                    (wrap [(#;Some altM) alts']))
-                                  
-                                  (#R;Error error)
-                                  (R;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)
-            #;Nil
-            (R;fail "{ This is not supposed to happen... }")
-            
-            (#;Cons last prevs)
-            (wrap (L/fold (function [left right] (#AltC left right))
-                          last
-                          prevs))))))
-
-    _
-    (if (C/= so-far addition)
-      ## The addition cannot possibly improve the coverage.
-      redundant-pattern
-      ## There are now 2 alternative paths.
-      (R/wrap (#AltC so-far addition)))))
-
-(def: get-coverage
-  (-> [la;Pattern la;Analysis] Coverage)
-  (|>. product;left determine-coverage))
-
 (def: #export (analyse-case analyse input branches)
   (-> &;Analyser Code (List [Code Code]) (Lux la;Analysis))
   (case branches
@@ -444,17 +226,17 @@
     (do Monad<Lux>
       [[inputT inputA] (&common;with-unknown-type
                          (analyse input))
-       outputH (analyse-branch analyse inputT patternH bodyH)
+       outputH (analyse-pattern #;None inputT patternH (analyse bodyH))
        outputT (mapM @
                      (function [[patternT bodyT]]
-                       (analyse-branch analyse inputT patternT bodyT))
+                       (analyse-pattern #;None inputT patternT (analyse bodyT)))
                      branchesT)
        _ (case (foldM R;Monad<Result>
-                      merge-coverages
-                      (get-coverage outputH)
-                      (L/map get-coverage outputT))
+                      &&coverage;merge
+                      (|> outputH product;left &&coverage;determine)
+                      (L/map (|>. product;left &&coverage;determine) outputT))
            (#R;Success coverage)
-           (if (total? coverage)
+           (if (&&coverage;total? coverage)
              (wrap [])
              (&;fail "Pattern-matching is not total."))
 
diff --git a/new-luxc/source/luxc/analyser/case/coverage.lux b/new-luxc/source/luxc/analyser/case/coverage.lux
new file mode 100644
index 000000000..754e555b2
--- /dev/null
+++ b/new-luxc/source/luxc/analyser/case/coverage.lux
@@ -0,0 +1,287 @@
+(;module:
+  lux
+  (lux (control monad
+                eq)
+       (data [bool "B/" Eq<Bool>]
+             [number]
+             ["R" result "R/" Monad<Result>]
+             (coll [list "L/" Fold<List>]
+                   ["D" dict])))
+  (luxc (lang ["la" analysis])))
+
+## 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 "total" 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 Nat (D;Dict Nat Coverage))
+  (#Seq Coverage Coverage)
+  (#Alt Coverage Coverage)
+  #Total)
+
+(def: #export (total? coverage)
+  (-> Coverage Bool)
+  (case coverage
+    (#Total _)
+    true
+
+    _
+    false))
+
+(def: #export (determine pattern)
+  (-> la;Pattern Coverage)
+  (case pattern
+    ## Binding amounts to total coverage because any value can be
+    ## matched that way.
+    ## Unit [] amounts to total coverage because there is only one
+    ## possible value, so matching against it covers all cases.
+    (^or (#la;BindP _) (^ (#la;TupleP (list))))
+    #Total
+
+    (^ (#la;TupleP (list singleton)))
+    (determine singleton)
+
+    ## Primitive patterns always have partial coverage because there
+    ## are too many possibilities as far as values go.
+    (^or (#la;NatP _)  (#la;IntP _)  (#la;DegP _)
+         (#la;RealP _) (#la;CharP _) (#la;TextP _))
+    #Partial
+
+    ## Bools are the exception, since there is only "true" and
+    ## "false", which means it is possible for boolean
+    ## pattern-matching to become total if complementary parts meet.
+    (#la;BoolP value)
+    (#Bool value)
+
+    ## Tuple patterns can be total if there is totality for all of
+    ## their sub-patterns.
+    (#la;TupleP subs)
+    (loop [subs subs]
+      (case subs
+        #;Nil
+        #Total
+
+        (#;Cons sub subs')
+        (let [post (recur subs')]
+          (if (total? post)
+            (determine sub)
+            (#Seq (determine sub)
+                  post)))))
+
+    ## Variant patterns can be shown to be total if all the possible
+    ## cases are handled totally.
+    (#la;VariantP tag-id num-tags sub)
+    (#Variant num-tags
+              (|> (D;new number;Hash<Nat>)
+                  (D;put tag-id (determine sub))))))
+
+(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
+## total, 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
+  (R;Result Coverage)
+  (R;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]
+      [#Total #Total]
+      true
+
+      [(#Bool sideR) (#Bool sideS)]
+      (B/= sideR sideS)
+
+      [(#Variant allR casesR) (#Variant allS casesS)]
+      (and (n.= allR allS)
+           (:: (D;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 total and whether it contains
+## redundant patterns.
+(def: #export (merge addition so-far)
+  (-> Coverage Coverage (R;Result Coverage))
+  (case [addition so-far]
+    ## The addition cannot possibly improve the coverage.
+    [_ #Total]
+    redundant-pattern
+
+    ## The addition completes the coverage.
+    [#Total _]
+    (R/wrap #Total)
+
+    [#Partial #Partial]
+    (R/wrap #Partial)
+
+    ## 2 boolean coverages are total if they compliment one another.
+    (^multi [(#Bool sideA) (#Bool sideSF)]
+            (xor sideA sideSF))
+    (R/wrap #Total)
+
+    [(#Variant allA casesA) (#Variant allSF casesSF)]
+    (cond (not (n.= allSF allA))
+          (R;fail "Variants do not match.")
+
+          (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA)
+          redundant-pattern
+
+          ## else
+          (do R;Monad<Result>
+            [casesM (foldM @
+                           (function [[tagA coverageA] casesSF']
+                             (case (D;get tagA casesSF')
+                               (#;Some coverageSF)
+                               (do @
+                                 [coverageM (merge coverageA coverageSF)]
+                                 (wrap (D;put tagA coverageM casesSF')))
+
+                               #;None
+                               (wrap (D;put tagA coverageA casesSF'))))
+                           casesSF (D;entries casesA))]
+            (wrap (if (let [case-coverages (D;values casesM)]
+                        (and (n.= allSF (list;size case-coverages))
+                             (list;every? total? case-coverages)))
+                    #Total
+                    (#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]
+      (R/wrap (#Alt so-far addition))
+
+      ## Same prefix
+      [true false]
+      (do R;Monad<Result>
+        [rightM (merge rightA rightSF)]
+        (if (total? rightM)
+          ## If all that follows is total, then it can be safely dropped
+          ## (since only the "left" part would influence whether the
+          ## merged coverage is total or not).
+          (wrap leftSF)
+          (wrap (#Seq leftSF rightM))))
+
+      ## Same suffix
+      [false true]
+      (do R;Monad<Result>
+        [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))
+    (R/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 R;Monad<Result>
+      [#let [fuse-once (: (-> Coverage (List Coverage)
+                              (R;Result [(Maybe Coverage)
+                                         (List Coverage)]))
+                          (function [coverage possibilities]
+                            (loop [alts possibilities]
+                              (case alts
+                                #;Nil
+                                (wrap [#;None (list coverage)])
+                                
+                                (#;Cons alt alts')
+                                (case (merge coverage alt)
+                                  (#R;Success altM)
+                                  (case altM
+                                    (#Alt _)
+                                    (do @
+                                      [[success alts+] (recur alts')]
+                                      (wrap [success (#;Cons alt alts+)]))
+
+                                    _
+                                    (wrap [(#;Some altM) alts']))
+                                  
+                                  (#R;Error error)
+                                  (R;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)
+            #;Nil
+            (R;fail "{ This is not supposed to happen... }")
+            
+            (#;Cons last prevs)
+            (wrap (L/fold (function [left right] (#Alt left right))
+                          last
+                          prevs))))))
+
+    _
+    (if (C/= so-far addition)
+      ## The addition cannot possibly improve the coverage.
+      redundant-pattern
+      ## There are now 2 alternative paths.
+      (R/wrap (#Alt so-far addition)))))
diff --git a/new-luxc/source/luxc/analyser/common.lux b/new-luxc/source/luxc/analyser/common.lux
index 7a9e5dbf8..c1246d81c 100644
--- a/new-luxc/source/luxc/analyser/common.lux
+++ b/new-luxc/source/luxc/analyser/common.lux
@@ -30,3 +30,10 @@
      output (body [id var])
      _ (&;within-type-env (TC;delete-var id))]
     (wrap output)))
+
+(def: #export (variant-out-of-bounds-error type size tag)
+  (All [a] (-> Type Nat Nat (Lux a)))
+  (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n"
+                  " Tag: " (%i (nat-to-int tag)) "\n"
+                  "Size: " (%i (nat-to-int size)) "\n"
+                  "Type: " (%type type))))
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 394e65c4d..1aad8954e 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -62,7 +62,7 @@
                     (function [[output-id outputT]]
                       (do @
                         [#let [funT (#;Function inputT outputT)]
-                         =function (recur funT)
+                         funA (recur funT)
                          funT' (&;within-type-env
                                 (TC;clean output-id funT))
                          concrete-input? (&;within-type-env
@@ -70,15 +70,17 @@
                          funT'' (if concrete-input?
                                   (&;within-type-env
                                    (TC;clean input-id funT'))
-                                  (wrap (#;UnivQ (list) (&inference;bind-var input-id +1 funT'))))
+                                  (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
                          _ (&;within-type-env
                             (TC;check expected funT''))]
-                        (wrap =function))
+                        (wrap funA))
                       ))))))
 
           (#;Function inputT outputT)
           (<| (:: @ map (|>. #la;Function))
               &;with-scope
+              ## Functions have access not only to their argument, but
+              ## also to themselves, through a local variable.
               (&env;with-local [func-name functionT])
               (&env;with-local [arg-name inputT])
               (&;with-expected-type outputT)
diff --git a/new-luxc/source/luxc/analyser/inference.lux b/new-luxc/source/luxc/analyser/inference.lux
index 824071ab3..11ec58eb3 100644
--- a/new-luxc/source/luxc/analyser/inference.lux
+++ b/new-luxc/source/luxc/analyser/inference.lux
@@ -10,16 +10,24 @@
         (lang ["la" analysis #+ Analysis])
         (analyser ["&;" common])))
 
-(def: #export (bind-var var-id bound-idx type)
+## When doing inference, type-variables often need to be created in
+## order to figure out which types are present in the expression being
+## inferred.
+## If a type-variable never gets bound/resolved to a type, then that
+## means the expression can be generalized through universal
+## quantification.
+## When that happens, the type-variable must be replaced by an
+## argument to the universally-quantified type.
+(def: #export (replace-var var-id bound-idx type)
   (-> Nat Nat Type Type)
   (case type
     (#;Host name params)
-    (#;Host name (L/map (bind-var var-id bound-idx) params))
+    (#;Host name (L/map (replace-var var-id bound-idx) params))
 
     (^template [<tag>]
       (<tag> left right)
-      (<tag> (bind-var var-id bound-idx left)
-             (bind-var var-id bound-idx right)))
+      (<tag> (replace-var var-id bound-idx left)
+             (replace-var var-id bound-idx right)))
     ([#;Sum]
      [#;Product]
      [#;Function]
@@ -32,18 +40,25 @@
 
     (^template [<tag>]
       (<tag> env quantified)
-      (<tag> (L/map (bind-var var-id bound-idx) env)
-             (bind-var var-id (n.+ +2 bound-idx) quantified)))
+      (<tag> (L/map (replace-var var-id bound-idx) env)
+             (replace-var var-id (n.+ +2 bound-idx) quantified)))
     ([#;UnivQ]
      [#;ExQ])
     
     (#;Named name unnamedT)
     (#;Named name
-             (bind-var var-id bound-idx unnamedT))
+             (replace-var var-id bound-idx unnamedT))
 
     _
     type))
 
+## 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 trated
+## as a function type, this method of inference should work.
 (def: #export (apply-function analyse funcT args)
   (-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
   (case args
@@ -63,10 +78,12 @@
             (do @
               [? (&;within-type-env
                   (TC;bound? var-id))
+               ## Quantify over the type if genericity/parametricity
+               ## is discovered.
                outputT' (if ?
                           (&;within-type-env
                            (TC;clean var-id outputT))
-                          (wrap (#;UnivQ (list) (bind-var var-id +1 outputT))))]
+                          (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))]
               (wrap [outputT' argsA])))))
 
       (#;ExQ _)
@@ -75,6 +92,13 @@
                       TC;existential)]
         (apply-function analyse (assume (type;apply-type funcT exT)) args))
 
+      ## 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 Monad<Lux>
         [[outputT' args'A] (apply-function analyse outputT args')
@@ -88,3 +112,72 @@
       _
       (&;fail (format "Cannot apply a non-function: " (%type funcT))))
     ))
+
+## Turns a record type into the kind of function type suitable for inference.
+(def: #export (record-inference-type type)
+  (-> Type (Lux Type))
+  (case type
+    (#;Named name unnamedT)
+    (do Monad<Lux>
+      [unnamedT+ (record-inference-type unnamedT)]
+      (wrap (#;Named name unnamedT+)))
+
+    (^template [<tag>]
+      (<tag> env bodyT)
+      (do Monad<Lux>
+        [bodyT+ (record-inference-type bodyT)]
+        (wrap (<tag> env bodyT+))))
+    ([#;UnivQ]
+     [#;ExQ])
+
+    (#;Product _)
+    (:: Monad<Lux> wrap (type;function (type;flatten-tuple type) type))
+
+    _
+    (&;fail (format "Not a record type: " (%type type)))))
+
+## Turns a variant type into the kind of function type suitable for inference.
+(def: #export (variant-inference-type tag expected-size type)
+  (-> Nat Nat Type (Lux Type))
+  (case type
+    (#;Named name unnamedT)
+    (do Monad<Lux>
+      [unnamedT+ (variant-inference-type tag expected-size unnamedT)]
+      (wrap (#;Named name unnamedT+)))
+
+    (^template [<tag>]
+      (<tag> env bodyT)
+      (do Monad<Lux>
+        [bodyT+ (variant-inference-type tag expected-size bodyT)]
+        (wrap (<tag> env bodyT+))))
+    ([#;UnivQ]
+     [#;ExQ])
+
+    (#;Sum _)
+    (let [cases (type;flatten-variant type)
+          actual-size (list;size cases)
+          boundary (n.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)
+              (:: Monad<Lux> wrap (type;function (list caseT) type))
+
+              #;None
+              (&common;variant-out-of-bounds-error type expected-size tag))
+            
+            (n.< expected-size actual-size)
+            (&;fail (format "Variant type is smaller than expected." "\n"
+                            "Expected: " (%i (nat-to-int expected-size)) "\n"
+                            "  Actual: " (%i (nat-to-int actual-size))))
+
+            (n.= boundary tag)
+            (let [caseT (type;variant (list;drop boundary cases))]
+              (:: Monad<Lux> wrap (type;function (list caseT) type)))
+            
+            ## else
+            (&common;variant-out-of-bounds-error type expected-size tag)))
+
+    _
+    (&;fail (format "Not a variant type: " (%type type)))))
diff --git a/new-luxc/source/luxc/analyser/procedure/common.lux b/new-luxc/source/luxc/analyser/procedure/common.lux
index 8a03f9cad..303cdc61c 100644
--- a/new-luxc/source/luxc/analyser/procedure/common.lux
+++ b/new-luxc/source/luxc/analyser/procedure/common.lux
@@ -71,6 +71,7 @@
   (simple-proc proc (list fromT) toT))
 
 ## [Analysers]
+## "lux is" represents reference/pointer equality.
 (def: (analyse-lux-is proc)
   (-> Text Proc-Analyser)
   (function [analyse args]
@@ -79,6 +80,8 @@
         ((binary-operation varT varT Bool proc)
          analyse args)))))
 
+## "lux try" provides a simple way to interact with the host platform's
+## error-handling facilities.
 (def: (analyse-lux-try proc)
   (-> Text Proc-Analyser)
   (function [analyse args]
diff --git a/new-luxc/source/luxc/analyser/structure.lux b/new-luxc/source/luxc/analyser/structure.lux
index 9447ea059..f93534463 100644
--- a/new-luxc/source/luxc/analyser/structure.lux
+++ b/new-luxc/source/luxc/analyser/structure.lux
@@ -24,7 +24,109 @@
         (analyser ["&;" common]
                   ["&;" inference])))
 
-## [Analysers]
+## 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.
+
+(do-template [<name> <side>]
+  [(def: (<name> inner)
+     (-> la;Analysis la;Analysis)
+     (#la;Sum (<side> inner)))]
+
+  [sum-left  #;Left]
+  [sum-right #;Right])
+
+(def: (variant tag size temp value)
+  (-> Nat Nat Nat la;Analysis la;Analysis)
+  (if (n.= (n.dec size) tag)
+    (if (n.= +1 tag)
+      (sum-right value)
+      (L/fold (function;const sum-left)
+              (sum-right value)
+              (list;n.range +0 (n.- +2 tag))))
+    (L/fold (function;const sum-left)
+            (case value
+              (#la;Sum _)
+              (#la;Case value (list [(#la;BindP temp)
+                                     (#la;Relative (#;Local temp))]))
+
+              _
+              value)
+            (list;n.range +0 tag))))
+
+(def: #export (analyse-sum analyse tag valueC)
+  (-> &;Analyser Nat Code (Lux la;Analysis))
+  (do Monad<Lux>
+    [expected macro;expected-type]
+    (&;with-stacked-errors
+      (function [_] (format "Invalid type for variant: " (%type expected)))
+      (case expected
+        (#;Sum _)
+        (let [flat (type;flatten-variant expected)
+              type-size (list;size flat)]
+          (case (list;nth tag flat)
+            (#;Some variant-type)
+            (do @
+              [valueA (&;with-expected-type variant-type
+                        (analyse valueC))
+               temp &env;next-local]
+              (wrap (variant tag type-size temp valueA)))
+
+            #;None
+            (&common;variant-out-of-bounds-error expected type-size tag)))
+
+        (#;Named name unnamedT)
+        (&;with-expected-type unnamedT
+          (analyse-sum analyse tag valueC))
+
+        (#;Var id)
+        (do @
+          [bound? (&;within-type-env
+                   (TC;bound? id))]
+          (if bound?
+            (do @
+              [expected' (&;within-type-env
+                          (TC;read-var id))]
+              (&;with-expected-type expected'
+                (analyse-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.
+            (&;fail (format "Invalid type for variant: " (%type expected)))))
+
+        (#;UnivQ _)
+        (do @
+          [[var-id var] (&;within-type-env
+                         TC;existential)]
+          (&;with-expected-type (assume (type;apply-type expected var))
+            (analyse-sum analyse tag valueC)))
+
+        (#;ExQ _)
+        (&common;with-var
+          (function [[var-id var]]
+            (&;with-expected-type (assume (type;apply-type expected var))
+              (analyse-sum analyse tag valueC))))
+        
+        _
+        (&;fail "")))))
+
+## Tuples get analysed into binary products for the sake of semantic
+## simplicity, since products/pairs can encode tuples of any length
+## through nesting.
+
+(def: (product members)
+  (-> (List la;Analysis) la;Analysis)
+  (case members
+    #;Nil
+    #la;Unit
+
+    (#;Cons singleton #;Nil)
+    singleton
+
+    (#;Cons left right)
+    (#la;Product left (product right))))
+
 (def: (analyse-typed-product analyse members)
   (-> &;Analyser (List Code) (Lux la;Analysis))
   (do Monad<Lux>
@@ -32,6 +134,8 @@
     (loop [expected expected
            members members]
       (case [expected members]
+        ## 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 (&;with-expected-type leftT
@@ -39,10 +143,29 @@
            rightA (recur rightT rightC)]
           (wrap (#la;Product leftA rightA)))
 
+        ## If the tuple runs out, whatever expression is the last gets
+        ## matched to the remaining type.
         [tailT (#;Cons tailC #;Nil)]
         (&;with-expected-type tailT
           (analyse tailC))
 
+        ## If, however, the type runs out but there is still enough
+        ## tail, the remaining elements get packaged into another
+        ## tuple, and analysed through the intermediation of a
+        ## temporary local variable.
+        ## 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.
+        ## The reason why an intermediate variable is used is that if
+        ## the code was just re-written with just tuple nesting, the
+        ## resulting analysis would have undone the explicity nesting,
+        ## since Product nodes rely on nesting inherently, thereby
+        ## blurring the line between what was wanted (the separation)
+        ## and what was analysed.
         [tailT tailC]
         (do @
           [g!tail (macro;gensym "tail")]
@@ -52,73 +175,6 @@
                          (~ g!tail))))))
         ))))
 
-(def: #export (normalize-record pairs)
-  (-> (List [Code Code]) (Lux (List [Ident Code])))
-  (mapM Monad<Lux>
-        (function [[key val]]
-          (case key
-            [_ (#;Tag key)]
-            (do Monad<Lux>
-              [key (macro;normalize key)]
-              (wrap [key val]))
-
-            _
-            (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key)))))
-        pairs))
-
-(def: #export (order-record pairs)
-  (-> (List [Ident Code]) (Lux [(List Code) Type]))
-  (case pairs
-    (#;Cons [head-k head-v] _)
-    (do Monad<Lux>
-      [head-k (macro;normalize head-k)
-       [_ tag-set recordT] (macro;resolve-tag head-k)
-       #let [size-record (list;size pairs)
-             size-ts (list;size tag-set)]
-       _ (if (n.= size-ts size-record)
-           (wrap [])
-           (&;fail (format "Record size does not match tag-set size." "\n"
-                           "Expected: " (|> size-ts nat-to-int %i) "\n"
-                           "  Actual: " (|> size-record nat-to-int %i) "\n"
-                           "For type: " (%type recordT))))
-       #let [tuple-range (list;n.range +0 (n.dec size-ts))
-             tag->idx (D;from-list ident;Hash<Ident> (list;zip2 tag-set tuple-range))]
-       idx->val (foldM @
-                       (function [[key val] idx->val]
-                         (do @
-                           [key (macro;normalize key)]
-                           (case (D;get key tag->idx)
-                             #;None
-                             (&;fail (format "Tag " (%code (code;tag key))
-                                             " does not belong to tag-set for type " (%type recordT)))
-
-                             (#;Some idx)
-                             (if (D;contains? idx idx->val)
-                               (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
-                               (wrap (D;put idx val idx->val))))))
-                       (: (D;Dict Nat Code)
-                          (D;new number;Hash<Nat>))
-                       pairs)
-       #let [ordered-tuple (L/map (function [idx]
-                                    (assume (D;get idx idx->val)))
-                                  tuple-range)]]
-      (wrap [ordered-tuple recordT]))
-
-    _
-    (:: Monad<Lux> wrap [(list) Unit])))
-
-(def: (tuple members)
-  (-> (List la;Analysis) la;Analysis)
-  (case members
-    #;Nil
-    #la;Unit
-
-    (#;Cons singleton #;Nil)
-    singleton
-
-    (#;Cons left right)
-    (#la;Product left (tuple right))))
-
 (def: #export (analyse-product analyse membersC)
   (-> &;Analyser (List Code) (Lux la;Analysis))
   (do Monad<Lux>
@@ -143,13 +199,14 @@
                           (TC;read-var id))]
               (&;with-expected-type expected'
                 (analyse-product analyse membersC)))
+            ## Must do inference...
             (do @
               [membersTA (mapM @ (|>. analyse &common;with-unknown-type)
                                membersC)
                _ (&;within-type-env
                   (TC;check expected
                             (type;tuple (L/map product;left membersTA))))]
-              (wrap (tuple (L/map product;right membersTA))))))
+              (wrap (product (L/map product;right membersTA))))))
 
         (#;UnivQ _)
         (do @
@@ -168,183 +225,91 @@
         (&;fail "")
         ))))
 
-(def: (record-function-type type)
-  (-> Type (Lux Type))
-  (case type
-    (#;Named name unnamedT)
-    (do Monad<Lux>
-      [unnamedT+ (record-function-type unnamedT)]
-      (wrap (#;Named name unnamedT+)))
-
-    (^template [<tag>]
-      (<tag> env bodyT)
-      (do Monad<Lux>
-        [bodyT+ (record-function-type bodyT)]
-        (wrap (<tag> env bodyT+))))
-    ([#;UnivQ]
-     [#;ExQ])
-
-    (#;Product _)
-    (:: Monad<Lux> wrap (type;function (type;flatten-tuple type) type))
-
-    _
-    (&;fail (format "Not a record type: " (%type type)))))
-
-(def: (out-of-bounds-error type size tag)
-  (All [a] (-> Type Nat Nat (Lux a)))
-  (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n"
-                  " Tag: " (%i (nat-to-int tag)) "\n"
-                  "Size: " (%i (nat-to-int size)) "\n"
-                  "Type: " (%type type))))
-
-(def: (variant-function-type tag expected-size type)
-  (-> Nat Nat Type (Lux Type))
-  (case type
-    (#;Named name unnamedT)
-    (do Monad<Lux>
-      [unnamedT+ (variant-function-type tag expected-size unnamedT)]
-      (wrap (#;Named name unnamedT+)))
-
-    (^template [<tag>]
-      (<tag> env bodyT)
-      (do Monad<Lux>
-        [bodyT+ (variant-function-type tag expected-size bodyT)]
-        (wrap (<tag> env bodyT+))))
-    ([#;UnivQ]
-     [#;ExQ])
-
-    (#;Sum _)
-    (let [cases (type;flatten-variant type)
-          actual-size (list;size cases)
-          boundary (n.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)
-              (:: Monad<Lux> wrap (type;function (list caseT) type))
-
-              #;None
-              (out-of-bounds-error type expected-size tag))
-            
-            (n.< expected-size actual-size)
-            (&;fail (format "Variant type is smaller than expected." "\n"
-                            "Expected: " (%i (nat-to-int expected-size)) "\n"
-                            "  Actual: " (%i (nat-to-int actual-size))))
-
-            (n.= boundary tag)
-            (let [caseT (type;variant (list;drop boundary cases))]
-              (:: Monad<Lux> wrap (type;function (list caseT) type)))
-            
-            ## else
-            (out-of-bounds-error type expected-size tag)))
-
-    _
-    (&;fail (format "Not a variant type: " (%type type)))))
-
-(def: #export (analyse-record analyse members)
-  (-> &;Analyser (List [Code Code]) (Lux la;Analysis))
-  (do Monad<Lux>
-    [members (normalize-record members)
-     [members recordT] (order-record members)
-     expectedT macro;expected-type
-     functionT (record-function-type recordT)
-     [inferredT membersA] (&inference;apply-function analyse functionT members)
-     _ (&;within-type-env
-        (TC;check expectedT inferredT))]
-    (wrap (tuple membersA))))
-
-(do-template [<name> <side>]
-  [(def: (<name> inner)
-     (-> la;Analysis la;Analysis)
-     (#la;Sum (<side> inner)))]
-
-  [sum-left  #;Left]
-  [sum-right #;Right])
-
-(def: (variant tag size temp value)
-  (-> Nat Nat Nat la;Analysis la;Analysis)
-  (if (n.= (n.dec size) tag)
-    (if (n.= +1 tag)
-      (sum-right value)
-      (L/fold (function;const sum-left)
-              (sum-right value)
-              (list;n.range +0 (n.- +2 tag))))
-    (L/fold (function;const sum-left)
-            (case value
-              (#la;Sum _)
-              (#la;Case value (list [(#la;BindP temp)
-                                     (#la;Relative (#;Local temp))]))
-
-              _
-              value)
-            (list;n.range +0 tag))))
-
 (def: #export (analyse-tagged-sum analyse tag value)
   (-> &;Analyser Ident Code (Lux la;Analysis))
   (do Monad<Lux>
     [tag (macro;normalize tag)
      [idx group variantT] (macro;resolve-tag tag)
      #let [case-size (list;size group)]
-     functionT (variant-function-type idx case-size variantT)
-     [inferredT valueA+] (&inference;apply-function analyse functionT (list value))
+     inferenceT (&inference;variant-inference-type idx case-size variantT)
+     [inferredT valueA+] (&inference;apply-function analyse inferenceT (list value))
      expectedT macro;expected-type
      _ (&;within-type-env
         (TC;check expectedT inferredT))
      temp &env;next-local]
     (wrap (variant idx case-size temp (|> valueA+ list;head assume)))))
 
-(def: #export (analyse-sum analyse tag valueC)
-  (-> &;Analyser Nat Code (Lux la;Analysis))
-  (do Monad<Lux>
-    [expected macro;expected-type]
-    (&;with-stacked-errors
-      (function [_] (format "Invalid type for variant: " (%type expected)))
-      (case expected
-        (#;Sum _)
-        (let [flat (type;flatten-variant expected)
-              type-size (list;size flat)]
-          (case (list;nth tag flat)
-            (#;Some variant-type)
-            (do @
-              [valueA (&;with-expected-type variant-type
-                        (analyse valueC))
-               temp &env;next-local]
-              (wrap (variant tag type-size temp valueA)))
+## 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]) (Lux (List [Ident Code])))
+  (mapM Monad<Lux>
+        (function [[key val]]
+          (case key
+            [_ (#;Tag key)]
+            (do Monad<Lux>
+              [key (macro;normalize key)]
+              (wrap [key val]))
 
-            #;None
-            (out-of-bounds-error expected type-size tag)))
+            _
+            (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key)))))
+        record))
 
-        (#;Named name unnamedT)
-        (&;with-expected-type unnamedT
-          (analyse-sum analyse tag valueC))
+## 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]) (Lux [(List Code) Type]))
+  (case record
+    ## empty-record = empty-tuple = unit = []
+    #;Nil
+    (:: Monad<Lux> wrap [(list) Unit])
 
-        (#;Var id)
-        (do @
-          [bound? (&;within-type-env
-                   (TC;bound? id))]
-          (if bound?
-            (do @
-              [expected' (&;within-type-env
-                          (TC;read-var id))]
-              (&;with-expected-type expected'
-                (analyse-sum analyse tag valueC)))
-            (&;fail (format "Invalid type for variant: " (%type expected)))))
+    (#;Cons [head-k head-v] _)
+    (do Monad<Lux>
+      [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 [])
+           (&;fail (format "Record size does not match tag-set size." "\n"
+                           "Expected: " (|> size-ts nat-to-int %i) "\n"
+                           "  Actual: " (|> size-record nat-to-int %i) "\n"
+                           "For type: " (%type recordT))))
+       #let [tuple-range (list;n.range +0 (n.dec size-ts))
+             tag->idx (D;from-list ident;Hash<Ident> (list;zip2 tag-set tuple-range))]
+       idx->val (foldM @
+                       (function [[key val] idx->val]
+                         (do @
+                           [key (macro;normalize key)]
+                           (case (D;get key tag->idx)
+                             #;None
+                             (&;fail (format "Tag " (%code (code;tag key))
+                                             " does not belong to tag-set for type " (%type recordT)))
 
-        (#;UnivQ _)
-        (do @
-          [[var-id var] (&;within-type-env
-                         TC;existential)]
-          (&;with-expected-type (assume (type;apply-type expected var))
-            (analyse-sum analyse tag valueC)))
+                             (#;Some idx)
+                             (if (D;contains? idx idx->val)
+                               (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
+                               (wrap (D;put idx val idx->val))))))
+                       (: (D;Dict Nat Code)
+                          (D;new number;Hash<Nat>))
+                       record)
+       #let [ordered-tuple (L/map (function [idx] (assume (D;get idx idx->val)))
+                                  tuple-range)]]
+      (wrap [ordered-tuple recordT]))
+    ))
 
-        (#;ExQ _)
-        (&common;with-var
-          (function [[var-id var]]
-            (&;with-expected-type (assume (type;apply-type expected var))
-              (analyse-sum analyse tag valueC))))
-        
-        _
-        (if (n.= +0 tag)
-          (analyse valueC)
-          (&;fail ""))))))
+(def: #export (analyse-record analyse members)
+  (-> &;Analyser (List [Code Code]) (Lux la;Analysis))
+  (do Monad<Lux>
+    [members (normalize members)
+     [members recordT] (order members)
+     expectedT macro;expected-type
+     inferenceT (&inference;record-inference-type recordT)
+     [inferredT membersA] (&inference;apply-function analyse inferenceT members)
+     _ (&;within-type-env
+        (TC;check expectedT inferredT))]
+    (wrap (product membersA))))
diff --git a/new-luxc/source/luxc/analyser/type.lux b/new-luxc/source/luxc/analyser/type.lux
index 3b9b83245..1eb278d2a 100644
--- a/new-luxc/source/luxc/analyser/type.lux
+++ b/new-luxc/source/luxc/analyser/type.lux
@@ -6,7 +6,9 @@
   (luxc ["&" base]
         (lang ["la" analysis #+ Analysis])))
 
-## [Analysers]
+## These 2 analysers are somewhat special, since they require the
+## means of evaluating Lux expressions at compile-time for the sake of
+## computing Lux type values.
 (def: #export (analyse-check analyse eval type value)
   (-> &;Analyser &;Eval Code Code (Lux Analysis))
   (do Monad<Lux>
diff --git a/new-luxc/test/test/luxc/analyser/structure.lux b/new-luxc/test/test/luxc/analyser/structure.lux
index b38a904c3..2b75baa9a 100644
--- a/new-luxc/test/test/luxc/analyser/structure.lux
+++ b/new-luxc/test/test/luxc/analyser/structure.lux
@@ -82,15 +82,6 @@
 
                          _
                          false)))
-      (assert "Can analyse pseudo-sum."
-              (|> (&;with-expected-type valueT
-                    (@;analyse-sum analyse +0 valueC))
-                  (macro;run init-compiler)
-                  (case> (#R;Success sumA)
-                         true
-
-                         _
-                         false)))
       (assert "Can analyse sum through bound type-vars."
               (|> (&;with-scope
                     (@common;with-var