X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/9b7ee2b22abce813120a633f5a4f5523a630a2ea..8cbb96323335d1a2b42a9daac94a9d538ab93536:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index d486603..8889540 100644
--- 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)