diff options
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2733.v | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 6 |
2 files changed, 10 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v index 60c371934..832de4f91 100644 --- a/test-suite/bugs/closed/shouldsucceed/2733.v +++ b/test-suite/bugs/closed/shouldsucceed/2733.v @@ -1,5 +1,8 @@ Unset Asymmetric Patterns. +Definition goodid : forall {A} (x: A), A := fun A x => x. +Definition wrongid : forall A (x: A), A := fun {A} x => x. + Inductive ty := N | B. Inductive alt_list : ty -> ty -> Type := @@ -21,4 +24,5 @@ alt_list t1 t3 := | Bcons b l1 => fun _ l2 => Bcons b (app (@P) l1 l2) end. -Check (fun {t t'} (l: alt_list t t') => app trullynul l nil). +Check (fun {t t'} (l: alt_list t t') => + app trullynul (goodid l) (wrongid _ nil)). diff --git a/toplevel/command.ml b/toplevel/command.ml index 9deaa270f..5aef9ec66 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -85,7 +85,11 @@ let interp_definition bl red_option c ctypopt = let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in - imps1@(Impargs.lift_implicits nb_args imps2), + (* Check that all implicit arguments inferable from the term is inferable from the type *) + if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false) + then warn (str "Implicit arguments declaration relies on type." ++ + spc () ++ str "The term declares more implicits than the type here."); + imps1@(Impargs.lift_implicits nb_args impsty), { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; |