[MLton-commit] r7434

Matthew Fluet fluet at mlton.org
Fri Mar 12 13:33:07 PST 2010


Fix bug with type checking of datatype declarations with withtype bindings.

The type checking and elaboration of datatype declarations had been
implemented by repeatedly elaborating the withtype bindings (in the
scope of the datatype type constructors) followed by the datatype
bindings (constructors) until the equality status of the datatype
tycons stabilized.

This implementation, however, has a problem with the following:
  type u = real ;
  datatype t = A of v | B of u
  withtype u = int and v = u ;

This should elaborate as:
  type u = real;
  datatype t = A of real | B of int ;
  type u = int and v = real ;
where the tycon t does not have equality status.

It was mistakenly elaborating as:
  type u = real ;
  datatype t = A of int | B of int ;
  type u = int and v = int ;
where the tycon t does not have equality status.  This was due to the
fact that after the first round of elaboration, the tycon t changed
from having equality status to not having equality status.  This
triggered a second round of elaboration, but in an environment where
"type u = int and v = real".  Thus, in the second round of
elaboration, the withtype bindings elaborate to
"type u = int and v = int" and the constructors elaborate to
"A of int" and "B of int".  However, the monotonicity of equality
status changes meant that the tycon t remained as not having equality
status.

To implement proper type checking of datatype declarations with
withtype bindings, elaborate the bindings exactly once and make the
determination of equality status from a tycon application "lazy", and
therefore sensitive to the changes in the equality status of the
tycon.
----------------------------------------------------------------------

U   mlton/trunk/doc/changelog
U   mlton/trunk/mlton/elaborate/elaborate-core.fun
U   mlton/trunk/mlton/elaborate/elaborate-env.fun
U   mlton/trunk/mlton/elaborate/type-env.fun

----------------------------------------------------------------------

Modified: mlton/trunk/doc/changelog
===================================================================
--- mlton/trunk/doc/changelog	2010-03-12 21:33:03 UTC (rev 7433)
+++ mlton/trunk/doc/changelog	2010-03-12 21:33:05 UTC (rev 7434)
@@ -62,6 +62,10 @@
     * Eliminated top-level 'type int = Int.int' in output.
     * Include (*#line line:col "file.grm" *) directives in output.
 
+* 2010-03-12
+  - Fixed bug in elaboration of datatype declarations with withtype
+    bindings.
+
 * 2009-12-11
   - Fixed performance bug in ref flatten SSA2 optimization.
 

Modified: mlton/trunk/mlton/elaborate/elaborate-core.fun
===================================================================
--- mlton/trunk/mlton/elaborate/elaborate-core.fun	2010-03-12 21:33:03 UTC (rev 7433)
+++ mlton/trunk/mlton/elaborate/elaborate-core.fun	2010-03-12 21:33:05 UTC (rev 7434)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2009 Matthew Fluet.
+(* Copyright (C) 2009-2010 Matthew Fluet.
  * Copyright (C) 1999-2008 Henry Cejtin, Matthew Fluet, Suresh
  *    Jagannathan, and Stephen Weeks.
  * Copyright (C) 1997-2000 NEC Research Institute.
@@ -1662,85 +1662,84 @@
                     tycon = tycon,
                     tyvars = tyvars}
                 end)
