Merge PR #11261: Use implicit types for printing (granting wish #10366).

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego

5 files changed, 137 insertions, 20 deletions

diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
new file mode 100644
index 0000000000..51818c666b
--- /dev/null
+++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  :cmd:`Implicit Types` are now taken into account for printing. To inhibit it,
+  unset the :flag:`Printing Use Implicit Types` flag
+  (`#11261 <https://github.com/coq/coq/pull/11261>`_,
+  by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f0bbaed8f3..9686500a35 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2208,6 +2208,13 @@ or :g:`m` to the type :g:`nat` of natural numbers).
 
   Adds blocks of implicit types with different specifications.
 
+.. flag:: Printing Use Implicit Types
+
+  By default, the type of bound variables is not printed when
+  the variable name is associated to an implicit type which matches the
+  actual type of the variable. This feature can be deactivated by
+  turning this flag off.
+
 .. _implicit-generalization:
 
 Implicit generalization
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 828c88adbe..38dc10a9b3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes
 (* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
 let print_no_symbol = ref false
 
+(* This tells to skip types if a variable has this type by default *)
+let print_use_implicit_types =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Use";"Implicit";"Types"]
+    ~value:true
+
+(**********************************************************************)
+
+let hole = CAst.make @@ CHole (None, IntroAnonymous, None)
+
+let is_reserved_type na t =
+  not !Flags.raw_print && print_use_implicit_types () &&
+  match na with
+  | Anonymous -> false
+  | Name id ->
+    try
+      let pat = Reserve.find_reserved_type id in
+      let _ = match_notation_constr false t ([],pat) in
+      true
+    with Not_found | No_match -> false
+
 (**********************************************************************)
 (* Turning notations and scopes on and off for printing *)
 module IRuleSet = Set.Make(struct
@@ -790,6 +812,12 @@ let rec flatten_application c = match DAst.get c with
     end
   | a -> c
 
+let same_binder_type ty nal c =
+  match nal, DAst.get c with
+  | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty'
+  | [], _ -> true
+  | _ -> assert false
+
 (**********************************************************************)
 (* mapping glob_constr to numerals (in presence of coercions, choose the *)
 (* one with no delimiter if possible)                                 *)
@@ -939,12 +967,10 @@ let rec extern inctx scopes vars r =
               extern inctx scopes (add_vname vars na) c)
 
   | GProd (na,bk,t,c) ->
-      let t = extern_typ scopes vars t in
-      factorize_prod scopes (add_vname vars na) na bk t c
+      factorize_prod scopes vars na bk t c
 
   | GLambda (na,bk,t,c) ->
-      let t = extern_typ scopes vars t in
-      factorize_lambda inctx scopes (add_vname vars na) na bk t c
+      factorize_lambda inctx scopes vars na bk t c
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -1045,7 +1071,10 @@ and extern_typ (subentry,(_,scopes)) =
 
 and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
 
-and factorize_prod scopes vars na bk aty c =
+and factorize_prod scopes vars na bk t c =
+  let implicit_type = is_reserved_type na t in
+  let aty = extern_typ scopes vars t in
+  let vars = add_vname vars na in
   let store, get = set_temporary_memory () in
   match na, DAst.get c with
   | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
@@ -1062,18 +1091,25 @@ and factorize_prod scopes vars na bk aty c =
       | _ -> CProdN ([binder],b))
      | _ -> assert false)
   | _, _ ->
-      let c = extern_typ scopes vars c in
-      match na, c.v with
+      let c' = extern_typ scopes vars c in
+      match na, c'.v with
       | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
-           when binding_kind_eq bk bk' && constr_expr_eq aty ty
-                && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
-         CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
+           when binding_kind_eq bk bk'
+                && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *)
+                && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+         let ty = if implicit_type then ty else aty in
+         CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b)
       | _, CProdN (bl,b) ->
-         CProdN (CLocalAssum([make na],Default bk,aty)::bl,b)
+         let ty = if implicit_type then hole else aty in
+         CProdN (CLocalAssum([make na],Default bk,ty)::bl,b)
       | _, _ ->
