diff --git a/Graph-notes-copy2.vue b/Graph-notes-copy2.vue
index a21ea07..2f91b26 100644
--- a/Graph-notes-copy2.vue
+++ b/Graph-notes-copy2.vue
@@ -1,14 +1,14 @@
-<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-03-23 -->
+<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-04-11 -->
 <!-- Tufts VUE: http://vue.tufts.edu/ -->
 <!-- Do Not Remove: VUE mapping @version(1.1) jar:file:/nix/store/z92y35qgs6g3cvvh0i4f14mg5n47zvvi-vue-3.3.0/share/vue/vue.jar!/tufts/vue/resources/lw_mapping_1_1.xml -->
-<!-- Do Not Remove: Saved date Thu Mar 23 01:54:28 CET 2017 by georges on platform Linux 4.4.40 in JVM 1.8.0_122-04 -->
+<!-- Do Not Remove: Saved date Tue Apr 11 14:04:44 CEST 2017 by georges on platform Linux 4.4.40 in JVM 1.8.0_122-04 -->
 <!-- Do Not Remove: Saving version @(#)VUE: built October 8 2015 at 1724 by tomadm on Linux 2.6.32-504.23.4.el6.x86_64 i386 JVM 1.7.0_21-b11(bits=32) -->
 <?xml version="1.0" encoding="US-ASCII"?>
 <LW-MAP xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
     xsi:noNamespaceSchemaLocation="none" ID="0"
     label="Graph-notes-copy2.vue" created="1479309847604" x="0.0"
     y="0.0" width="1.4E-45" height="1.4E-45" strokeWidth="0.0" autoSized="false">
-    <resource referenceCreated="1490230468578" size="216025"
+    <resource referenceCreated="1491912284366" size="216026"
         spec="/home/georges/phc/racket-packages/phc-graph/Graph-notes-copy2.vue"
         type="1" xsi:type="URLResource">
         <title>Graph-notes-copy2.vue</title>
@@ -3914,7 +3914,7 @@
         <URIString>http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2</URIString>
     </layer>
     <userZoom>0.75</userZoom>
-    <userOrigin x="-1182.522" y="-189.81644"/>
+    <userOrigin x="-1182.522" y="-282.81644"/>
     <presentationBackground>#FFFFFF</presentationBackground>
     <PathwayList currentPathway="0" revealerIndex="-1">
         <pathway ID="0" label="Chemin sans nom" created="1479309847603"
diff --git a/info.rkt b/info.rkt
index 0d7b185..eb4e939 100644
--- a/info.rkt
+++ b/info.rkt
@@ -16,7 +16,8 @@
                "remember"
                "extensible-parser-specifications"
                "subtemplate"
-               "stxparse-info"))
+               "stxparse-info"
+               "dotlambda"))
 (define build-deps '("scribble-lib"
                      "racket-doc"
                      "remember"
diff --git a/invariants-phantom.hl.rkt b/invariants-phantom.hl.rkt
index c89b684..43400a9 100644
--- a/invariants-phantom.hl.rkt
+++ b/invariants-phantom.hl.rkt
@@ -331,8 +331,10 @@ invariants, and therefore use a second nested function type to flip again the
 variance direction. We always include the @racket[Or] element in the union, to
 avoid ever having an empty union.
 
+@chunk[<Or>
+       (struct Or ())]
+
 @chunk[<grouping-invariants>
-       (struct Or ())
        (define-type-expander (Invariants stx)
          (syntax-case stx ()
            [(_ invᵢ …)
@@ -405,25 +407,6 @@ making a union of all paths, without factoring out common parts.
 
 @chunk[<parse>
        (begin-for-syntax
-         (define-syntax-class dot-ish
-           #:literals (dot λdot)
-           (pattern ({~and d dot} e …)
-                    #:with full
-                    (add-between (syntax->list #'(e …))
-                                 (datum->syntax #'d '|.| #'d #'d)))
-           (pattern ({~and d λdot} e …)
-                    #:with full
-                    (cons (datum->syntax #'d '|.| #'d #'d)
-                          (add-between (syntax->list #'(e …))
-                                       (datum->syntax #'d '|.| #'d #'d)))))
-         (define-syntax ~dot-ish
-           (pattern-expander
-            (λ (stx)
-              (syntax-case stx ()
-                [(_ pat …)
-                 #'(~and x:dot-ish
-                         (~parse (pat …) #'x.full))]))))
-
          (define (match-id rx id)
            (let ([m (regexp-match rx (identifier→string id))])
              (and m (map (λ (%) (datum->syntax id (string->symbol %) id id))
@@ -445,25 +428,34 @@ making a union of all paths, without factoring out common parts.
            #:attributes (τ)
            (pattern {~rx-id #px"^:([^:]+)$" τ}))
          (define-syntax-class π-elements
-           #:datum-literals (|.|)
+           #:literals (#%dotted-id #%dot-separator)
            #:attributes ([f 1] [τ 1])
-           (pattern (~dot-ish {~seq |.| :f+τ} …)))
+           (pattern (#%dotted-id {~seq #%dot-separator :f+τ} …)))
+         (define-syntax-class extract-star
+           #:literals (* #%dotted-id)
+           (pattern (#%dotted-id {~and st *} . rest)
+                    #:with {extracted-star …} #'{st (#%dotted-id . rest)})
+           (pattern other
+                    #:with {extracted-star …} #'{other}))
          (define-syntax-class sub-elements
-           #:literals (*) #:datum-literals (|.|)
+           #:literals (* #%dot-separator)
            #:attributes ([f 2] [τ 2] [sub 1])
            (pattern
-            ({~either :π-elements {~seq sub:sub-elements *}} …))))]
+            (:extract-star …)
+            #:with ({~either :π-elements {~seq sub:sub-elements *}} …)
+            #|  |# #'(extracted-star … …))))]
 
 @chunk[<parse>
-       (define-type-expander (<~τ stx)
-         (syntax-case stx ()
+       (define-type-expander <~τ
+         (syntax-parser
            [(_ τ) #'τ]
            [(_ f₀ . more)
-            #'(f₀ (<~τ . more))]))
+            #`(f₀ (<~τ . more))]))
        (begin-for-syntax
          (define-template-metafunction generate-sub-π
            (syntax-parser
              [(_ :sub-elements after)
+              #:with R (gensym 'R)
               (template
                (Rec R
                     (U (<~τ (?? (∀ (more) (generate-sub-π sub more))
@@ -476,14 +468,22 @@ making a union of all paths, without factoring out common parts.
                        after)))])))
        (define-type-expander Π
          (syntax-parser
-           [(_ {~optional (~dot-ish fst-τ:just-τ {~seq |.| fst:f+τ} …)}
+           #:literals (#%dotted-id #%dot-separator)
+           [(_ {~optional (~or (#%dotted-id fst-τ:just-τ
+                                            {~seq #%dot-separator fst:f+τ} …)
+                               (~and fst-τ:just-τ
+                                     {~parse (fst:f+τ …) #'()})
+                               {~datum :})}
                . :sub-elements)
-            (template (Rec R (U (Pairof Any R)
-                                (List* (?? (?@ (Pairof AnyField fst-τ.τ)
-                                               (Pairof (?? 'fst.f AnyField)
-                                                       (?? fst.τ AnyType))
-                                               …))
-                                       <π>))))]))]
+            #:with R (gensym 'R)
+            (template/top-loc
+             this-syntax
+             (Rec R (U (Pairof Any R)
+                       (List* (?? (?@ (Pairof AnyField fst-τ.τ)
+                                      (Pairof (?? 'fst.f AnyField)
+                                              (?? fst.τ AnyType))
+                                      …))
+                              <π>))))]))]
 
 @chunk[<π>
        (<~τ (?? (∀ (more) (generate-sub-π sub more))
@@ -494,18 +494,31 @@ making a union of all paths, without factoring out common parts.
             Null)]
 
 @chunk[<Invariant>
+       ;; TODO: /top-loc everywhere
        (define-type-expander Invariant
          (syntax-parser
            #:literals (≡ ≢ ∈ ∉ ∋ ∌)
-           ;; For ≡ and ≢, use (U l r) because they are symmetric
-           [(_ π₁ … ≡ π₂ …) #`(inv≡ (U (Π π₁ …) (Π π₂ …)))]
-           [(_ π₁ … ≢ π₂ …) #`(inv≢ (U (Π π₁ …) (Π π₂ …)))]
+           [(_ π₁ … ≡ π₂ …) #`(U (inv≡ (Pairof (Π π₁ …) (Π π₂ …)))
+                                 (inv≡ (Pairof (Π π₂ …) (Π π₁ …))))]
+           [(_ π₁ … ≢ π₂ …) #`(U (inv≢ (Pairof (Π π₁ …) (Π π₂ …)))
+                                 (inv≢ (Pairof (Π π₂ …) (Π π₁ …))))]
            [(_ π₁ … ∈ π₂ …) #`(inv∈ (Pairof (Π π₁ …) (Π π₂ …)))]
            [(_ π₁ … ∋ π₂ …) #`(inv∈ (Pairof (Π π₂ …) (Π π₁ …)))]
            [(_ π₁ … ∉ π₂ …) #`(inv≢ (Pairof (Π π₁ …) (Π π₂ … ?)))]
            [(_ π₁ … ∌ π₂ …) #`(inv≢ (Pairof (Π π₂ …) (Π π₁ … ?)))]
            ))]
 
+@chunk[<Invariants>
+       (define-type-expander Invariants
+         (syntax-parser
+           [(_ inv …)
+            #`(→ (U Or (Invariant . inv) …) Void)]))]
+
+@chunk[<Any*>
+       (struct AnyField () #:transparent)
+       (struct AnyType () #:transparent)
+       (define-type ε (Π))]
+
 @subsubsection{Comparison operator tokens}
 
 We define some tokens which will be used to identify the operator which
@@ -551,9 +564,6 @@ relates two nodes in the graph.
        (struct ε () #:transparent)
        (struct (T) Target ([x : T]) #:transparent)
        (struct (T) NonTarget Target () #:transparent)
-
-       (struct AnyField () #:transparent)
-       (struct AnyType () #:transparent)
        
        (define-type-expander Cycle
          (syntax-parser
@@ -617,16 +627,23 @@ relates two nodes in the graph.
 
 @subsection{Putting it all together}
 
-@chunk[<*>
-       (require (for-syntax racket/base
+@CHUNK[<*>
+       (require (only-in typed/dotlambda #%dotted-id #%dot-separator)
+                "dot-lang.rkt"
+                (for-syntax racket/base
                             racket/list
                             phc-toolkit/untyped
                             syntax/parse
                             syntax/parse/experimental/template)
                 (for-meta 2 racket/base)
                 (for-meta 2 phc-toolkit/untyped/aliases)
-                (for-meta 3 racket/base)
-                "dot-lang.rkt")
+                (for-meta 3 racket/base))
+
+       (begin-for-syntax
+         (define-syntax-rule (quasisyntax e)
+           (quasisyntax/top-loc this-syntax e))
+         (define-syntax-rule (template/top-loc loc e)
+           (quasisyntax/top-loc loc #,(template e))))
 
        (provide ≡ ≢ ∈ ∉ ∋ ∌)
        
@@ -637,8 +654,8 @@ relates two nodes in the graph.
                 inv≡
                 inv≢
                 Or
-                Target
-                NonTarget
+                ;Target
+                ;NonTarget
                 ε
                 witness-value
                 Π
@@ -649,8 +666,11 @@ relates two nodes in the graph.
        <parse>
 
        <witness-value>
-       <grouping-invariants>
-       <cycles>
+       ;<grouping-invariants>
+       ;<cycles>
+       <Any*>
        <comparison-operators>
        <Invariant>
+       <Invariants>
+       <Or>
        <≡>]
diff --git a/test/invariant-phantom/simple.rkt b/test/invariant-phantom/simple.rkt
index d159073..e12133a 100644
--- a/test/invariant-phantom/simple.rkt
+++ b/test/invariant-phantom/simple.rkt
@@ -1,4 +1,5 @@
-#lang type-expander
+#lang typed/dotlambda
+(require type-expander)
 
 (require (lib "phc-graph/invariants-phantom.hl.rkt")
          "util.rkt"
@@ -6,122 +7,161 @@
          phc-toolkit)
 
 (check-same-type
- (Π (λdot a aa) ((λdot b c))* (λdot d e))
+ (Π .a.aa(.b.c)*.d.e)
  (Rec
-  R
-  (U (Pairof Any R)
+  R1
+  (U (Pairof Any R1)
      (Pairof
       (Pairof 'a AnyType)
       (Pairof
        (Pairof 'aa AnyType)
        (Rec
-        R
+        R2
         (U (Pairof
             (Pairof 'b AnyType)
-            (Pairof (Pairof 'c AnyType) R))
+            (Pairof (Pairof 'c AnyType) R2))
            (List (Pairof 'd AnyType) (Pairof 'e AnyType)))))))))
-(struct a ()); the field.
+
+(struct a ()); the node.
+(struct b ()); the node.
+
 (check-same-type
- (Π (dot :a aa) ((λdot b c))* (λdot d e))
+ (Π :a.aa(.b.c)*.d.e)
  (Rec
-  R
-  (U (Pairof Any R)
+  R1
+  (U (Pairof Any R1)
      (Pairof
       (Pairof AnyField a)
       (Pairof
        (Pairof 'aa AnyType)
        (Rec
-        R
+        R2
         (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
-           (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R)))))))))
+           (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2)))))))))
 (check-same-type
- (Π (dot :a) ((λdot b c))* (λdot d e))
+ (Π :a(.b.c)*.d.e)
  (Rec
-  R
-  (U (Pairof Any R)
+  R1
+  (U (Pairof Any R1)
      (Pairof
       (Pairof AnyField a)
       (Rec
-       R
+       R2
        (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
-          (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R))))))))
+          (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2))))))))
 
 (check-same-type
- (Π (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e))
+ (Π :a(.b.c(.w)*.x.y)*.d.e)
  (Rec
-  R
-  (U (Pairof Any R)
+  R1
+  (U (Pairof Any R1)
      (Pairof
       (Pairof AnyField a)
-      (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
-         (Pairof
-          (Pairof 'b AnyType)
+      (Rec
+       R2
+       (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
           (Pairof
-           (Pairof 'c AnyType)
-           (Rec
-            R
-            (U (Pairof (Pairof 'w AnyType) R)
-               (Pairof
-                (Pairof 'x AnyType)
-                (Pairof (Pairof 'y AnyType) R)))))))))))
+           (Pairof 'b AnyType)
+           (Pairof
+            (Pairof 'c AnyType)
+            (Rec
+             R3
+             (U (Pairof (Pairof 'w AnyType) R3)
+                (Pairof
+                 (Pairof 'x AnyType)
+                 (Pairof (Pairof 'y AnyType) R2))))))))))))
 
 ;; TODO: test with deeper nesting of ()*
 
 (check-same-type
- (Invariant (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)
-            ≡
-            (dot :a) ((λdot b c))* (λdot d e))
- (inv≡
-  (U (Rec
-      R
-      (U (Pairof Any R)
-         (Pairof
-          (Pairof AnyField a)
-          (Rec
-           R
-           (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
-              (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R)))))))
-     (Rec
-      R
-      (U (Pairof Any R)
-         (Pairof
-          (Pairof AnyField a)
-          (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
-             (Pairof
-              (Pairof 'b AnyType)
-              (Pairof
-               (Pairof 'c AnyType)
-               (Rec
-                R
-                (U (Pairof (Pairof 'w AnyType) R)
-                   (Pairof
-                    (Pairof 'x AnyType)
-                    (Pairof (Pairof 'y AnyType) R)))))))))))))
+ (Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e)
+ (U (inv≡
+     (Pairof
+      (Rec
+       R1
+       (U (Pairof Any R1)
+          (Pairof
+           (Pairof AnyField a)
+           (Rec
+            R2
+            (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
+               (Pairof
+                (Pairof 'b AnyType)
+                (Pairof (Pairof 'c AnyType) R2)))))))
+      (Rec
+       R1
+       (U (Pairof Any R1)
+          (Pairof
+           (Pairof AnyField a)
+           (Rec
+            R2
+            (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
+               (Pairof
+                (Pairof 'b AnyType)
+                (Pairof
+                 (Pairof 'c AnyType)
+                 (Rec
+                  R3
+                  (U (Pairof (Pairof 'w AnyType) R3)
+                     (Pairof
+                      (Pairof 'x AnyType)
+                      (Pairof (Pairof 'y AnyType) R2)))))))))))))
+    (inv≡
+     (Pairof
+      (Rec
+       R1
+       (U (Pairof Any R1)
+          (Pairof
+           (Pairof AnyField a)
+           (Rec
+            R2
+            (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
+               (Pairof
+                (Pairof 'b AnyType)
+                (Pairof
+                 (Pairof 'c AnyType)
+                 (Rec
+                  R3
+                  (U (Pairof (Pairof 'w AnyType) R3)
+                     (Pairof
+                      (Pairof 'x AnyType)
+                      (Pairof (Pairof 'y AnyType) R2)))))))))))
+      (Rec
+       R1
+       (U (Pairof Any R1)
+          (Pairof
+           (Pairof AnyField a)
+           (Rec
+            R2
+            (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
+               (Pairof
+                (Pairof 'b AnyType)
+                (Pairof (Pairof 'c AnyType) R2)))))))))))
 
 (check-same-type
- (Invariant (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)
+ (Invariant :a(.b.c(.w)*.x.y)*.d.e
             ∈
-            (dot :a) ((λdot b c))* (λdot d e))
- (Invariant (dot :a) ((λdot b c))* (λdot d e)
+            :a(.b.c)*.d.e)
+ (Invariant :a(.b.c)*.d.e
             ∋
-            (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)))
+            :a(.b.c(.w)*.x.y)*.d.e))
 
 
+;;;
+
 (check-ann witness-value (Invariants)) ;; No invariants
-(check-ann witness-value (Invariants (≡x (_ a) (_ a b c))))
+(check-ann witness-value (Invariants (:a ≡ :a.b.c)))
 
-(check-a-stronger-than-b (Invariants (≡x (_ a) (_ a b c)))
+(check-a-stronger-than-b (Invariants (:a ≡ :a.b.c))
                          (Invariants))
-
-(check-a-same-as-b (Invariants (≡x (_ a) (_ a b c)))
-                   (Invariants (≡x (_ a b c) (_ a))))
-
-(check-a-stronger-than-b (Invariants (≡x (_) (_ b c))
-                                     (≡x (_) (_ b d)))
-                         (Invariants (≡x (_) (_ b c))))
-(check-a-stronger-than-b (Invariants (≡x (_) (_ b d))
-                                     (≡x (_) (_ b c)))
-                         (Invariants (≡x (_) (_ b c))))
+(check-a-same-as-b (Invariants (:a ≡ :a.b.c))
+                   (Invariants (:a.b.c ≡ :a)))
+(check-a-stronger-than-b (Invariants (: ≡ :b.c)
+                                     (: ≡ :b.d))
+                         (Invariants (: ≡ :b.c)))
+(check-a-stronger-than-b (Invariants (: ≡ :b.d)
+                                     (: ≡ :b.c))
+                         (Invariants (: ≡ :b.c)))
 
 ;; ∀ .b.d(.a.b.>d)* of length ≥ 5
 ;; is stronger than
@@ -129,12 +169,9 @@
 ;; as the elements of the latter are included in the former, but
 ;; the first element (length = 5) is missing in the latter, so the
 ;; former constrains more paths.
-(check-a-stronger-than-b (Invariants (≡x (_)
-                                         (_ b d ↙ a b (d))))
-                         (Invariants (≡x (_)
-                                         (_ b d a b d ↙ a b (d)))))
+(check-a-stronger-than-b (Invariants (: ≡ .b.d(.a.b.d)*))
+                         (Invariants (: ≡ .b.d.a.b.d(.a.b.d)*)))
+
+(check-a-stronger-than-b (Invariants (: ≡ .a.b.c(.d.e)*))
+                         (Invariants (: ≡ .a.b.c.d.e)))
 
-(check-a-stronger-than-b (Invariants (≡x (_)
-                                         (_ a b c ↙ d (e))))
-                         (Invariants (≡x (_)
-                                         (_ a b c d e))))