From af622fc60e42ee40c83b4e2b744b8212616b681d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 18 Aug 2016 13:24:50 +0200
Subject: Inference of return clause: giving uniformly priority to "small
 inversion".

As noted by Jason Gross on coq-club (Aug 18, 2016), the "small
inversion" heuristic is not used consistently depending on whether the
variables in the type constraint are Rel or Var.

This commit simply gives uniformly preference to the inversion of the
predicate along the indices of the type over other heuristics.

The next three commits will improve further a uniform use of the
different heuristics.

----------------------------------------------------------------------
Here are some extra comments on how to go further with the inference
of the return predicate:

The "small inversion" heuristic build_inversion_problem (1) is
characterized by two features:

- small inversion properly speaking (a), i.e. that is for a match on
  t:I params p1(u11..u1p1) ... pn(un1..unpn) with pi exposing the
  constructor structure of the indices of the type of t, a return
  clause of the form "fun x1..xn (y:I params x1..xn) => match x1..xn y with
  | p1(z11..z1p1) ... pn(zn1..znpn) => ?T@{z11..znpn}
  | _ => IDProp
  end" is used,

- the dependent subterms in the external type constraint U are replaced
  by existential variables (b) which can be filled either by projecting
  (i.e. installing a dependency) or imitating (i.e. no dependency);
  this is obtained by solving the constraint ?T@{u11..unpn} == U by
  setting ?T@{z11..znpn} := U'(...?wij@{zij:=uij}...) where U has been
  written under the form U'(...uij...) highlighting all occurrences of
  each of the uij occurring in U; otherwise said the problem is reduced to
  the question of instantiating each wij, deciding whether wij@{zij} := zij
  (projection) or wij@{zij} := uij (imitation) [There may be different
  way to expose the uij in U, e.g. in the presence of overlapping, or of
  evars in U; this is left undetermined].

The two other heuristics used are:

- prepare_predicate_from_arsign_tycon (2): takes the external type
  constraint U and decides that each subterm of the form xi or y for a
  match on "y:I params x1 ... xn" is dependent; otherwise said, it
  corresponds to the degenerated form of (1) where
  - no constructor structure is exposed (i.e. each pi is trivial)
  - only uij that are Rel are replaced by an evar ?wij and this evar is
    directly instantiated by projection (hence creating a dependency),

- simple use of of an evar in case no type constraint is given (3):
  this evar is not dependent on the indices nor on the term to match.

Heuristic (1) is not strictly more powerful than other heuristics
because of (at least) two weaknesses.

- The first weakness is due to feature (b), i.e. to letting
  unification decide whether these evars have to create a dependency
  (projection) or not (imitation).

  In particular, the heuristic (2) gives priority to systematic
  abstraction over the dependencies (i.e. giving priority to
  projection over imitation) and it can then be better as the
  following example (from RelationClasses.v) shows:

  Fixpoint arrows (l : Tlist) (r : Type) : Type :=
    match l with
    | Tnil => r
    | A :: l' => A -> arrows l' r
    end.

  Fixpoint predicate_all (l : Tlist) : arrows l Prop -> Prop :=
    match l with
    | Tnil => fun f => f
    | A :: tl => fun f => forall x : A, predicate_all tl (f x)
    end.

  Using (1) fails. It proposes the predicate
  "fun l' => arrows ?l[l':=l'] Prop" so that typing the first branch
  leads to unify "arrows ?l[l:=Tnil] Prop == Prop", a problem about
  which evarconv unification is not able (yet!) to see what are the
  two possible solutions. Using (2) works. It instead directly
  suggests that the predicate is "fun l => arrows l Prop" is used, so
  that unification is not needed.

  Even if in practice the (2) is good (and hence could be added to
  (1)), it is not universally better. Consider e.g.

     y:bool,H1:P y,H2:P y,f:forall y, P y -> Q y |-
              match y as z return Q y with
              | true  => f y H1
              | false => f y H2
              end : Q y

  There is no way to type it with clause "as z return Q z" even if
  trying to generalize H1 and H2 so that they get type P z.

- A second weakness is due to the interaction between small inversion
  and constructors having a type whose indices havex a less refined
  constructor structure than in the term to match, as in:

  Inductive I : nat -> Set :=
  | C1 : forall n : nat, listn n -> I n
  | C2 : forall n : nat, I n -> I n.

  Check (fun x : I 0 => match x with
                        | C1 n l => 0
                        | C2 n c => 0
                        end).

  where the inverted predicate is "in I n return match n with 0 => ?T | _ => IDProp end"
  but neither C1 nor C2 have fine enough types so that n becomes
  constructed. There is a generic solution to that kind of situation which
  is to compile the above into

  Check (fun x : I 0 => match x with
                        | C1 n l => match n with 0 => 0 | _ -> id end
                        | C2 n c => match n with 0 => 0 | _ -> id end
                        end).

  but this is not implemented yet.

  In the absence of this refinement, heuristic (3) can here work
  better.

