diff --git a/flexible-with-generalized-ctor-test.rkt b/flexible-with-generalized-ctor-test.rkt
index 6cf65c6..c4eb7ce 100644
--- a/flexible-with-generalized-ctor-test.rkt
+++ b/flexible-with-generalized-ctor-test.rkt
@@ -30,76 +30,71 @@
       'none))
 |#
 
-(struct (A) Some ([f : A]) #:transparent)
-(struct (A) Some0 Some () #:transparent)
-(struct (A) Some1 Some () #:transparent)
-(struct (A) Some2 Some () #:transparent)
-(struct (A) Some3 Some () #:transparent)
-(struct (A) None ([f : A]) #:transparent)
+
+
+
+
+
+
+
+
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Actual good implementation:
+
+;(struct (A) Some ([f : A]) #:transparent)
+;(struct (A) Some0 Some () #:transparent)
+;(struct (A) Some1 Some () #:transparent)
+;(struct (A) Some2 Some () #:transparent)
+;(struct (A) Some3 Some () #:transparent)
+;(struct (A) None ([f : A]) #:transparent)
 
 ;; A is:
-#;(U (Pairof Any (None (Listof (Some Any))))
-     (Some Any))
+#;(Pairof Any (U (Some Any) (None (Listof Any))))
 
-(struct |0| ())
-(struct |1| ())
-(struct |2| ())
-(struct |3| ())
+(: f (builder-τ 4 2))
 
-(: f (∀ (A 0/K 0/X 1/K 1/X)
-        (→ (∩ 0/K (U |0| |1| |2| |3|))
-           0/X
-           (∩ 1/K (U |0| |1| |2| |3|))
-           1/X
-           (List
-            (∩
-             (U
-              (Pairof |0| (None (List (∩ 0/K (U |1| |2| |3|)) (∩ 1/K (U |1| |2| |3|)))))
-              (∩ (Pairof 0/K (Some 0/X)) (Pairof |0| Any))
-              (∩ (Pairof 1/K (Some 1/X)) (Pairof |0| Any)))
-             A)
-            (∩
-             (U
-              (Pairof |1| (None (List (∩ 0/K (U |0| |2| |3|)) (∩ 1/K (U |0| |2| |3|)))))
-              (∩ (Pairof 0/K (Some 0/X)) (Pairof |1| Any))
-              (∩ (Pairof 1/K (Some 1/X)) (Pairof |1| Any)))
-             A)
-            (∩
-             (U
-              (Pairof |2| (None (List (∩ 0/K (U |0| |1| |3|)) (∩ 1/K (U |0| |1| |3|)))))
-              (∩ (Pairof 0/K (Some 0/X)) (Pairof |2| Any))
-              (∩ (Pairof 1/K (Some 1/X)) (Pairof |2| Any)))
-             A)
-            (∩
-             (U
-              (Pairof |3| (None (List (∩ 0/K (U |0| |1| |2|)) (∩ 1/K (U |0| |1| |2|)))))
-              (∩ (Pairof 0/K (Some 0/X)) (Pairof |3| Any))
-              (∩ (Pairof 1/K (Some 1/X)) (Pairof |3| Any)))
-             A)))))
-
-(define (f kx x ky y)
+(define (f oracle kx x ky y)
   (list (cond
-          [((make-predicate |0|) kx) (cons kx (Some x))]
-          [((make-predicate |0|) ky) (cons ky (Some y))]
-          [else (cons |0| (None (list kx ky)))])
+          [((make-predicate '|0|) kx)
+           (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|0| Any))) (cons kx (Some x)))
+                (∩ (Pairof 0/K (Some 0/X)) (Pairof '|0| Any) A))]
+          [((make-predicate '|0|) ky)
+           (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|0| Any))) (cons ky (Some y)))
+                (∩ (Pairof 1/K (Some 1/X)) (Pairof '|0| Any) A))]
+          [else
+           ((inst oracle (Pairof '|0| (None (List (∩ 0/K (U '|1| '|2| '|3|)) (∩ 1/K (U '|1| '|2| '|3|))))))
+            (cons '|0| (None (list kx ky))))])
         (cond
-          [((make-predicate |1|) kx) (cons kx (Some x))]
-          [((make-predicate |1|) ky) (cons ky (Some y))]
-          [else (cons |1| (None (list kx ky)))])
+          [((make-predicate '|1|) kx)
+           (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|1| Any))) (cons kx (Some x)))
+                (∩ (Pairof 0/K (Some 0/X)) (Pairof '|1| Any) A))]
+          [((make-predicate '|1|) ky)
+           (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|1| Any))) (cons ky (Some y)))
+                (∩ (Pairof 1/K (Some 1/X)) (Pairof '|1| Any) A))]
+          [else
+           ((inst oracle (Pairof '|1| (None (List (∩ 0/K (U '|0| '|2| '|3|)) (∩ 1/K (U '|0| '|2| '|3|))))))
+            (cons '|1| (None (list kx ky))))])
         (cond
-          [((make-predicate |2|) kx) (cons kx (Some x))]
-          [((make-predicate |2|) ky) (cons ky (Some y))]
-          [else (cons |2| (None (list kx ky)))])
+          [((make-predicate '|2|) kx)
+           (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|2| Any))) (cons kx (Some x)))
+                (∩ (Pairof 0/K (Some 0/X)) (Pairof '|2| Any) A))]
+          [((make-predicate '|2|) ky)
+           (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|2| Any))) (cons ky (Some y)))
+                (∩ (Pairof 1/K (Some 1/X)) (Pairof '|2| Any) A))]
+          [else
+           ((inst oracle (Pairof '|2| (None (List (∩ 0/K (U '|0| '|1| '|3|)) (∩ 1/K (U '|0| '|1| '|3|))))))
+            (cons '|2| (None (list kx ky))))])
         (cond
-          [((make-predicate |3|) kx) (cons kx (Some x))]
-          [((make-predicate |3|) ky) (cons ky (Some y))]
-          [else (cons |3| (None (list kx ky)))]))
-  ((λ () (error "not yet"))))
-
-
-
-
-
-
-
-
+          [((make-predicate '|3|) kx)
+           (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|3| Any))) (cons kx (Some x)))
+                (∩ (Pairof 0/K (Some 0/X)) (Pairof '|3| Any) A))]
+          [((make-predicate '|3|) ky)
+           (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|3| Any))) (cons ky (Some y)))
+                (∩ (Pairof 1/K (Some 1/X)) (Pairof '|3| Any) A))]
+          [else
+           ((inst oracle (Pairof '|3| (None (List (∩ 0/K (U '|0| '|1| '|2|)) (∩ 1/K (U '|0| '|1| '|2|))))))
+            (cons '|3| (None (list kx ky))))])))
diff --git a/flexible-with-generalized-ctor.hl.rkt b/flexible-with-generalized-ctor.hl.rkt
index dbdfcc0..a97181f 100644
--- a/flexible-with-generalized-ctor.hl.rkt
+++ b/flexible-with-generalized-ctor.hl.rkt
@@ -1,101 +1,230 @@
-#lang dotlambda/unhygienic type-expander/lang
-#|hyper-literate #:♦ #:no-auto-require (dotlambda/unhygienic
+#lang hyper-literate #:꩜ #:no-auto-require (dotlambda/unhygienic
                                             . type-expander/lang)
 
-♦chunk[<*>|#
-       
-(provide builder-τ
-         None
-         Some
-         Some?
-         Some-f
-         propagate-τ)
+꩜title[#:tag "generalized-flex-ctor"]{Generalised constructor functions for
+ flexible structures}
 
-(require racket/require
-         (for-syntax (subtract-in racket/base subtemplate/override)
-                     syntax/stx
-                     racket/list
-                     racket/function
-                     subtemplate/override)
-         (for-meta 2 racket/base))
+꩜(require hyper-literate/diff1)
+꩜(init)
 
-(struct (T) Some ([f : T]))
-(struct (T) None ([f : T]))
+꩜chunk[<*>
+       (provide builder-τ
+                None
+                Some
+                Some?
+                Some-f
+                propagate-τ)
 
-(define-type-expander BinaryTree
-  (syntax-parser
-    [(_ leafⱼ …)
-     ;; TODO: implement BinaryTree.
-     #'(List leafⱼ …)]))
+       (require racket/require
+                (for-syntax (subtract-in racket/base subtemplate/override)
+                            syntax/stx
+                            racket/list
+                            racket/function
+                            subtemplate/override)
+                (for-meta 2 racket/base))
 
-(define-syntax (def-SomeNone* stx)
-  (syntax-case stx ()
-    [(_ Some n)
-     (with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i))
-                                   (range n))])
-       #`(begin
-           (provide Someᵢ …)
-           (struct (T) Someᵢ Some ()) …))]))
+       (struct (T) Some ([f : T]))
+       (struct (T) None ([f : T]))
 
-(def-SomeNone* Some 4)
+       (define-type-expander BinaryTree
+         (syntax-parser
+           [(_ leafⱼ …)
+            ;; TODO: implement BinaryTree.
+            #'(List leafⱼ …)]))
 
-(define-type-expander builder-τ
-  (syntax-parser
-    [(_ n m)
-     #:with (Nᵢ …) (range n)
-     #:with (Mⱼ …) (range m)
-     #:with (Someᵢ …) (map (λ (n) (format-id #'HERE? "Some~a" n)) (Nᵢ …))
-     #:with ((Someᵢⱼ …) …) (map λ.(map (const %) (Mⱼ …)) (#'Someᵢ …))
-     ;#:with ((Noneᵢⱼ …) …) (map (const #'(Noneᵢ …)) (Nᵢ …))
-     #:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …))
-     #:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …))
-     #:with ((Nᵢⱼ …) …) (map (λ (ni) (map (const ni) (Xⱼ …))) (Nᵢ …))
-     #:with ((Nⱼᵢ …) …) (map (const #'(Nᵢ …)) (Mⱼ …))
-     (define Ns (Nᵢ …))
-     (define Ms (Mⱼ …))
-     (define Somes (Someᵢ …))
-     ;(define/with-syntax exceptⱼ (remove Mⱼ Ns)) …
-     ;     (define/with-syntax ((exceptᵢⱼ …) …)
-     ;       (map (const (exceptⱼ …)) (Nᵢ …)))
-     (define/with-syntax (exceptᵢ …) ((remove Nᵢ Ns) …))
-     (define/with-syntax (((exceptᵢⱼ …) …) …)
-       ((map (const (remove Someᵢ Somes)) Ms) …))
+       (define-syntax (def-SomeNone* stx)
+         (syntax-case stx ()
+           [(_ Some n)
+            (with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i))
+                                          (range n))])
+              #`(begin
+                  (provide Someᵢ …)
+                  (struct (T) Someᵢ Some ()) …))]))
 
-     (define/with-syntax result
-       #'(∀ (A (?@ Kⱼ Xⱼ) …)
-            (→ (?@ (∩ Kⱼ (Some Any)) (∩ Kⱼ Xⱼ)) …
-               (BinaryTree
-                (∩ (U (Pairof Nᵢ
-                              ;; If Kⱼ is Nᵢ, then {∩ Kᵢⱼ {U . exceptᵢⱼ}} will
-                              ;; Nothing. We multiply the Nothing together by
-                              ;; building a List out of them (a single occurrence
-                              ;; of Nothing should collapse the list), so that the
-                              ;; result should be Nothing only if there is no Kⱼ
-                              ;; equal to Nᵢ. To force TR to propagate Nothing as
-                              ;; much as possible, we intersect it with
-                              ;; (None Any), which should be a no-op, but makes
-                              ;; sure the simplifier which runs with ∩ kicks in.
-                              ;; Therefore, the (None whatever) should appear only
-                              ;; if there is indeed no key provided for that leaf.
-                              (None (List {∩ Kᵢⱼ {U (exceptᵢⱼ Any) …}} …)))
-                      (∩ Kᵢⱼ (Someᵢⱼ Xᵢⱼ))
-                      …)
-                   A)
-                …))))
-     (displayln (syntax->datum #'result))
-     #'result]))
+       (def-SomeNone* Some 4)
 
-(define-type propagate-τ
-  (Pairof Any
-          (U (None (Listof Natural))
-             (Some Any))))
+       <builder-τ>
 
-; ../../../.racket/snapshot/pkgs/typed-racket-lib/typed-racket/types/overlap.rkt
-;:40:0: mask-accessor: contract violation
-;  expected: mask?
-;  given: #f
-;(define-type τ-4-2 (builder-τ 4 2))
+       <propagate-τ>]
+
+We first define the builder function's type. Since this type is rather
+complex, we define it using a macro. The type expander takes two arguments.
+The first argument ꩜racket[n] indicates the total number of fields which
+appear in the program (i.e. on the number of leaves of the generated tree
+type), and the second argument ꩜racket[m] indicates how many key/value pairs
+the function accepts.
+
+꩜chunk[<builder-τ>
+       (define-type-expander builder-τ
+         (syntax-parser
+           [(_ n m)
+            <builder-τ-with-1>
+            <builder-τ-with-2>
+            <builder-τ-with-3>
+            #'|<builder-function-type''>|]))]
+
+We start by defining a few syntax pattern variables which will be used in the
+later definitions. The lists ꩜racket[Nᵢ] and ꩜racket[Mⱼ] range over the field
+and argument indices, respectively:
+
+꩜chunk[<builder-τ-with-1>
+       #:with (Nᵢ …) (range n)
+       #:with (Mⱼ …) (range m)]
+
+The builder function takes a number of keys and values, and builds a (promise
+for) a binary tree where the leaves corresponding to those keys contain given
+value, and other leaves contain ꩜racket[None]. We could write (a simplified
+form of) the builder function type as follows:
+
+꩜chunk[<builder-function-type>
+       (∀ ({?@ Kⱼ Xⱼ} …)
+          (→ (code:comment "; Keys and values:")
+             {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
+             ;; Result type:
+             (BinaryTree |<Some or None>| …)))]
+
+We expect each key ꩜racket[Kⱼ] to be a symbol of the shape ꩜racket[|0|],
+꩜racket[|1|], ꩜racket[|2|] and so on:
+
+꩜chunk[<builder-τ-with-2>
+       #:with (NSymᵢ …) ((string->symbol (format "~a" Nᵢ)) …)
+       #:with ((NSymⱼᵢ …) …) (map (const (NSymᵢ …)) (Mⱼ …))]
+
+The type of each leaf of the binary tree should be ꩜racket[(Some Xⱼ)] if a
+corresponding ꩜racket[Kⱼ] matches the leaf name, and ꩜racket[None] otherwise.
+
+꩜chunk[|<Some or None>|
+       (U |<(Some Xⱼ) if Kⱼ = NSymᵢ>|
+          |<None if ∀ k ∈ Kⱼ, k ≠ NSymᵢ>|)]
+
+This type-level conditional is achieved via a trick involving intersection
+types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one
+of the ꩜racket['NSymᵢ …] symbols. For a given leaf with index ꩜racket[i], if
+the ꩜racket[Kⱼ] key is the type ꩜racket['NSymᵢ], then the intersection type
+꩜racket[(∩ Kⱼ 'NSymᵢ)] is ꩜racket['NSymᵢ]. Conversely, if the ꩜racket[Kⱼ] key
+is not ꩜racket['NSymᵢ], the intersection will be the bottom type
+꩜racket[Nothing]. No values inhabit the bottom type, and Typed Racket can
+determine that there is no pair whose first (or second) element has the type
+꩜racket[Nothing], since no concrete value could be used to construct such a
+pair.
+
+꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>|
+       (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ)
+               (Some Xᵢⱼ))
+       …]
+
+where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows:
+
+꩜chunk[<builder-τ-with-3>
+       #:with ((Kᵢⱼ …) …) (map (const (Kⱼ …)) (Nᵢ …))
+       #:with ((Xᵢⱼ …) …) (map (const (Xⱼ …)) (Nᵢ …))
+       #:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))]
+
+We use this fact to construct a pair above. Its first element is either
+꩜racket['NSymᵢ] when ꩜racket[Kⱼ] is ꩜racket['NSymᵢ], and ꩜racket[Nothing]
+otherwise. The second element of the pair contains our expected
+꩜racket[(Some Xⱼ)] type, but the whole pair is collapsed to ꩜racket[Nothing]
+when ꩜racket[Kⱼ] is not ꩜racket['NSymᵢ].
+
+We use a similar approach to conditionally produce the ꩜racket[None] element,
+but instead of intersecting ꩜racket[Kⱼ] with ꩜racket['NSymᵢ], we intersect it
+with the complement of ꩜racket['NSymᵢ]. Typed Racket lacks the possibility to
+negate a type, so we manually compute the complement of ꩜racket['NSymᵢ] in the
+set of possible keys (that is, ꩜racket['NSymᵢ …]).
+
+꩜chunk[<builder-τ-with-3>
+       #:with NSyms (NSymᵢ …)
+       #:with Ms (Mⱼ …)
+       #:with (exceptᵢ …) ((remove NSymᵢ NSyms) …)
+       #:with (((exceptᵢⱼ …) …) …) ((map (const exceptᵢ) Ms) …)]
+
+If ꩜racket[Kⱼ] is ꩜racket[Nᵢ], then ꩜racket[{∩ Kⱼ {U . exceptᵢ}}] will be
+꩜racket[Nothing]. We take the Cartesian product of the intersections by
+building a ꩜racket[List] out of them. A single occurrence of ꩜racket[Nothing]
+will collapse the whole list to ꩜racket[Nothing], because the Cartesian
+product of the empty set and any other set will produce the empty set.
+
+The resulting type should therefore be ꩜racket[Nothing] only if there is no
+꩜racket[Kⱼ] equal to ꩜racket[Nᵢ], and be the list of symbols
+꩜racket[(List . exceptᵢ)] otherwise.
+
+꩜chunk[|<None if ∀ k ∈ Kⱼ, k ≠ NSymᵢ>|
+       (Pairof 'NSymᵢ
+               (None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …)))]
+
+This approach relies on the fact that occurrences of ꩜racket[Nothing] within
+structs and pairs containing collapse the entire struct or pair type to
+꩜racket[Nothing]. Unfortunately, current versions of Typed Racket perform this
+simplification step in some situations but not others:
+
+꩜itemlist[
+ ꩜item{It simplifies polymorphic types when they are defined;}
+ ꩜item{When a polymorphic type is instantiated, the parts which are directly
+  affected by the intersection with a polymorphic type variable are subject to
+  this simplification;}
+ ꩜item{However, occurrences of ꩜racket[Nothing] which occur as a result of
+  instantiating the type variable do not propagate outside of the intersection
+  itself. This means that given the following type:
+  ꩜racketblock[(define-type (Foo A) (U (Pairof (∩ Integer A) String) Boolean))]
+  its instantiation ꩜racket[(Foo Symbol)] will produce the type
+  ꩜racket[(U (Pairof Nothing String) Boolean)], but this type will not be
+  simplified to ꩜racket[(U Nothing Boolean)] or equivalently to
+  ꩜racket[Boolean].}]
+
+To force Typed Racket to propagate ꩜racket[Nothing] outwards as much as
+we need, we intersect the whole form with a polymorphic type ꩜racket[A]:
+
+꩜hlite[|<builder-function-type'>|
+       {/(∀(+ _ / _ _)(→ _ _ ooo (bt + (∩ / _ + A) / _)))}
+       (∀ (A {?@ Kⱼ Xⱼ} …)
+          (→ (code:comment "; Keys and values:")
+             {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
+             ;; Result type:
+             (BinaryTree (∩ |<Some or None>| A) …)))]
+
+The type ꩜racket[propagate-τ] defined below is used to instantiate ꩜racket[A],
+and is carefully picked so that its intersection will in no way change the
+result type (i.e. the intersection with ꩜racket[A] will be an identity
+operation where it is used). In other words, ꩜racket[propagate-τ] has the same
+shape as the leaves of the binary tree. This intersection however forces the
+simplification step to be performed on the affected parts once the type is
+instantiated.
+
+꩜chunk[<propagate-τ>
+       (define-type propagate-τ
+         (Pairof Any
+                 (U (None (Listof Natural))
+                    (Some Any))))]
+
+꩜;Use chunkref instead of ꩜racket[|<Some or None>|] ?
+
+The implementation of the builder function will need to convert values with
+the ꩜racket[|<Some or None>|] type to values of type
+꩜racket[(∩ |<Some or None>| A)]. Since the intersection could, in principle,
+be any subtype of ꩜racket[|<Some or None>|], we request that the caller
+supplies a proof that the conversion is possible. This proof takes the form of
+an ꩜racket[oracle] function, which transforms an element with the type
+꩜racket[propagate-τ] (which is a supertype of every possible
+꩜racket[|<Some or None>|] type) into an element with the type
+꩜racket[(∩ A B)], where ꩜racket[B] is the original type of the value to
+upgrade.
+
+꩜chunk[<oracle-type>
+       (∀ (B) (→ (∩ B
+                    (Pairof Any (U (Some Any) (None (Listof Any)))))
+                 (∩ A B)))]
+
+The builder function type is updated as follows:
+
+꩜hlite[|<builder-function-type''>|
+       {/(∀(_ _ _)(→ + _ _ / _ _ ooo _))}
+       (∀ (A {?@ Kⱼ Xⱼ} …)
+          (→ (code:comment "; Oracle:")
+             <oracle-type>
+             (code:comment "; Keys and values:")
+             {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
+             ;; Result type:
+             (BinaryTree (∩ |<Some or None>| A) …)))]
 
 
-;]
 
diff --git a/scribblings/phc-graph-implementation.scrbl b/scribblings/phc-graph-implementation.scrbl
index d3fe94f..3c8e70e 100644
--- a/scribblings/phc-graph-implementation.scrbl
+++ b/scribblings/phc-graph-implementation.scrbl
@@ -17,4 +17,5 @@ the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document.
 @include-section[(submod "../graph-info.hl.rkt" doc)]
 @include-section[(submod "../graph-type.hl.rkt" doc)]
 @include-section[(submod "../graph.hl.rkt" doc)]
-@include-section[(submod "../main-draft.hl.rkt" doc)]
\ No newline at end of file
+@include-section[(submod "../main-draft.hl.rkt" doc)]
+@include-section[(submod "../flexible-with-generalized-ctor.hl.rkt" doc)]