Type annotations on environment variable reads

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

diff --git a/src/tycheck.sml b/src/tycheck.sml
index d486603..8889540 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -184,10 +184,21 @@ fun baseCondition t =
                              | _ => false))
       | _ => NONE
 
+fun simplifyKindOf e =
+    case e of
+       (EApp ((EVar s, _), e'), _) =>
+       (case Env.function s of
+            NONE => e
+          | SOME f =>
+            case f [e'] of
+                NONE => e
+              | SOME e => e)
+      | _ => e
+
 fun hasTyp (e, t1, t2) =
     if (case baseCondition t2 of
            NONE => false
-         | SOME rule => rule e) then
+         | SOME rule => rule (simplifyKindOf e)) then
        ()
     else
        subTyp (t1, t2)
@@ -237,7 +248,7 @@ fun envVarSetFrom v (e, _) =
            SOME e
        else
            NONE
-      | EGet (_, _, e) => envVarSetFrom v e
+      | EGet (_, _, _, e) => envVarSetFrom v e
       | ESeq es => foldr (fn (e, found) =>
                             case found of
                                 SOME _ => found
@@ -247,6 +258,11 @@ fun envVarSetFrom v (e, _) =
 
       | _ => NONE
 
+fun ununify (tAll as (t, _)) =
+    case t of
+       TUnif (_, ref (SOME t)) => ununify t
+      | _ => tAll
+
 fun checkExp G (eAll as (e, loc)) =
     let
        val dte = Describe.describe_type_error loc
@@ -346,14 +362,18 @@ fun checkExp G (eAll as (e, loc)) =
                          SM.insert (SM.empty, evar, t)),
                 loc)
            end
-         | EGet (x, evar, rest) =>
+         | EGet (x, topt, evar, rest) =>
            let
                val xt = (newUnif (), loc)
                val G' = bindVal G (x, xt, NONE)
 
                val rt = whnorm (checkExp G' rest)
            in
-               case rt of
+               case topt of
+                   NONE => ()
+                 | SOME t => subTyp (xt, checkTyp G t);
+
+               case ununify rt of
                    (TAction (p, d, r), _) =>
                    (case SM.find (d, evar) of
                         NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)