From 1c58ce1a627bedb4d57e64f429d09721c55de340 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 23 Dec 2014 13:42:20 -0500 Subject: Improve wildify heuristic for finding record type-class witnesses --- src/elaborate.sml | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) (limited to 'src/elaborate.sml') 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 -- cgit v1.2.3