Fixed a mind-numbing De Bruijn bug

4 files changed, 27 insertions, 7 deletions

diff --git a/lib/top.ur b/lib/top.ur
index 16d2ed42..ec0e58af 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -4,3 +4,13 @@ con mapTT (f :: Type -> Type) = fold (fn nm t acc => [nm] ~ acc =>
 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
 
 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v)
+
+fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
+        (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
+                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+        (i : tr []) =
+        fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
+                (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
+                        [[nm] ~ rest] =>
+                        fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+                (fn _ _ => i)
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 1b9de129..6c3d7802 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -241,7 +241,8 @@ fun pushCRel (env : env) x k =
                           })
                           (#classes env),
 
-         renameE = #renameE env,
+         renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
+                            | Named' (n, c) => Named' (n, lift c)) (#renameE env),
          relE = map (fn (x, c) => (x, lift c)) (#relE env),
          namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
 
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 6c75768b..3cdc37c1 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -92,10 +92,10 @@ fun hnormCon env (cAll as (c, loc)) =
                      handle SynUnif => cAll
                  (*val env' = E.pushCRel env x k*)
              in
-                 (*eprefaces "Subst" [("x", Print.PD.string x),
-                                    ("cb", p_con env' cb),
-                                    ("c2", p_con env c2),
-                                    ("sc", p_con env sc)];*)
+                 (*Print.eprefaces "Subst" [("x", Print.PD.string x),
+                                          ("cb", ElabPrint.p_con env' cb),
+                                          ("c2", ElabPrint.p_con env c2),
+                                          ("sc", ElabPrint.p_con env sc)];*)
                  sc
              end
            | c1' as CApp (c', i) =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 223c10e6..7e4ff670 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1609,19 +1609,26 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
           | L.ECApp (e, c) =>
             let
                 val (e', et, gs1) = elabExp (env, denv) e
+                val oldEt = et
                 val (e', et, gs2) = elabHead (env, denv) e' et
                 val (c', ck, gs3) = elabCon (env, denv) c
                 val ((et', _), gs4) = hnormCon (env, denv) et
             in
                 case et' of
                     L'.CError => (eerror, cerror, [])
-                  | L'.TCFun (_, _, k, eb) =>
+                  | L'.TCFun (_, x, k, eb) =>
                     let
                         val () = checkKind env c' ck k
                         val eb' = subConInCon (0, c') eb
                             handle SynUnif => (expError env (Unif ("substitution", eb));
                                                cerror)
                     in
+                        (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
+                                               ("et", p_con env oldEt),
+                                               ("x", PD.string x),
+                                               ("eb", p_con (E.pushCRel env x k) eb),
+                                               ("c", p_con env c'),
+                                               ("eb'", p_con env eb')];*)
                         ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
                     end
 
@@ -1637,7 +1644,9 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
             let
                 val expl' = elabExplicitness expl
                 val k' = elabKind k
-                val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
+
+                val env' = E.pushCRel env x k'
+                val (e', et, gs) = elabExp (env', D.enter denv) e
             in
                 ((L'.ECAbs (expl', x, k', e'), loc),
                  (L'.TCFun (expl', x, k', et), loc),