Make summary unification more conservative; infer implicit arguments after applications

4 files changed, 77 insertions, 77 deletions

diff --git a/lib/ur/monad.ur b/lib/ur/monad.ur
index efba7546..e15da523 100644
--- a/lib/ur/monad.ur
+++ b/lib/ur/monad.ur
@@ -1,10 +1,10 @@
 fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) =
-    foldR [m] [fn ts => m $ts]
-    (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
-        this <- action;
-        others <- acc;
-        return ({nm = this} ++ others))
-    (return {}) [ts] fd r
+    @foldR [m] [fn ts => m $ts]
+     (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
+         this <- action;
+         others <- acc;
+         return ({nm = this} ++ others))
+     (return {}) fd r
 
 fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
 
@@ -16,40 +16,40 @@ fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
           (f : nm :: Name -> t :: K -> rest :: {K}
                -> [[nm] ~ rest] =>
            tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
-          (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
-             (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                              (acc : _ -> m (tr rest)) r =>
-                 acc' <- acc (r -- nm);
-                 f [nm] [t] [rest] ! r.nm acc')
-             (fn _ => return i)
-             [_] fl
+          (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> m (tr rest)) r =>
+         acc' <- acc (r -- nm);
+         f [nm] [t] [rest] ! r.nm acc')
+     (fn _ => return i)
+     fl
 
 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
             tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-           (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
-       (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                        (acc : _ -> _ -> m (tr rest)) r1 r2 =>
-           acc' <- acc (r1 -- nm) (r2 -- nm);
-           f [nm] [t] [rest] ! r1.nm r2.nm acc')
-       (fn _ _ => return i)
-       [_] fl
+           (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> _ -> m (tr rest)) r1 r2 =>
+         acc' <- acc (r1 -- nm) (r2 -- nm);
+         f [nm] [t] [rest] ! r1.nm r2.nm acc')
+     (fn _ _ => return i)
+     fl
 
 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
             tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-           (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
-       (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                        (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
-           acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
-           f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
-       (fn _ _ _ => return i)
-       [_] fl
+           (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
+         acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
+         f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
+     (fn _ _ _ => return i)
+     fl
 
 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
          (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index 9ad9262d..698a4b5b 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -14,7 +14,7 @@ val foldR : K --> m ::: (Type -> Type) -> monad m
                 -> [[nm] ~ rest] =>
                 tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
             -> tr []
-            -> r :: {K} -> folder r -> $(map tf r) -> m (tr r)
+            -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r)
 
 val foldR2 : K --> m ::: (Type -> Type) -> monad m
              -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
@@ -23,7 +23,7 @@ val foldR2 : K --> m ::: (Type -> Type) -> monad m
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
 
 val foldR3 : K --> m ::: (Type -> Type) -> monad m
              -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
@@ -32,16 +32,16 @@ val foldR3 : K --> m ::: (Type -> Type) -> monad m
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
 
 val mapR : K --> m ::: (Type -> Type) -> monad m
            -> tf :: (K -> Type)
            -> tr :: (K -> Type)
            -> (nm :: Name -> t :: K -> tf t -> m (tr t))
-           -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
+           -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
 
 val mapR2 : K --> m ::: (Type -> Type) -> monad m
             -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
             -> tr :: (K -> Type)
             -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
-            -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
+            -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index e4e33940..b6f6349a 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -9,7 +9,7 @@ con folder = K ==> fn r :: {K} =>
 fun fold [K] [tf :: {K} -> Type]
          (f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                tf r -> tf ([nm = v] ++ r)))
-         (i : tf []) [r :: {K}] (fl : folder r) = fl [tf] f i
+         (i : tf []) [r ::: {K}] (fl : folder r) = fl [tf] f i
 
 structure Folder = struct
     fun nil [K] [tf :: {K} -> Type]
@@ -92,27 +92,27 @@ fun read_option [t ::: Type] (_ : read t) =
 fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) =
     cdata (show v)
 
-fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r :: {K}] (fl : folder r) =
+fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc =>
         acc ++ {nm = f [t]})
     {}
 
-fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r :: {K}] (fl : folder r) =
+fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
         acc (r -- nm) ++ {nm = f r.nm})
     (fn _ => {})
 
 fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
-         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r :: {K}] (fl : folder r) =
+         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
         acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
     (fn _ _ => {})
 
 fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
-         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r :: {K}] (fl : folder r) =
+         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
         acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
@@ -122,7 +122,7 @@ fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf -> tr rest -> tr ([nm] ++ rest))
-           (i : tr []) [r :: {Unit}] (fl : folder r) =
+           (i : tr []) [r ::: {Unit}] (fl : folder r) =
     fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
        (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
            f [nm] [rest] ! r.nm (acc (r -- nm)))
