fix propagation of size constraints

detail/semantic/inference.sml

@@ -58,11 +58,11 @@ end = struct
             let
                val (eStr,si) = E.kappaToStringSI (env,si)
             in
-               (acc ^ "\n\t" ^ str ^ ": " ^ eStr,si)
+               (acc ^ "\t" ^ str ^ ": " ^ eStr,si)
             end
          val (str, si) = List.foldl
                            genRow
-                           (str ^ msg, TVar.emptyShowInfo) envStrs
+                           (str ^ msg ^ "\n", TVar.emptyShowInfo) envStrs
       in
          raise S.UnificationFailure str
       end
@@ -416,7 +416,11 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
             handle S.UnificationFailure str =>
                refineError (str,
                             " while passing",
-                            List.map (fn e2 => (envArg, "argument    " ^ showProg (20, PP.exp, e2))) es2 @
+                            (#1 (List.foldr
+                            (fn (e2,(res,env)) => 
+                              ((env, "argument    " ^ showProg (20, PP.exp, e2))::res,
+                               E.popKappa env)
+                            ) ([], envArg) es2)) @
                             [(envFun, "to function " ^ showProg (20, PP.exp, e1))])
          (*val _ = TextIO.print ("**** app fun,res unified:\n" ^ E.topToString env)*)
          val env = E.reduceToResult env

detail/semantic/typing/environment.sml

@@ -1298,6 +1298,12 @@ end = struct
          val env1 = (scs,cons)*)
       
          val (env1,env2) = mergeUses (env1, env2)
+
+         val (_, state1) = env1
+         val (_, state2) = env2
+         val sCons = SC.merge (Scope.getSize state1,Scope.getSize state2)
+         val (sCons, substs) = applySizeConstraints (sCons, substs)
+
          val (ei, bFunFlow, env) =
             applySubsts (substs, emptyExpandInfo, BD.empty, directed, env1, env2)
          
@@ -1306,8 +1312,6 @@ end = struct
          val (sStr,si) = showSubstsSI (substs,si)
          val kind = if directed then "directed" else "equalizing"
          val _ = TextIO.print ("**** meet " ^ kind ^ ":\n" ^ e1Str' ^ "++++ intersected with\n" ^ e2Str')*)
-         val (_, state1) = env1
-         val (_, state2) = env2
 
          val bVars1 = Scope.getBVars env1
          val bVars2 = Scope.getBVars env2
@@ -1318,8 +1322,6 @@ end = struct
                               "\nand\n" ^ BD.showBFun (Scope.getFlow state2) ^ 
                               "\nis\n" ^ BD.showBFun bFun ^ "\n")*)
 
-         val sCons = SC.merge (Scope.getSize state1,Scope.getSize state2)
-         val (sCons, substs) = applySizeConstraints (sCons, substs)
 
          val bFun = BD.projectOnto (bVars, bFun)
          val bFun = applyExpandInfo ei bFun

detail/semantic/typing/size-constraint.sml

@@ -152,7 +152,7 @@ end = struct
                       (str ^ " " ^ vStr ^ "=" ^ Int.toString(f), si)
                    end) ("", si) is
               in
-                 "result : " ^ scsStr ^ " and " ^ vsStr ^ "instantiated\n"
+                 "result : " ^ scsStr ^ " and" ^ vsStr ^ " instantiated\n"
               end
             | UNSATISFIABLE => "unsatisfiabilitiy"
             | FRACTIONAL => "non-integrality"
@@ -189,15 +189,18 @@ end = struct
       
    fun merge (scs1, scs2) =
       let
-         (*val (sStr1, si) = toStringSI (scs1, NONE, TVar.emptyShowInfo)
-         val (sStr2, si) = toStringSI (scs2, NONE, si)
-         val _ = TextIO.print ("merging " ^ sStr1 ^ " with " ^ sStr2 ^ "\n")*)
          fun m ([], scs) = scs
            | m (eq :: eqs, scs) = case add (eq, scs) of
                 RESULT (_, scs) => m (eqs, scs)
               | _ => raise SizeConstraintBug
+         val scs = m (scs1, scs2)
+         (*val (sStr1, si) = toStringSI (scs1, NONE, TVar.emptyShowInfo)
+         val (sStr2, si) = toStringSI (scs2, NONE, si)
+         val (sStr3, si) = toStringSI (scs, NONE, si)
+         val _ = TextIO.print ("merging " ^ sStr1 ^ " with " ^ sStr2 ^ 
+                               " resulting in " ^ sStr3 ^ "\n")*)
       in
-         m (scs1, scs2)
+         scs
       end
 
    fun rename (v1,v2,scs) =

detail/semantic/typing/substitutions.sml

@@ -381,10 +381,12 @@ end = struct
       let
          val vs = SC.getVarset sCons
          val (Substs ss) = substsFilter (substs, vs)
+
          fun updateSubsts ((v,WITH_TYPE (CONST c)), (sCons, substs)) =
             (case SC.add (SC.equality (v,[],c), sCons) of
                 SC.RESULT (is,sCons) =>
-                  (sCons, List.foldl (fn ((v,c), substs) =>
+                  (sCons,
+                   List.foldl (fn ((v,c), substs) =>
                      #1 (addSubst (v,WITH_TYPE (CONST c)) (substs, emptyExpandInfo))
                      ) substs is)
                | SC.UNSATISFIABLE => raise UnificationFailure
@@ -397,6 +399,7 @@ end = struct
            | updateSubsts ((v1,WITH_TYPE (VAR (v2,_))), (sCons, substs)) =
                (SC.rename (v1,v2,sCons), substs)
            | updateSubsts _ = raise SubstitutionBug
+
       in
          List.foldl updateSubsts (sCons, substs) ss
       end

detail/semantic/typing/tvar.sml

@@ -48,13 +48,13 @@ end = struct
    fun name idx = (if idx>25 then name (Int.div (idx,26)-1) else "") ^
         Char.toString (Char.chr (Char.ord #"a"+Int.mod (idx,26)))
 
-   fun varToString (TVAR var, tab) = (*(name var, tab)*) case VarMap.find (tab, var) of
-                                  SOME str => (str, tab)
-                                | NONE => let
-                                     val str = name (VarMap.numItems(tab))
-                                  in
-                                     (str, VarMap.insert(tab, var, str))
-                                  end                              
+   fun varToString (TVAR var, tab) = (name var, tab) (*case VarMap.find (tab, var) of
+                                     SOME str => (str, tab)
+                                   | NONE => let
+                                        val str = name (VarMap.numItems(tab))
+                                     in
+                                        (str, VarMap.insert(tab, var, str))
+                                     end                *)              
 
    structure IntSet = SplaySetFn(struct
       type ord_key = int