From 4ecbfd4c845e35126c61e182146005f27d45339a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 13 Oct 2007 13:38:46 +0000 Subject: [PATCH] Add special case for function applications in base type rule checks --- src/tycheck.sml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/tycheck.sml b/src/tycheck.sml index d486603..e2feb90 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) -- 2.20.1