summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-01-28 08:47:04 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2015-01-28 08:47:04 -0500
commit1a063e0d926ebaf414349df3854af12369c81f5a (patch)
tree76628810e7ccd84fa5062c9d06310d668ea8ee96 /src
parent4ebd5fa2b9a3419e93d1289150d9fd5559a58e42 (diff)
Improve wildification for records of type-class witnesses
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml17
1 files changed, 16 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f6819830..5b18ae94 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3697,6 +3697,21 @@ and wildifyStr env (str, sgn) =
| c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE)
+ fun isClassOrFolder' env (c : L'.con) =
+ case #1 c of
+ L'.CAbs (x, k, c) =>
+ let
+ val env = E.pushCRel env x k
+
+ fun toHead (c : L'.con) =
+ case #1 c of
+ L'.CApp (c, _) => toHead c
+ | _ => isClassOrFolder env c
+ in
+ toHead (hnormCon env c)
+ end
+ | _ => isClassOrFolder env c
+
fun buildNeeded env sgis =
#1 (foldl (fn ((sgi, loc), (nd, env')) =>
(case sgi of
@@ -3715,7 +3730,7 @@ and wildifyStr env (str, sgn) =
(case hnormCon env' f of
(L'.CApp (f, cl), loc) =>
(case hnormCon env' f of
- (L'.CMap _, _) => isClassOrFolder env' cl
+ (L'.CMap _, _) => isClassOrFolder' env' cl
| _ => false)
| _ => false)
| (L'.CConcat (c1, c2), _) =>