Add special case for function applications in base type rule checks
authorAdam Chlipala <adamc@hcoop.net>
Sat, 13 Oct 2007 13:38:46 +0000 (13:38 +0000)
committerAdam Chlipala <adamc@hcoop.net>
Sat, 13 Oct 2007 13:38:46 +0000 (13:38 +0000)
src/tycheck.sml

index d486603..e2feb90 100644 (file)
@@ -184,10 +184,21 @@ fun baseCondition t =
                              | _ => false))
       | _ => NONE
 
                              | _ => 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
 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)
        ()
     else
        subTyp (t1, t2)