-            val change = ref false
-            fun elabAll () =
-               (elabTypBind withtypes
-                ; (Vector.map
-                   (datatypes,
-                    fn {cons, makeCons, name, tycon, tyvars} =>
-                    let
-                       val resultType: Type.t =
-                          Type.con (tycon, Vector.map (tyvars, Type.var))
-                       val (schemes, datatypeCons) =
-                          Vector.unzip
-                          (Vector.map
-                           (cons, fn {arg, con, ...} =>
-                            let
-                               val (arg, ty) =
-                                  case arg of
-                                     NONE => (NONE, resultType)
-                                   | SOME t =>
-                                        let
-                                           val t = elabType t
-                                        in
-                                           (SOME t, Type.arrow (t, resultType))
-                                        end
-                               val scheme =
-                                  Scheme.make {canGeneralize = true,
-                                               ty = ty,
-                                               tyvars = tyvars}
-                            in
-                               (scheme, {arg = arg, con = con})
-                            end))
-                       val _ =
-                          let
-                             val r = TypeEnv.tyconAdmitsEquality tycon
-                             datatype z = datatype AdmitsEquality.t
-                          in
-                             case !r of
-                                Always => Error.bug "ElaborateCore.elaborateDec.elabDatBind: Always"
-                              | Never => ()
-                              | Sometimes =>
-                                   if Vector.forall
-                                      (datatypeCons, fn {arg, ...} =>
-                                       case arg of
-                                          NONE => true
-                                        | SOME ty =>
-                                             Scheme.admitsEquality
-                                             (Scheme.make {canGeneralize = true,
-                                                           ty = ty,
-                                                           tyvars = tyvars}))
-                                      then ()
-                                   else (r := Never; change := true)
-                          end
-                    val typeStr =
-                       TypeStr.data (tycon,
-                                     Kind.Arity (Vector.length tyvars),
-                                     makeCons schemes)
-                    val _ =
-                       Env.extendTycon (E, name, typeStr,
-                                        {forceUsed = false, isRebind = true})
-                 in
-                    ({cons = datatypeCons,
-                      tycon = tycon,
-                      tyvars = tyvars},
-                     {tycon = name,
-                      typeStr = typeStr})
-                 end)))
-            (* We don't want to re-elaborate the datatypes if there has been a
-             * type error, because that will cause duplicate error messages.
-             *)
-            val numErrors = !Control.numErrors
+            val _ = elabTypBind withtypes
+            val (dbs, strs) =
+               (Vector.unzip o Vector.map)
+               (datatypes,
+                fn {cons, makeCons, name, tycon, tyvars} =>
+                let
+                   val resultType: Type.t =
+                      Type.con (tycon, Vector.map (tyvars, Type.var))
+                   val (schemes, datatypeCons) =
+                      Vector.unzip
+                      (Vector.map
+                       (cons, fn {arg, con, ...} =>
+                        let
+                           val (arg, ty) =
+                              case arg of
+                                 NONE => (NONE, resultType)
+                               | SOME t =>
+                                    let
+                                       val t = elabType t
+                                    in
+                                       (SOME t, Type.arrow (t, resultType))
+                                    end
+                           val scheme =
+                              Scheme.make {canGeneralize = true,
+                                           ty = ty,
+                                           tyvars = tyvars}
+                        in
+                           (scheme, {arg = arg, con = con})
+                        end))
+                   val typeStr =
+                      TypeStr.data (tycon,
+                                    Kind.Arity (Vector.length tyvars),
+                                    makeCons schemes)
+                in
+                   ({cons = datatypeCons,
+                     tycon = tycon,
+                     tyvars = tyvars},
+                    {tycon = name,
+                     typeStr = typeStr})
+                end)
+            val _ =
+               Vector.map
+               (strs, fn {tycon, typeStr} =>
+                Env.extendTycon (E, tycon, typeStr,
+                                 {forceUsed = false, isRebind = true}))
             (* Maximize equality. *)
+            val change = ref false
             fun loop () =
                let
-                  val res = elabAll ()
+                  val _ =
+                     Vector.foreach
+                     (dbs, fn {cons, tycon, tyvars} =>
+                      let
+                         val r = TypeEnv.tyconAdmitsEquality tycon
+                         datatype z = datatype AdmitsEquality.t
+                      in
+                         case !r of
+                            Always => Error.bug "ElaborateCore.elaborateDec.elabDatBind: Always"
+                          | Never => ()
+                          | Sometimes =>
+                               if Vector.forall
+                                  (cons, fn {arg, con, ...} =>
+                                   case arg of
+                                      NONE => true
+                                    | SOME ty =>
+                                         Scheme.admitsEquality
+                                         (Scheme.make {canGeneralize = true,
+                                                       ty = ty,
+                                                       tyvars = tyvars}))
+                                  then ()
+                               else (r := Never; change := true)
+                      end)
                in
-                  if !change andalso numErrors = !Control.numErrors
+                  if !change
                      then (change := false; loop ())
