diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2014-12-23 13:42:20 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2014-12-23 13:42:20 -0500 |
| commit | ddb9bc67c740c21040267f2a6a68fd72f2cdfa25 (patch) | |
| tree | 16241b26a2754583c32f51ad977348034ba4f908 | |
| parent | d9656e5b07438175a837d77a92f3fc16d8b3c318 (diff) | |
Improve wildify heuristic for finding record type-class witnesses
| -rw-r--r-- | src/elaborate.sml | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index f5edbe3e..84d3dc09 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3699,19 +3699,23 @@ and wildifyStr env (str, sgn) = 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 |