diff src/elaborate.sml @ 2109:f42fea631c1d

Improve wildification for records of type-class witnesses
author Adam Chlipala <adam@chlipala.net>
date Wed, 28 Jan 2015 08:47:04 -0500
parents 32e2752390ad
children 010ce27228f1
line wrap: on
line diff
--- a/src/elaborate.sml	Thu Jan 22 11:26:24 2015 -0500
+++ b/src/elaborate.sml	Wed Jan 28 08:47:04 2015 -0500
@@ -3697,6 +3697,21 @@
 
                        | 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 @@
                                                             (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), _) =>