-                  else res
+                  else ()
                end
-            val (dbs, strs) = Vector.unzip (loop ())
+            val _ = loop ()
          in
             (Decs.single (Cdec.Datatype dbs), strs)
          end

Modified: mlton/trunk/mlton/elaborate/elaborate-env.fun
===================================================================
--- mlton/trunk/mlton/elaborate/elaborate-env.fun	2010-03-12 21:33:03 UTC (rev 7433)
+++ mlton/trunk/mlton/elaborate/elaborate-env.fun	2010-03-12 21:33:05 UTC (rev 7434)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2009 Matthew Fluet.
+(* Copyright (C) 2009-2010 Matthew Fluet.
  * Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh
  *    Jagannathan, and Stephen Weeks.
  * Copyright (C) 1997-2000 NEC Research Institute.
@@ -2039,7 +2039,7 @@
                case uses of
                   New => newUses ()
                 | Old u => u
-                | Rebind => Error.bug "ElaborateEnv.extend.rebind.new"
+                | Rebind => Error.bug "ElaborateEnv.extend.rebind.new: Rebind"
          in
             {domain = domain,
              range = range,

Modified: mlton/trunk/mlton/elaborate/type-env.fun
===================================================================
--- mlton/trunk/mlton/elaborate/type-env.fun	2010-03-12 21:33:03 UTC (rev 7433)
+++ mlton/trunk/mlton/elaborate/type-env.fun	2010-03-12 21:33:05 UTC (rev 7434)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2009 Matthew Fluet.
+(* Copyright (C) 2009-2010 Matthew Fluet.
  * Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh
  *    Jagannathan, and Stephen Weeks.
  * Copyright (C) 1997-2000 NEC Research Institute.
@@ -146,6 +146,7 @@
        | Unknown of {whenKnown: (bool -> bool) list ref}
       datatype t =
          False
+       | Lazy of unit -> t
        | Maybe of maybe ref
        | True
 
@@ -154,6 +155,7 @@
       fun set (e: t, b: bool): bool =
          case e of
             False => b = false
+          | Lazy th => set (th (), b)
           | Maybe r =>
                (case !r of
                    Known b' => b = b'
@@ -164,6 +166,7 @@
       fun when (e: t, f: bool -> bool): bool =
          case e of
             False => f false
+          | Lazy th => when (th (), f)
           | Maybe r =>
                (case !r of
                    Known b => f b
@@ -180,6 +183,8 @@
           | (_, False) => False
           | (True, _) => e'
           | (_, True) => e
+          | (Lazy th, e') => Lazy (fn () => and2 (th (), e'))
+          | (e, Lazy th') => Lazy (fn () => and2 (e, th' ()))
           | (Maybe r, Maybe r') =>
                (case (!r, !r') of
                    (Known false, _) => False
@@ -220,6 +225,7 @@
       fun toBoolOpt (e: t): bool option =
          case e of
             False => SOME false
+          | Lazy th => toBoolOpt (th ())
           | Maybe r =>
                (case !r of
                    Known b => SOME b
@@ -235,7 +241,20 @@
          in
             case !(tyconAdmitsEquality c) of
                Always => truee
-             | Sometimes => andd es
+             | Sometimes =>
+                  let
+                     val e = andd es
+                  in
+                     case e of
+                        False => falsee
+                      | _ =>
+                           Lazy
+                           (fn () =>
+                            case !(tyconAdmitsEquality c) of
+                               Always => Error.bug "TypeEnv.Equality.applyTycon: Always"
+                             | Sometimes => e
+                             | Never => falsee)
+                  end
              | Never => falsee
          end
 
@@ -1589,6 +1608,10 @@
             Type.unknown {canGeneralize = canGeneralize,
                           equality = Equality.truee})))
 
+      val admitsEquality =
+         Trace.trace ("TypeEnv.Scheme.admitsEquality", layout, Bool.layout)
+         admitsEquality
+
       fun haveFrees (v: t vector): bool vector =
          let
             fun con (_, _, bs) = Vector.exists (bs, fn b => b)




More information about the MLton-commit mailing list