Fun with type classes and modules

2 files changed, 38 insertions, 18 deletions

diff --git a/src/elab_env.sml b/src/elab_env.sml
index 1b25749f..392fcf02 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -713,7 +713,11 @@ fun enrichClasses env classes (m1, ms) sgn =
                               fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap))
                           in
                               case #1 sgi of
-                                  SgiClassAbs xn => found xn
+                                  SgiStr (x, _, sgn) =>
+                                  (enrichClasses env classes (m1, ms @ [x]) sgn,
+                                   newClasses,
+                                   sgiSeek (#1 sgi, fmap))
+                                | SgiClassAbs xn => found xn
                                 | SgiClass (x, n, _) => found (x, n)
                                 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
                                   (case IM.find (newClasses, f) of
@@ -735,6 +739,7 @@ fun enrichClasses env classes (m1, ms) sgn =
                                                 newClasses,
                                                 fmap)
                                            end)
+                                | SgiVal _ => default ()
                                 | _ => default ()
                           end)
                 (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2046432b..ebd46eca 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1373,20 +1373,33 @@ fun exhaustive (env, denv, t, ps) =
         isTotal (combinedCoverage ps, t)
     end
 
-fun normClassConstraint envs c =
-    let
-        val ((c, loc), gs1) = hnormCon envs c
-    in
-        case c of
-            L'.CApp (f, x) =>
-            let
-                val (f, gs2) = hnormCon envs f
-                val (x, gs3) = hnormCon envs x
-            in
-                ((L'.CApp (f, x), loc), gs1 @ gs2 @ gs3)
-            end
-          | _ => ((c, loc), gs1)
-    end
+fun unmodCon env (c, loc) =
+    case c of
+        L'.CNamed n =>
+        (case E.lookupCNamed env n of
+             (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c
+           | _ => (c, loc))
+      | L'.CModProj (m1, ms, x) =>
+        let
+            val (str, sgn) = E.chaseMpath env (m1, ms)
+        in
+            case E.projectCon env {str = str, sgn = sgn, field = x} of
+                NONE => raise Fail "unmodCon: Can't projectCon"
+              | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
+              | _ => (c, loc)
+        end
+      | _ => (c, loc)
+
+fun normClassConstraint envs (c, loc) =
+    case c of
+        L'.CApp (f, x) =>
+        let
+            val f = unmodCon (#1 envs) f
+            val (x, gs) = hnormCon envs x
+        in
+            ((L'.CApp (f, x), loc), gs)
+        end
+      | _ => ((c, loc), [])
 
 fun elabExp (env, denv) (eAll as (e, loc)) =
     let
@@ -2728,11 +2741,13 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                                   | SOME c => elabCon (env, denv) c
 
             val (e', et, gs2) = elabExp (env, denv) e
-            val (env', n) = E.pushENamed env x c'
-
             val gs3 = checkCon (env, denv) e' et c'
+            val (c', gs4) = normClassConstraint (env, denv) c'
+            val (env', n) = E.pushENamed env x c'
         in
-            ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
+            (*prefaces "DVal" [("x", Print.PD.string x),
+                             ("c'", p_con env c')];*)
+            ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs4 @ gs))
         end
       | L.DValRec vis =>
         let