So, the current status of the claim is that for (1) to be strictly
more powerful than other current heuristics, work has to be done

- (A) at the unification level (by either being able to reduce problems of
  the form "match ?x[constructor] with ... end = a-rigid-term", or, at
  worst, by being able to use the heuristic favoring projecting for such
  a problem), so that it is better than (2),

- (B) at the match compilation level, by enforcing that, in each branch,
  the corresponding constructor is refined so has to match (or
  discriminate) the constraints given by the type of the term to
  match, and hence being better than (3).

Moreover, (2) and (3) are disjoint. Here is an example which (3) can
solve but not (2) (and (1) cannot because of (B)). [To be fixed in
next commit.]

Inductive I : bool -> bool -> Type := C : I true true | D x : I x x.

Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
              match y with
              | C  => f y H1
              | D _ => f y H2
              end : Q y z.

Indeed, (2) infers "as y' in I b z return Q y z" which does not work.

Here is an example which (2) can solve but not (3) (and (1) cannot
because of (B) again). [To be fixed in 2nd next commit].

Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
              match y with
              | C  => f y true H1
              | D b => f y b H2
              end : Q y z.

fix
---
 pretyping/cases.ml          | 22 +++++++++-------------
 test-suite/output/Cases.out | 11 +++--------
 2 files changed, 12 insertions(+), 21 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 33ee579eca..a26e1830d7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1996,10 +1996,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * type and 1 assumption for each term not _syntactically_ in an
  * inductive type.
 
- * Each matched terms are independently considered dependent or not.
-
- * A type constraint but no annotation case: we try to specialize the
- * tycon to make the predicate if it is not closed.
+ * Each matched term is independently considered dependent or not.
  *)
 
 exception LocalOccur
@@ -2031,15 +2028,14 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
     | None, Some t when not (noccur_with_meta sigma 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
-       (* First strategy: we abstract the tycon wrt to the dependencies *)
-         let sigma, t = refresh_tycon sigma t in
-         let p1 =
+        (* First strategy: we build an "inversion" predicate *)
+        let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+        (* Optional second strategy: we abstract the tycon wrt to the dependencies *)
+        let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
-	(* Second strategy: we build an "inversion" predicate *)
-	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	(match p1 with
-         | Some (sigma1,pred1,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign]
-         | None -> [sigma2, pred2, arsign])
+        (match p2 with
+         | Some (sigma2,pred2,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign]
+         | None -> [sigma1, pred1, arsign])
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -2052,7 +2048,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
 	in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-	(* Second strategy: we directly use the evar as a non dependent pred *)
+        (* Second strategy: we use the evar or tycon as a non dependent pred *)
         let pred2 = lift (List.length (List.flatten arsign)) t in
         [sigma1, pred1, arsign; sigma, pred2, arsign]
     (* Some type annotation *)
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index dfab400baa..cb835ab48d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -64,14 +64,9 @@ In environment
 texpDenote : forall t : type, texp t -> typeDenote t
 t : type
 e : texp t
-t1 : type
-t2 : type
-t0 : type
-b : tbinop t1 t2 t0
-e1 : texp t1
-e2 : texp t2
-The term "0" has type "nat" while it is expected to have type
- "typeDenote t0".
+n : nat
+The term "n" has type "nat" while it is expected to have type
+ "typeDenote ?t@{t1:=Nat}".
 fun '{{n, m, _}} => n + m
      : J -> nat
 fun '{{n, m, p}} => n + m + p
-- 
cgit v1.2.3


From 7cf8be66f4215dabb1c072c589299283e4134d4c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 16:52:12 +0200
Subject: Trying a no-inversion no-dependency heuristic for match return
 clause.

The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.

See previous commit for discussion.
---
 pretyping/cases.ml          | 55 ++++++++++++++++++---------------------------
 test-suite/success/Case13.v | 14 ++++++++++++
 2 files changed, 36 insertions(+), 33 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a26e1830d7..951c36290c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1999,21 +1999,6 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * Each matched term is independently considered dependent or not.
  *)
 
