E-mail aliases

[hcoop/domtool2.git] / src / tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 8d35e2d..ac69a6d 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -112,9 +112,6 @@ datatype type_error =
        | UnboundVariable of string
        | WrongPred of string * pred * pred
 
-fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
-                                       [PD.string s, PD.space 1, d]))
-
 fun describe_unification_error t ue =
     case ue of
        UnifyPred (p1, p2) =>
@@ -281,17 +278,23 @@ fun whnorm (tAll as (t, loc)) =
        TUnif (_, ref (SOME tAll)) => whnorm tAll
       | _ => tAll
 
+fun baseCondition t =
+    case whnorm t of
+       (TBase name, _) => typeRule name
+      | (TList t, _) =>
+       (case baseCondition t of
+            NONE => NONE
+          | SOME f => SOME (fn (EList ls, _) => List.all f ls
+                             | _ => false))
+      | _ => NONE
+
 fun hasTyp (e, t1, t2) =
-    case whnorm t2 of
-       (TBase name, _) =>
-       (case typeRule name of
-            NONE => subTyp (t1, t2)
-          | SOME rule =>
-            if rule e then
-                ()
-            else
-                subTyp (t1, t2))
-      | _ => subTyp (t1, t2)
+    if (case baseCondition t2 of
+           NONE => false
+         | SOME rule => rule e) then
+       ()
+    else
+       subTyp (t1, t2)
 
 fun checkTyp G (tAll as (t, loc)) =
     let