-         CProdN ([CLocalAssum([make na],Default bk,aty)],c)
+         let ty = if implicit_type then hole else aty in
+         CProdN ([CLocalAssum([make na],Default bk,ty)],c')
 
-and factorize_lambda inctx scopes vars na bk aty c =
+and factorize_lambda inctx scopes vars na bk t c =
+  let implicit_type = is_reserved_type na t in
+  let aty = extern_typ scopes vars t in
+  let vars = add_vname vars na in
   let store, get = set_temporary_memory () in
   match na, DAst.get c with
   | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
@@ -1090,16 +1126,20 @@ and factorize_lambda inctx scopes vars na bk aty c =
       | _ -> CLambdaN ([binder],b))
      | _ -> assert false)
   | _, _ ->
-      let c = sub_extern inctx scopes vars c in
-      match c.v with
+      let c' = sub_extern inctx scopes vars c in
+      match c'.v with
       | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
-           when binding_kind_eq bk bk' && constr_expr_eq aty ty
-                && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+           when binding_kind_eq bk bk'
+                && not (occur_name na ty)  (* avoid na in ty escapes scope *)
+                && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+         let aty = if implicit_type then ty else aty in
          CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
       | CLambdaN (bl,b) ->
-         CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b)
+         let ty = if implicit_type then hole else aty in
+         CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b)
       | _ ->
-         CLambdaN ([CLocalAssum([make na],Default bk,aty)],c)
+         let ty = if implicit_type then hole else aty in
+         CLambdaN ([CLocalAssum([make na],Default bk,ty)],c')
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
@@ -1113,15 +1153,17 @@ and extern_local_binder scopes vars = function
                    Option.map (extern false scopes vars) ty) :: l)
 
     | GLocalAssum (na,bk,ty) ->
+      let implicit_type = is_reserved_type na ty in
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
           (assums,ids,CLocalAssum(nal,k,ty')::l)
-            when constr_expr_eq ty ty' &&
+            when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
                CLocalAssum(CAst.make na::nal,k,ty')::l)
         | (assums,ids,l) ->
+            let ty = if implicit_type then hole else ty in
             (na::assums,na::ids,
              CLocalAssum([CAst.make na],Default bk,ty) :: l))
 
diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
new file mode 100644
index 0000000000..824c260e92
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.out
@@ -0,0 +1,26 @@
+forall b, b = b
+     : Prop
+forall b : nat, b = b
+     : Prop
+forall b : bool, @eq bool b b
+     : Prop
+forall b : bool, b = b
+     : Prop
+forall b c : bool, b = c
+     : Prop
+forall c b : bool, b = c
+     : Prop
+forall b1 b2, b1 = b2
+     : Prop
+fun b => b = b
+     : bool -> Prop
+fix f b (n : nat) {struct n} : bool :=
+  match n with
+  | 0 => b
+  | S p => f b p
+  end
+     : bool -> nat -> bool
+∀ b c : bool, b = c
+     : Prop
+∀ b1 b2, b1 = b2
+     : Prop
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
new file mode 100644
index 0000000000..dbc83f9229
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.v
@@ -0,0 +1,37 @@
+Implicit Types b : bool.
+Check forall b, b = b.
+
+(* Check the type is not used if not the reserved one *)
+Check forall b:nat, b = b.
+
+(* Check full printing *)
+Set Printing All.
+Check forall b, b = b.
+Unset Printing All.
+
+(* Check printing of type *)
+Unset Printing Use Implicit Types.
+Check forall b, b = b.
+Set Printing Use Implicit Types.
+
+(* Check factorization: we give priority on factorization over implicit type *)
+Check forall b c, b = c.
+Check forall c b, b = c.
+
+(* Check factorization of implicit types *)
+Check forall b1 b2, b1 = b2.
+
+(* Check in "fun" *)
+Check fun b => b = b.
+
+(* Check in binders *)
+Check fix f b n := match n with 0 => b | S p => f b p end.
+
+(* Check in notations *)
+Module Notation.
+  Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+    (at level 200, x binder, y binder, right associativity,
+    format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+  Check forall b c, b = c.
+  Check forall b1 b2, b1 = b2.
+End Notation.