Attempt to improve error rendering in pattern-matching compilation (#5142).

When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.

3 files changed, 21 insertions, 5 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0ac34b7186..5c9ce2624c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -62,13 +62,14 @@ let error_wrong_numarg_constructor_loc loc env c n =
 let error_wrong_numarg_inductive_loc loc env c n =
   raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n))
 
-let rec list_try_compile f = function
-  | [a] -> f a
-  | [] -> anomaly (str "try_find_f")
+let list_try_compile f l =
+  let rec aux errors = function
+  | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors)
   | h::t ->
       try f h
-      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
-	    list_try_compile f t
+      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+	    aux (e::errors) t in
+  aux [] l
 
 let force_name =
   let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 2b828d382a..95fcd362ef 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -56,3 +56,6 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+The command has indeed failed with message:
+Non exhaustive pattern-matching: no clause found for pattern 
+gadtTy _ _
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 3c2eaf42c9..1903753cc5 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -77,3 +77,15 @@ destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
+
+(* Was enhancement request #5142 (error message reported on the most
+   general return clause heuristic) *)
+
+Inductive gadt : Type -> Type :=
+| gadtNat : nat -> gadt nat
+| gadtTy : forall T, T -> gadt T.
+
+Fail Definition gadt_id T (x: gadt T) : gadt T :=
+  match x with
+  | gadtNat n => gadtNat n
+  end.