From 4dce690086c8d6132c22d5c47a0561a4b1261293 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 16 Jun 2009 14:38:01 -0400
Subject: Fix a bug in type class enrichment from substructures

---
 src/elab_env.sml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'src/elab_env.sml')

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,
-- 
cgit v1.2.3