Fix a bug in type class enrichment from substructures

5 files changed, 48 insertions, 7 deletions

diff --git a/src/elab_env.sml b/src/elab_env.sml
index 2296d819..c7dfc0b1 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1070,6 +1070,9 @@ and hnormSgn env (all as (sgn, loc)) =
             end
           | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
 
+fun manifest (m, ms, loc) =
+    foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms
+
 fun enrichClasses env classes (m1, ms) sgn =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
@@ -1089,10 +1092,15 @@ fun enrichClasses env classes (m1, ms) sgn =
                           in
                               case #1 sgi of
                                   SgiStr (x, _, sgn) =>
-                                  (enrichClasses env classes (m1, ms @ [x]) sgn,
-                                   newClasses,
-                                   sgiSeek (#1 sgi, fmap),
-                                   env)
+                                  let
+                                      val str = manifest (m1, ms, #2 sgi)
+                                      val sgn' = sgnSubSgn (str, fmap) sgn
+                                  in
+                                      (enrichClasses env classes (m1, ms @ [x]) sgn',
+                                       newClasses,
+                                       sgiSeek (#1 sgi, fmap),
+                                       env)
+                                  end
                                 | SgiSgn (x, n, sgn) =>
                                   (classes,
                                    newClasses,
diff --git a/src/elab_err.sml b/src/elab_err.sml
index dc34560b..f6fec25b 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -218,7 +218,7 @@ fun expError env err =
                                               ("Type", p_con env c)]) co)
       | Unresolvable (loc, c) =>
         (ErrorMsg.errorAt loc "Can't resolve type class instance";
-         eprefaces' [("Class constraint", p_con env c)(*,
+         eprefaces' [("Class constraint", p_con env c),
                      ("Class database", p_list (fn (c, rules) =>
                                                    box [P.p_con env c,
                                                         PD.string ":",
@@ -228,7 +228,7 @@ fun expError env err =
                                                                         PD.string ":",
                                                                         space,
                                                                         P.p_con env c]) rules])
-                                        (E.listClasses env))*)])
+                                        (E.listClasses env))])
       | IllegalRec (x, e) =>
         (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
          eprefaces' [("Variable", PD.string x),
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e78132c4..f0aa8d7a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -696,7 +696,6 @@
 
  and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
      let
-         val loc = #2 k
          (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)),
                                            ("#1", p_summary env s1),
                                            ("#2", p_summary env s2)]*)
diff --git a/src/list_util.sig b/src/list_util.sig
index a89998b2..6e1cd5a5 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -36,6 +36,8 @@ signature LIST_UTIL = sig
 
     val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
     val foldlMapPartial : ('data1 * 'state -> 'data2 option * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
+    val foldlMapiPartial : (int * 'data1 * 'state -> 'data2 option * 'state)
+                           -> 'state -> 'data1 list -> 'data2 list * 'state
     val foldlMapConcat : ('data1 * 'state -> 'data2 list * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
     val foldlMapAbort : ('data1 * 'state -> ('data2 * 'state) option)
                         -> 'state -> 'data1 list -> ('data2 list * 'state) option
@@ -44,6 +46,7 @@ signature LIST_UTIL = sig
     val searchi : (int * 'a -> 'b option) -> 'a list -> 'b option
 
     val mapi : (int * 'a -> 'b) -> 'a list -> 'b list
+    val mapiPartial : (int * 'a -> 'b option) -> 'a list -> 'b list
     val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b
     val foldri : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b
 
diff --git a/src/list_util.sml b/src/list_util.sml
index 1f6b24ee..03c9549e 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -123,6 +123,24 @@ fun foldlMapPartial f s =
         fm ([], s)
     end
 
+fun foldlMapiPartial f s =
+    let
+        fun fm (n, ls', s) ls =
+            case ls of
+                nil => (rev ls', s)
+              | h :: t =>
+                let
+                    val (h', s') = f (n, h, s)
+                    val ls' = case h' of
+                                  NONE => ls'
+                                | SOME h' => h' :: ls'
+                in
+                    fm (n + 1, ls', s') t
+                end
+    in
+        fm (0, [], s)
+    end
+
 fun foldlMapAbort f s =
     let
         fun fm (ls', s) ls =
@@ -172,6 +190,19 @@ fun mapi f =
         m 0 []
     end
 
+fun mapiPartial f =
+    let
+        fun m i acc ls =
+            case ls of
+                [] => rev acc
+              | h :: t =>
+                m (i + 1) (case f (i, h) of
+                               NONE => acc
+                             | SOME v => v :: acc) t
+    in
+        m 0 []
+    end
+
 fun appi f =
     let
         fun m i ls =