# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1448656092 18000
# Node ID 100352dbae3676d2ede67a9c809b4f7da18b4657
# Parent  18e6fb487880fde89c537089d0df537cc5f69bc2
Fix tricky case of functor signature subsumption

diff -r 18e6fb487880 -r 100352dbae36 src/elab_env.sig
--- a/src/elab_env.sig	Wed Nov 25 18:48:17 2015 -0500
+++ b/src/elab_env.sig	Fri Nov 27 15:28:12 2015 -0500
@@ -37,6 +37,8 @@
 
     type env
 
+    val dump : env -> unit
+
     val empty : env
 
     exception UnboundRel of int
diff -r 18e6fb487880 -r 100352dbae36 src/elab_env.sml
--- a/src/elab_env.sml	Wed Nov 25 18:48:17 2015 -0500
+++ b/src/elab_env.sml	Fri Nov 27 15:28:12 2015 -0500
@@ -239,6 +239,10 @@
      str : (string * sgn) IM.map
 }
 
+fun dump (env : env) =
+    (print "NamedC:\n";
+     IM.appi (fn (n, (x, k, co)) => print (x ^ " [" ^ Int.toString n ^ "]\n")) (#namedC env))
+
 val namedCounter = ref 0
 
 fun newNamed () =
diff -r 18e6fb487880 -r 100352dbae36 src/elaborate.sml
--- a/src/elaborate.sml	Wed Nov 25 18:48:17 2015 -0500
+++ b/src/elaborate.sml	Fri Nov 27 15:28:12 2015 -0500
@@ -1359,7 +1359,9 @@
      end
 
  and unifyCons env loc c1 c2 =
-     unifyCons' env loc c1 c2
+     ((*Print.prefaces "uc" [("c1", p_con env c1),
+                           ("c2", p_con env c2)];*)
+     unifyCons' env loc c1 c2)
      handle CUnify' (env', err) => raise CUnify (c1, c2, env', err)
           | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg)
 
@@ -3079,6 +3081,8 @@
 
             fun cpart n = IM.find (!counterparts, n)
             fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1)
+            fun uncparts n2 = (counterparts := #1 (IM.remove (!counterparts, n2)))
+                              handle NotFound => ()
 
             val sub2 = U.Con.map {kind = fn k => k,
                                   con = fn c =>
@@ -3107,7 +3111,8 @@
                                                           if E.checkENamed env n then
                                                               env
                                                           else
-                                                              E.pushCNamedAs env x n k (SOME c)
+                                                              (uncparts n;
+                                                               E.pushCNamedAs env x n k (SOME c))
                                                         | L'.SgiConAbs (x, n, k) =>
                                                           if E.checkENamed env n then
                                                               env
diff -r 18e6fb487880 -r 100352dbae36 tests/subfunctor.ur
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/subfunctor.ur	Fri Nov 27 15:28:12 2015 -0500
@@ -0,0 +1,6 @@
+functor F(M : sig con fs :: {Type} end) = struct
+    open M
+
+    functor G(M : sig val x : $(map sql_injectable_prim fs) end) = struct
+    end
+end
diff -r 18e6fb487880 -r 100352dbae36 tests/subfunctor.urs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/subfunctor.urs	Fri Nov 27 15:28:12 2015 -0500
@@ -0,0 +1,3 @@
+functor F(M : sig con fs :: {Type} end) : sig
+    functor G(M : sig val x : $(map sql_injectable_prim M.fs) end) : sig end
+end