From c771a68c26e952531aca922c0837d961991bd3bc Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Tue, 29 Jul 2014 14:46:06 -0400
Subject: Retweak the last tweak to allow type inference to succeed in a strict
 superset of the places where it used to succeed

---
 src/elaborate.sml | 26 ++++++++++++++++----------
 1 file changed, 16 insertions(+), 10 deletions(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5029ef4d..03e9d6e8 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2013, Adam Chlipala
+(* Copyright (c) 2008-2014, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -1191,6 +1191,12 @@
                  (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
                | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
                | _ => isRecord' ()
+
+         fun maybeIsRecord c =
+             case c of
+                 L'.CRecord _ => isRecord ()
+               | L'.CConcat _ => isRecord ()
+               | _ => err COccursCheckFailed
      in
          (*eprefaces "unifyCons''" [("c1", p_con env c1All),
                                   ("c2", p_con env c2All)];*)
@@ -1220,21 +1226,16 @@
              else
                  err (fn _ => TooLifty (loc1, loc2))
 
-           | (L'.CRecord _, _) => isRecord ()
-           | (_, L'.CRecord _) => isRecord ()
-           | (L'.CConcat _, _) => isRecord ()
-           | (_, L'.CConcat _) => isRecord ()
-
            | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) =>
              if occursCon r c2All then
-                 err COccursCheckFailed
+                 maybeIsRecord c2
              else if f c2All then
                  r := L'.Known c2All
              else
                  err CScope
            | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) =>
              if occursCon r c1All then
-                 err COccursCheckFailed
+                 maybeIsRecord c1
              else if f c1All then
                  r := L'.Known c1All
              else
@@ -1242,7 +1243,7 @@
 
            | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
              if occursCon r c2All then
-                 err COccursCheckFailed
+                 maybeIsRecord c2
              else
                  (let
                       val sq = squish nl c2All
@@ -1255,7 +1256,7 @@
                   handle CantSquish => err (fn _ => TooDeep))
            | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) =>
              if occursCon r c1All then
-                 err COccursCheckFailed
+                 maybeIsRecord c1
              else
                  (let
                       val sq = squish nl c1All
@@ -1267,6 +1268,11 @@
                   end
                   handle CantSquish => err (fn _ => TooDeep))
 
+           | (L'.CRecord _, _) => isRecord ()
+           | (_, L'.CRecord _) => isRecord ()
+           | (L'.CConcat _, _) => isRecord ()
+           | (_, L'.CConcat _) => isRecord ()
+
 
            | (L'.CUnit, L'.CUnit) => ()
 
-- 
cgit v1.2.3