diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2014-07-29 14:46:06 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2014-07-29 14:46:06 -0400 |
| commit | c771a68c26e952531aca922c0837d961991bd3bc (patch) | |
| tree | 8964db62b823642a86861b501dbf64c5ec441b5f /src/elaborate.sml | |
| parent | 2d7238252d0cd1165f74aea511a03b9899ca105b (diff) | |
Retweak the last tweak to allow type inference to succeed in a strict superset of the places where it used to succeed
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 26 |
1 files changed, 16 insertions, 10 deletions
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) => () |