Explicit error message if rewrite fails due to TC inference (fix #21)

1 files changed, 12 insertions, 3 deletions

diff --git a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
index c55067c..b21de4d 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
@@ -590,6 +590,7 @@ let match_upats_FO upats env sigma0 ise c =
 
 let match_upats_HO upats env sigma0 ise c =
  let it_did_match = ref false in
+ let failed_because_of_TC = ref false in
  let rec aux upats env sigma0 ise c =
   let f, a = splay_app ise c in let i0 = ref (-1) in
   let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
@@ -620,6 +621,9 @@ let match_upats_HO upats env sigma0 ise c =
         raise (FoundUnif (ungen_upat lhs pt' u))
       with FoundUnif _ as sigma_u -> raise sigma_u 
       | NoProgress -> it_did_match := true
+      | Pretype_errors.PretypeError
+         (_,_,Pretype_errors.UnsatisfiableConstraints _) ->
+          failed_because_of_TC:=true
       | _ -> () in
     List.iter one_match fpats
   done;
@@ -627,7 +631,8 @@ let match_upats_HO upats env sigma0 ise c =
   Array.iter (aux upats env sigma0 ise) a
  in
  aux upats env sigma0 ise c;
- if !it_did_match then raise NoProgress
+ if !it_did_match then raise NoProgress;
+ !failed_because_of_TC
 
 let prof_HO = mk_profiler "match_upats_HO";;
 let match_upats_HO upats env sigma0 ise c =
@@ -697,13 +702,17 @@ let source () = match upats_origin, upats with
       anomaly "mk_tpattern_matcher with no upats_origin" in
 ((fun env c h ~k -> 
   do_once upat_that_matched (fun () -> 
+    let failed_because_of_TC = ref false in
     try
       match_upats_FO upats env sigma0 ise c;
-      match_upats_HO upats env sigma0 ise c;
+      failed_because_of_TC:=match_upats_HO upats env sigma0 ise c;
       raise NoMatch
     with FoundUnif sigma_u -> sigma_u
     | NoMatch when (not raise_NoMatch) ->
-      errorstrm (source () ++ str "does not match any subterm of the goal")
+      if !failed_because_of_TC then
+        errorstrm (source ()++strbrk"matches but type classes inference fails")
+      else
+        errorstrm (source () ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
         let dir = match upats_origin with Some (d,_) -> d | _ ->
           anomaly "mk_tpattern_matcher with no upats_origin" in