diff src/elaborate.sml @ 2094:0d898b086bbe

Improve wildify heuristic for finding record type-class witnesses
author Adam Chlipala <adam@chlipala.net>
date Tue, 23 Dec 2014 13:42:20 -0500
parents d4eb9b6729f8
children 8efba492c48b
line wrap: on
line diff
--- a/src/elaborate.sml	Tue Dec 23 12:24:38 2014 -0500
+++ b/src/elaborate.sml	Tue Dec 23 13:42:20 2014 -0500
@@ -3699,19 +3699,23 @@
                                             fun should t =
                                                 let
                                                     val t = normClassConstraint env' t
+
+                                                    fun shouldR c =
+                                                        case hnormCon env' c of
+                                                            (L'.CApp (f, _), _) =>
+                                                            (case hnormCon env' f of
+                                                                 (L'.CApp (f, cl), loc) =>
+                                                                 (case hnormCon env' f of
+                                                                      (L'.CMap _, _) => isClassOrFolder env' cl
+                                                                    | _ => false)
+                                                               | _ => false)
+                                                            | (L'.CConcat (c1, c2), _) =>
+                                                              shouldR c1 orelse shouldR c2
+                                                            | c => false
                                                 in
                                                     case #1 t of
                                                         L'.CApp (f, _) => isClassOrFolder env' f
-                                                      | L'.TRecord t =>
-                                                        (case hnormCon env' t of
-                                                             (L'.CApp (f, _), _) =>
-                                                             (case hnormCon env' f of
-                                                                  (L'.CApp (f, cl), loc) =>
-                                                                  (case hnormCon env' f of
-                                                                       (L'.CMap _, _) => isClassOrFolder env' cl
-                                                                     | _ => false)
-                                                                | _ => false)
-                                                           | _ => false)
+                                                      | L'.TRecord t => shouldR t
                                                       | _ => false
                                                 end
                                          in