# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1216932527 14400
# Node ID 870e8abbe3b99cdfa2bec678f15a398321357602
# Parent  1e382d10e8324e818abaf313eb9d1ee5eb446e24
Datatype import signature-matches abstract datatype

diff -r 1e382d10e832 -r 870e8abbe3b9 src/elaborate.sml
--- a/src/elaborate.sml	Thu Jul 24 16:41:12 2008 -0400
+++ b/src/elaborate.sml	Thu Jul 24 16:48:47 2008 -0400
@@ -1751,44 +1751,57 @@
 
                       | L'.SgiDatatype (x, n2, xncs2) =>
                         seek (fn sgi1All as (sgi1, _) =>
-                                 case sgi1 of
-                                     L'.SgiDatatype (x', n1, xncs1) =>
-                                     let
-                                         fun mismatched ue =
-                                             (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
-                                              SOME (env, denv))
+                                 let
+                                     fun found (n1, xncs1) =
+                                         let
+                                             fun mismatched ue =
+                                                 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
+                                                  SOME (env, denv))
 
-                                         fun good () =
-                                             let
-                                                 val env = E.sgiBinds env sgi2All
-                                                 val env = if n1 = n2 then
-                                                               env
-                                                           else
-                                                               E.pushCNamedAs env x n1 (L'.KType, loc)
-                                                                              (SOME (L'.CNamed n1, loc))
-                                             in
-                                                 SOME (env, denv)
-                                             end
+                                             fun good () =
+                                                 let
+                                                     val env = E.sgiBinds env sgi2All
+                                                     val env = if n1 = n2 then
+                                                                   env
+                                                               else
+                                                                   E.pushCNamedAs env x n1 (L'.KType, loc)
+                                                                                  (SOME (L'.CNamed n1, loc))
+                                                 in
+                                                     SOME (env, denv)
+                                                 end
 
-                                         fun xncBad ((x1, _, t1), (x2, _, t2)) =
-                                             String.compare (x1, x2) <> EQUAL
-                                             orelse case (t1, t2) of
-                                                        (NONE, NONE) => false
-                                                      | (SOME t1, SOME t2) =>
-                                                        not (List.null (unifyCons (env, denv) t1 t2))
-                                                      | _ => true
-                                     in
-                                         (if x = x' then
-                                             if length xncs1 <> length xncs2
-                                                orelse ListPair.exists xncBad (xncs1, xncs2) then
-                                                 mismatched NONE
-                                             else
-                                                 good ()
-                                          else
-                                              NONE)
-                                         handle CUnify ue => mismatched (SOME ue)
-                                     end
-                                   | _ => NONE)
+                                             fun xncBad ((x1, _, t1), (x2, _, t2)) =
+                                                 String.compare (x1, x2) <> EQUAL
+                                                 orelse case (t1, t2) of
+                                                            (NONE, NONE) => false
+                                                          | (SOME t1, SOME t2) =>
+                                                            not (List.null (unifyCons (env, denv) t1 t2))
+                                                          | _ => true
+                                         in
+                                             (if length xncs1 <> length xncs2
+                                                 orelse ListPair.exists xncBad (xncs1, xncs2) then
+                                                  mismatched NONE
+                                              else
+                                                  good ())
+                                             handle CUnify ue => mismatched (SOME ue)
+                                         end
+                                 in
+                                     case sgi1 of
+                                         L'.SgiDatatype (x', n1, xncs1) =>
+                                         if x' = x then
+                                             found (n1, xncs1)
+                                         else
+                                             NONE
+                                       | L'.SgiDatatypeImp (x', n1, m1, ms, s) =>
+                                         let
+                                             val (str, sgn) = E.chaseMpath env (m1, ms)
+                                         in
+                                             case E.projectDatatype env {str = str, sgn = sgn, field = s} of
+                                                 NONE => NONE
+                                               | SOME xncs1 => found (n1, xncs1)
+                                         end
+                                       | _ => NONE
+                                 end)
 
                       | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) =>
                         seek (fn sgi1All as (sgi1, _) =>
diff -r 1e382d10e832 -r 870e8abbe3b9 tests/datatypeMod.lac
--- a/tests/datatypeMod.lac	Thu Jul 24 16:41:12 2008 -0400
+++ b/tests/datatypeMod.lac	Thu Jul 24 16:48:47 2008 -0400
@@ -16,3 +16,5 @@
 val b : M3.t = M4.B
 
 structure Ma : sig type t end = M
+
+structure Magain : sig datatype t = A | B end = M