@@ -132,7 +132,7 @@ fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type]
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
-           (i : tr []) [r :: {Unit}] (fl : folder r) =
+           (i : tr []) [r ::: {Unit}] (fl : folder r) =
     fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
        (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
            f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
@@ -142,16 +142,16 @@ fun foldURX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf1 -> tf2 -> xml ctx [] []) =
-    foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
-            (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
-                <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
-            <xml/>
+    @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
+          <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
+      <xml/>
 
 fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
                       tf t -> tr rest -> tr ([nm = t] ++ rest))
-           (i : tr []) [r :: {K}] (fl : folder r) =
+           (i : tr []) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf r) -> tr r]
        (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
            f [nm] [t] [rest] ! r.nm (acc (r -- nm)))
@@ -161,7 +161,7 @@ fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
             (f : nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) [r :: {K}] (fl : folder r) =
+            (i : tr []) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
        (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
                         (acc : _ -> _ -> tr rest) r1 r2 =>
@@ -172,7 +172,7 @@ fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {
             (f : nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) [r :: {K}] (fl : folder r) =
+            (i : tr []) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
        (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
                         (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
@@ -183,30 +183,30 @@ fun foldRX [K] [tf :: K -> Type] [ctx :: {Unit}]
             (f : nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf t -> xml ctx [] []) =
-    foldR [tf] [fn _ => xml ctx [] []]
-          (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
-              <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
-          <xml/>
+    @@foldR [tf] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
+          <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
+      <xml/>
 
 fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
              (f : nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> xml ctx [] []) =
-    foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
-           (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
-                            r1 r2 acc =>
-               <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
-           <xml/>
+    @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+                       r1 r2 acc =>
+          <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
+      <xml/>
 
 fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
              (f : nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
-    foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
-           (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
-                            r1 r2 r3 acc =>
-               <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
-           <xml/>
+    @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+                       r1 r2 r3 acc =>
+          <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
+      <xml/>
 
 fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) =
     query q
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 11547ace..d23b3e01 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -6,7 +6,7 @@ val fold : K --> tf :: ({K} -> Type)
            -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                tf r -> tf ([nm = v] ++ r))
            -> tf []
-           -> r :: {K} -> folder r -> tf r
+           -> r ::: {K} -> folder r -> tf r
 
 structure Folder : sig
     val nil : K --> folder (([]) :: {K})
@@ -47,40 +47,40 @@ val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
 
 val map0 : K --> tf :: (K -> Type)
            -> (t :: K -> tf t)
-           -> r :: {K} -> folder r -> $(map tf r)
+           -> r ::: {K} -> folder r -> $(map tf r)
 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
          -> (t ::: K -> tf1 t -> tf2 t)
-         -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
+         -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
            -> (t ::: K -> tf1 t -> tf2 t -> tf t)
-           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
+           -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
            -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
-           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
+           -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
 
 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}
                  -> [[nm] ~ rest] =>
                        tf -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf r) -> tr r
+             -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r
 
 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}
                  -> [[nm] ~ rest] =>
                        tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
+             -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
 
 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
               -> (nm :: Name -> rest :: {Unit}
                   -> [[nm] ~ rest] =>
                         tf1 -> tf2 -> xml ctx [] [])
-              -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
+              -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
 
 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
              -> (nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf t -> tr rest -> tr ([nm = t] ++ rest))
-             -> tr [] -> r :: {K} -> folder r -> $(map tf r) -> tr r
+             -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
 
 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
              -> tr :: ({K} -> Type)
@@ -88,7 +88,7 @@ val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
 
 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
              -> tr :: ({K} -> Type)
@@ -96,26 +96,26 @@ val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
 
 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
              -> (nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf t -> xml ctx [] [])
-             -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] []
+             -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
 
 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
               -> (nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> xml ctx [] [])
-              -> r :: {K} -> folder r
+              -> r ::: {K} -> folder r
               -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
 
 val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
               -> (nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
-              -> r :: {K} -> folder r
+              -> r ::: {K} -> folder r
               -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
 
 val queryL : tables ::: {{Type}} -> exps ::: {Type}