Signature ascription for type classes

3 files changed, 53 insertions, 12 deletions

diff --git a/src/elab_env.sml b/src/elab_env.sml
index 392fcf02..49eb1d86 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -700,23 +700,31 @@ fun enrichClasses env classes (m1, ms) sgn =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         let
-            val (classes, _, _) =
-                foldl (fn (sgi, (classes, newClasses, fmap)) =>
+            val (classes, _, _, _) =
+                foldl (fn (sgi, (classes, newClasses, fmap, env)) =>
                           let
                               fun found (x, n) =
                                   (CM.insert (classes,
                                               ClProj (m1, ms, x),
                                               empty_class),
                                    IM.insert (newClasses, n, x),
-                                   sgiSeek (#1 sgi, fmap))
+                                   sgiSeek (#1 sgi, fmap),
+                                   env)
 
-                              fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap))
+                              fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
                           in
                               case #1 sgi of
                                   SgiStr (x, _, sgn) =>
                                   (enrichClasses env classes (m1, ms @ [x]) sgn,
                                    newClasses,
-                                   sgiSeek (#1 sgi, fmap))
+                                   sgiSeek (#1 sgi, fmap),
+                                   env)
+                                | SgiSgn (x, n, sgn) =>
+                                  (classes,
+                                   newClasses,
+                                   fmap,
+                                   pushSgnNamedAs env x n sgn)
+
                                 | SgiClassAbs xn => found xn
                                 | SgiClass (x, n, _) => found (x, n)
                                 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
@@ -737,12 +745,13 @@ fun enrichClasses env classes (m1, ms) sgn =
                                            in
                                                (CM.insert (classes, cn, class),
                                                 newClasses,
-                                                fmap)
+                                                fmap,
+                                                env)
                                            end)
                                 | SgiVal _ => default ()
                                 | _ => default ()
                           end)
-                (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis
+                      (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
         in
             classes
         end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index ebd46eca..dc630e0e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1913,11 +1913,12 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             val (c', ck, gs') = elabCon (env, denv) c
 
             val (env', n) = E.pushENamed env x c'
+            val (c', gs'') = normClassConstraint (env, denv) c'
         in
             (unifyKinds ck ktype
              handle KUnify ue => strError env (NotType (ck, ue)));
 
-            ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
+            ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs))
         end
 
       | L.SgiStr (x, sgn) =>
@@ -2137,6 +2138,8 @@ fun selfify env {str, strs, sgn} =
                               (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
                             | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
                               (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
+                            | (L'.SgiClassAbs (x, n), loc) =>
+                              (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc)
                             | (L'.SgiStr (x, n, sgn), loc) =>
                               (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
                             | x => x) sgis), #2 sgn)
@@ -2339,9 +2342,9 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                              found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
                                          end
                                        | L'.SgiClassAbs (x', n1) => found (x', n1,
-                                                                        (L'.KArrow ((L'.KType, loc),
-                                                                                    (L'.KType, loc)), loc),
-                                                                        NONE)
+                                                                           (L'.KArrow ((L'.KType, loc),
+                                                                                       (L'.KType, loc)), loc),
+                                                                           NONE)
                                        | L'.SgiClass (x', n1, c) => found (x', n1,
                                                                            (L'.KArrow ((L'.KType, loc),
                                                                                        (L'.KType, loc)), loc),
@@ -2592,7 +2595,16 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                      fun found (x', n1, c1) =
                                          if x = x' then
                                              let
-                                                 fun good () = SOME (E.pushCNamedAs env x n2 k (SOME c2), denv)
+                                                 fun good () =
+                                                     let
+                                                         val env = E.pushCNamedAs env x n2 k (SOME c2)
+                                                         val env = if n1 = n2 then
+                                                                       env
+                                                                   else
+                                                                       E.pushCNamedAs env x n1 k (SOME c1)
+                                                     in
+                                                         SOME (env, denv)
+                                                     end
                                              in
                                                  (case unifyCons (env, denv) c1 c2 of
                                                       [] => good ()
@@ -2823,6 +2835,8 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                                                                 case d of
                                                                     L.DCon (x, _, _) => (SS.delete (needed, x)
                                                                                          handle NotFound => needed)
+                                                                  | L.DClass (x, _) => (SS.delete (needed, x)
+                                                                                        handle NotFound => needed)
                                                                   | L.DOpen _ => SS.empty
                                                                   | _ => needed)
                                                             needed ds
diff --git a/tests/type_classMod2.lac b/tests/type_classMod2.lac
new file mode 100644
index 00000000..ba700c22
--- /dev/null
+++ b/tests/type_classMod2.lac
@@ -0,0 +1,18 @@
+signature S = sig
+        class c
+        val default : t :: Type -> c t -> t
+
+        val string_c : c string
+        val int_c : c int
+end
+
+structure M : S = struct
+        class c t = t
+        val default = fn t :: Type => fn v : c t => v
+
+        val int_c : c int = 0
+        val string_c : c string = "Hi"
+end
+
+val hi = M.default [string] _
+val zero = M.default [int] _