-exception LocalOccur
-
-let noccur_with_meta sigma n m term =
-  let rec occur_rec n c = match EConstr.kind sigma c with
-    | Rel p -> if n<=p && p<n+m then raise LocalOccur
-    | App(f,cl) ->
-        (match EConstr.kind sigma f with
-           | Cast (c,_,_) when isMeta sigma c -> ()
-           | Meta _ -> ()
-           | _ -> EConstr.iter_with_binders sigma succ occur_rec n c)
-    | Evar (_, _) -> ()
-    | _ -> EConstr.iter_with_binders sigma succ occur_rec n c
-  in
-  try (occur_rec n term; true) with LocalOccur -> false
-
 let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
     (** If we put the typing constraint in the term, it has to be
@@ -2025,30 +2010,34 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
     (* No return clause *)
-    | None, Some t when not (noccur_with_meta sigma 0 max_int t) ->
-	(* If the tycon is not closed w.r.t real variables, we try *)
-        (* two different strategies *)
-        (* First strategy: we build an "inversion" predicate *)
+    | None, Some t ->
+        let sigma,t = refresh_tycon sigma t in
+        (* First strategy: we build an "inversion" predicate, also replacing the *)
+        (* dependencies with existential variables *)
         let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
         (* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+        (* Third strategy: we take the type constraint as it is; of course we could *)
+        (* need something inbetween, abstracting some but not all of the dependencies *)
+        (* the "inversion" strategy deals with that but unification may not be *)
+        (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
+        (* work (yet) when a constructor has a type not precise enough for the inversion *)
+        (* see log message for details *)
+        let pred3 = lift (List.length (List.flatten arsign)) t in
         (match p2 with
-         | Some (sigma2,pred2,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign]
-         | None -> [sigma1, pred1, arsign])
-    | None, _ ->
-	(* No dependent type constraint, or no constraints at all: *)
-	(* we use two strategies *)
-        let sigma,t = match tycon with
-	| Some t -> refresh_tycon sigma t
-	| None -> 
-          let (sigma, (t, _)) =
-            new_type_evar !!env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
-	    sigma, t
-	in
+         | Some (sigma2,pred2,arsign) when not (EConstr.eq_constr sigma pred2 pred3) ->
+             [sigma1, pred1, arsign; sigma2, pred2, arsign; sigma, pred3, arsign]
+         | _ ->
+             [sigma1, pred1, arsign; sigma, pred3, arsign])
+    | None, None ->
+        (* No type constraint: we use two strategies *)
+        (* we first create a generic evar type constraint *)
+        let src = (loc, Evar_kinds.CasesType false) in
+        let sigma, (t, _) = new_type_evar !!env sigma univ_flexible_alg ~src in
         (* First strategy: we build an "inversion" predicate *)
-	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-        (* Second strategy: we use the evar or tycon as a non dependent pred *)
+        let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+        (* Second strategy: we use the evar as a non dependent pred *)
         let pred2 = lift (List.length (List.flatten arsign)) t in
         [sigma1, pred1, arsign; sigma, pred2, arsign]
     (* Some type annotation *)
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..e388acdcb0 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,17 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+   given (and when the "inversion-and-dependencies-as-evars" strategy
+   is not strong enough because of a constructor with a type whose
+   pattern structure is not refined enough for it to be captured by
+   the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
-- 
cgit v1.2.3


From 29f749d87aebb8226bb9da624c57f83942881a99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:13:58 +0200
Subject: Trying an abstracting dependencies heuristic for the match return
 clause even when no type constraint is given.

This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.

By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.

See penultimate commit for discussion.
---
 pretyping/cases.ml          | 25 +++++++++++--------------
 test-suite/success/Case13.v | 12 ++++++++++++
 2 files changed, 23 insertions(+), 14 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 951c36290c..f167e65b96 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2008,10 +2008,17 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
                       !!env sigma t
   in
   let preds =
-    match pred, tycon with
+    match pred with
     (* No return clause *)
-    | None, Some t ->
-        let sigma,t = refresh_tycon sigma t in
+    | None ->
+        let sigma,t =
+          match tycon with
+          | Some t -> refresh_tycon sigma t
+          | None ->
+             (* No type constraint: we first create a generic evar type constraint *)
+             let src = (loc, Evar_kinds.CasesType false) in
+             let sigma, (t, _) = new_type_evar !!env sigma univ_flexible_alg ~src in
+             sigma, t in
         (* First strategy: we build an "inversion" predicate, also replacing the *)
         (* dependencies with existential variables *)
         let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
@@ -2030,18 +2037,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
              [sigma1, pred1, arsign; sigma2, pred2, arsign; sigma, pred3, arsign]
          | _ ->
              [sigma1, pred1, arsign; sigma, pred3, arsign])
-    | None, None ->
-        (* No type constraint: we use two strategies *)
-        (* we first create a generic evar type constraint *)
-        let src = (loc, Evar_kinds.CasesType false) in
-        let sigma, (t, _) = new_type_evar !!env sigma univ_flexible_alg ~src in
-        (* First strategy: we build an "inversion" predicate *)
-        let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-        (* Second strategy: we use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten arsign)) t in
-        [sigma1, pred1, arsign; sigma, pred2, arsign]
     (* Some type annotation *)
-    | Some rtntyp, _ ->
+    | Some rtntyp ->
       (* We extract the signature of the arity *)
       let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index e388acdcb0..8fad41cd8f 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -101,3 +101,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
         | F  => f y H1
         | G _ => f y H2
         end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.
-- 
cgit v1.2.3


From b2361208a1242a92af7d18cb723ef3b7b55d79b5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:29:26 +0200
Subject: Possible abstractions over goal variables when inferring match return
 clause.

The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".

By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".

See antepenultimate commit for discussion.
---
 pretyping/cases.ml          | 42 +++++++++++++++++++++++++++++++-----------
 test-suite/success/Case13.v | 12 ++++++++++++
 2 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f167e65b96..37dd3708b3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1941,16 +1941,28 @@ let inh_conv_coerce_to_tycon ?loc env sigma j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
+let add_subst sigma c len (rel_subst,var_subst) =
+  match EConstr.kind sigma c with
+  | Rel n -> (n,len) :: rel_subst, var_subst
+  | Var id -> rel_subst, (id,len) :: var_subst
+  | _ -> assert false
+
+let dependent_rel_or_var sigma tm c =
+  match EConstr.kind sigma tm with
+  | Rel n -> not (noccurn sigma n c)
+  | Var id -> Termops.local_occur_var sigma id c
+  | _ -> assert false
+
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let subst, len =
+  let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match EConstr.kind sigma tm with
-          | Rel n when Int.equal signlen 1 && not (noccurn sigma n c)
+          | Rel _ | Var _ when Int.equal signlen 1 && dependent_rel_or_var sigma tm c
             (* The term to match is not of a dependent type itself *) ->
-	      ((n, len) :: subst, len - signlen)
-	  | Rel n when signlen > 1 (* The term is of a dependent type,
+              (add_subst sigma tm len subst, len - signlen)
+          | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1959,28 +1971,36 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match EConstr.kind sigma arg with
-                          | Rel n when not (noccurn sigma n c) ->
-			      ((n, len) :: subst, pred len)
+                          | Rel _ | Var _ when dependent_rel_or_var sigma arg c ->
+                              (add_subst sigma arg len subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-                      if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs
-		      then (n, len) :: subst else subst
+                      if dependent_rel_or_var sigma tm c && List.for_all (fun c -> isRel sigma c || isVar sigma c) realargs
+                      then add_subst sigma tm len subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign ([], nar)
+      (List.rev tomatchs) arsign (([],[]), nar)
   in
   let rec predicate lift c =
     match EConstr.kind sigma c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) subst in
+              let idx = Int.List.assoc (n - lift) rel_subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign. *)
+              (* A variable that is not matched, lift over the arsign *)
 	      mkRel (n + nar))
