From 17b3f5af99c07d7361fb99124412aff1768cfe13 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 21 Oct 2008 19:24:39 -0400
Subject: Sum demo, minus inference of {Unit}s

---
 src/elaborate.sml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index b965f0da..1ea854cd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -821,17 +821,20 @@
              gs1 @ gs2 @ gs3 @ gs4
          end
        | _ =>
-         let
-             val (c1, gs1) = hnormCon (env, denv) c1
-             val (c2, gs2) = hnormCon (env, denv) c2
-         in
+         case (kindof env c1, kindof env c2) of
+             ((L'.KUnit, _), (L'.KUnit, _)) => []
+           | _ =>
              let
-                 val gs3 = unifyCons'' (env, denv) c1 c2
+                 val (c1, gs1) = hnormCon (env, denv) c1
+                 val (c2, gs2) = hnormCon (env, denv) c2
              in
-                 gs1 @ gs2 @ gs3
+                 let
+                     val gs3 = unifyCons'' (env, denv) c1 c2
+                 in
+                     gs1 @ gs2 @ gs3
+                 end
+                 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
              end
-             handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
-         end
 
  and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
      let
-- 
cgit v1.2.3