summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-02-14 15:11:22 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-02-14 15:11:22 -0500
commit6a907ba38d008761d8b5260bcfd721ead0626e08 (patch)
treeb74bb91f14dc7c250113d1f205b43a431e93f7ee /src/elaborate.sml
parent9d1eacaab495588439dfc5cb25b6e495bce332c1 (diff)
Fix a subtle renaming problem in elaborating functor applications
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml25
1 files changed, 22 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0c8db756..959a6cd1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4481,9 +4481,28 @@ and elabStr (env, denv) (str, loc) =
case #1 (hnormSgn env ran) of
L'.SgnError => (strerror, sgnerror, [])
| L'.SgnConst sgis =>
- ((L'.StrApp (str1', str2'), loc),
- (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
- gs1 @ gs2)
+ let
+ (* This code handles a tricky case that led to a very nasty bug.
+ * An invariant about signatures of elaborated modules is that no
+ * identifier that could appear directly in a program is defined
+ * twice. We add "?" in front of identifiers where necessary to
+ * maintain the invariant, but the code below, to extend a functor
+ * body with a binding for the functor argument, wasn't written
+ * with the invariant in mind. Luckily for us, references to
+ * an identifier later within a signature work by globally
+ * unique index, so we just need to change the string name in the
+ * new declaration. *)
+ val m =
+ if List.exists (fn (L'.SgiStr (x, _, _), _) => x = m
+ | _ => false) sgis then
+ "?" ^ m
+ else
+ m
+ in
+ ((L'.StrApp (str1', str2'), loc),
+ (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
+ gs1 @ gs2)
+ end
| _ => raise Fail "Unable to hnormSgn in functor application")
| _ => (strError env (NotFunctor sgn1);
(strerror, sgnerror, []))