+      | Var id ->
+          (try
+              (* Make the predicate dependent on the matched variable *)
+              let idx = Id.List.assoc id var_subst in
+                mkRel (idx + lift)
+            with Not_found ->
+              (* A variable that is not matched *)
+              c)
       | _ ->
 	  EConstr.map_with_binders sigma succ predicate lift c
   in
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8fad41cd8f..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -113,3 +113,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
         | F  => f y true H1
         | G b => f y b H2
         end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.
-- 
cgit v1.2.3


From bfbc82eb29c9dbf868d3decbd30b0462ea398ebd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 May 2018 18:33:26 +0200
Subject: A word about PR #262 in CHANGES.

---
 CHANGES | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index b2f2987249..e16da2ab2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -83,7 +83,7 @@ Focusing
   e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
   As usual, unfocus with `}` once the sub-goal is fully solved.
 
-Specification language
+Specification language, type inference
 
 - A fix to unification (which was sensitive to the ascii name of
   variables) may occasionally change type inference in incompatible
@@ -94,6 +94,11 @@ Specification language
   induce an overhead if the cost of checking the conversion of the
   corresponding definitions is additionally high (PR #8215).
 
+- A few improvements in inference of the return clause of "match" can
+  exceptionally introduce incompatibilities (PR #262). This can be
+  solved by writing an explicit "return" clause, sometimes even simply
+  an explicit "return _" clause.
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
-- 
cgit v1.2.3