Fix type class resolution infinite loop, discovered while meeting with Ezra

5 files changed, 58 insertions, 7 deletions

diff --git a/src/elab_env.sml b/src/elab_env.sml
index c7dfc0b1..1bd4e059 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -500,6 +500,47 @@ fun unifyKinds (k1, k2) =
       | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
       | _ => raise Unify
 
+fun eqCons (c1, c2) =
+    case (#1 c1, #1 c2) of
+        (CUnif (_, _, _, ref (SOME c1)), _) => eqCons (c1, c2)
+      | (_, CUnif (_, _, _, ref (SOME c2))) => eqCons (c1, c2)
+
+      | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
+
+      | (TFun (d1, r1), TFun (d2, r2)) => (eqCons (d1, d2); eqCons (r1, r2))
+      | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); eqCons (r1, r2))
+      | (TRecord c1, TRecord c2) => eqCons (c1, c2)
+      | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
+        (eqCons (a1, a2); eqCons (b1, b2); eqCons (c1, c2))
+
+      | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
+      | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
+        if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
+      | (CApp (f1, x1), CApp (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2))
+      | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); eqCons (b1, b2))
+
+      | (CKAbs (_, b1), CKAbs (_, b2)) => eqCons (b1, b2)
+      | (CKApp (c1, k1), CKApp (c2, k2)) => (eqCons (c1, c2); unifyKinds (k1, k2))
+      | (TKFun (_, c1), TKFun (_, c2)) => eqCons (c1, c2)
+
+      | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
+
+      | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
+        (unifyKinds (k1, k2);
+         ListPair.appEq (fn ((x1, c1), (x2, c2)) => (eqCons (x1, x2); eqCons (c1, c2))) (xcs1, xcs2)
+         handle ListPair.UnequalLengths => raise Unify)
+      | (CConcat (f1, x1), CConcat (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2))
+      | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
+
+      | (CUnit, CUnit) => ()
+
+      | (CTuple cs1, CTuple cs2) => (ListPair.appEq (eqCons) (cs1, cs2)
+                                     handle ListPair.UnequalLengths => raise Unify)
+      | (CProj (c1, n1), CProj (c2, n2)) => (eqCons (c1, c2);
+                                             if n1 = n2 then () else raise Unify)
+
+      | _ => raise Unify
+
 fun unifyCons rs =
     let
         fun unify d (c1, c2) =
@@ -524,7 +565,7 @@ fun unifyCons rs =
                     in
                         case !r of
                             NONE => r := SOME c1
-                          | SOME c2 => unify d (c1, c2)
+                          | SOME c2 => eqCons (c1, c2)
                     end
 
               | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2))
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 6b25cedb..0a15dab1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3175,7 +3175,7 @@ and wildifyStr env (str, sgn) =
 
 and elabDecl (dAll as (d, loc), (env, denv, gs)) =
     let
-        (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
+        (*val () = preface ("elabDecl", SourcePrint.p_decl dAll)*)
         (*val befor = Time.now ()*)
 
         val r = 
@@ -3410,7 +3410,6 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                              L'.StrFun _ => ()
                            | _ => strError env (FunctorRebind loc))
                       | _ => ();
-
                     ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv', gs' @ gs))
                 end
 
@@ -3620,10 +3619,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
 
         (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
     in
-        (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
-                             ("t", PD.string (LargeReal.toString (Time.toReal
-                                                                      (Time.- (Time.now (), befor)))))];*)
-
+        (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll)];*)
         r
     end
 
diff --git a/tests/filter.ur b/tests/filter.ur
new file mode 100644
index 00000000..efd326c3
--- /dev/null
+++ b/tests/filter.ur
@@ -0,0 +1,9 @@
+fun filter [fs ::: {Type}] [ks] (t : sql_table fs ks) (p : sql_exp [T = fs] [] [] bool)
+   : sql_query [T = fs] [] =
+   (SELECT * FROM t WHERE {p})
+
+table t : { A : int, B : float }
+
+fun main () =
+    queryX (filter t (WHERE t.A > 3))
+           (fn r => <xml>{[r.T.A]}, {[r.T.B]}</xml>)
diff --git a/tests/filter.urp b/tests/filter.urp
new file mode 100644
index 00000000..102a1871
--- /dev/null
+++ b/tests/filter.urp
@@ -0,0 +1,4 @@
+debug
+database dbname=filter
+
+filter
diff --git a/tests/filter.urs b/tests/filter.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/tests/filter.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page