[Merged by Bors] - feat(simps): improve error messages

src/tactic/simps.lean

@@ -14,11 +14,11 @@ reducing a definition when projections are applied to it.
 
 There are three attributes being defined here
 * `@[simps]` is the attribute for objects of a structure or instances of a class. It will
-  automatically generate simplication lemmas for each projection of the object/instance that contains
-  data. See the doc strings for `simps_attr` and `simps_cfg` for more details and configuration
-  options
+  automatically generate simplification lemmas for each projection of the object/instance that
+  contains data. See the doc strings for `simps_attr` and `simps_cfg` for more details and
+  configuration options.
 * `@[_simps_str]` is automatically added to structures that have been used in `@[simps]` at least
-  once. They contain the data of the projections used for this structure by all following
+  once. This attribute contains the data of the projections used for this structure by all following
   invocations of `@[simps]`.
 * `@[notation_class]` should be added to all classes that define notation, like `has_mul` and
   `has_zero`. This specifies that the projections that `@[simps]` used are the projections from
@@ -112,7 +112,8 @@ meta def simps_get_raw_projections (e : environment) (str : name) :
     when_tracing `simps.verbose trace!"[simps] > found projection information for structure {str}",
     simps_str_attr.get_param str
   else do
-    when_tracing `simps.verbose trace!"[simps] > generating projection information for structure {str}:",
+    when_tracing `simps.verbose trace!
+      "[simps] > generating projection information for structure {str}:",
     d_str ← e.get str,
     projs ← e.structure_fields_full str,
     let raw_univs := d_str.univ_params,
@@ -123,10 +124,21 @@ meta def simps_get_raw_projections (e : environment) (str : name) :
       custom_proj ← (do
         decl ← e.get (str ++ `simps ++ proj.last),
         let custom_proj := decl.value.instantiate_univ_params $ decl.univ_params.zip raw_levels,
-        when_tracing `simps.verbose trace!"[simps] > found custom projection for {proj}:\n        > {custom_proj}",
+        when_tracing `simps.verbose trace!
+          "[simps] > found custom projection for {proj}:\n        > {custom_proj}",
         return custom_proj) <|> return raw_expr,
       is_def_eq custom_proj raw_expr <|>
-        fail!"Invalid custom projection:\n {custom_proj}\nExpression is not definitionally equal to {raw_expr}.",
+        -- if the type of the expression is different, we show a different error message, because
+        -- that is more likely going to be helpful.
+        do {
+          custom_proj_type ← infer_type custom_proj,
+          raw_expr_type ← infer_type raw_expr,
+          b ← succeeds (is_def_eq custom_proj_type raw_expr_type),
+          if b then fail!"Invalid custom projection:\n  {custom_proj}
+Expression is not definitionally equal to {raw_expr}."
+          else fail!"Invalid custom projection:\n  {custom_proj}
+Expression has different type than {raw_expr}. Given type:\n  {custom_proj_type}
+Expected type:\n  {raw_expr_type}" },
       return custom_proj),
     /- Check for other coercions and type-class arguments to use as projections instead. -/
     (args, _) ← open_pis d_str.type,
@@ -143,7 +155,8 @@ meta def simps_get_raw_projections (e : environment) (str : name) :
         (hyp, e_inst) ← try_for 1000 (mk_conditional_instance e_str e_inst_type),
         raw_expr ← mk_mapp proj_nm [args.head, e_inst],
         clear hyp,
-        raw_expr_lambda ← lambdas [hyp] raw_expr, -- `expr.bind_lambda` doesn't give the correct type
+        -- Note: `expr.bind_lambda` doesn't give the correct type
+        raw_expr_lambda ← lambdas [hyp] raw_expr,
         return (raw_expr, raw_expr_lambda.lambdas args))
       else (do
         e_inst_type ← to_expr ((expr.const class_nm []).app (pexpr.of_expr e_str)),
@@ -156,9 +169,11 @@ meta def simps_get_raw_projections (e : environment) (str : name) :
         not been overrriden by the user. -/
       guard (projs.any (= relevant_proj) ∧ ¬ e.contains (str ++ `simps ++ relevant_proj.last)),
       let pos := projs.find_index (= relevant_proj),
-      when_tracing `simps.verbose trace!"        > using function {proj_nm} instead of the default projection {relevant_proj.last}.",
+      when_tracing `simps.verbose trace!
+        "        > using {proj_nm} instead of the default projection {relevant_proj.last}.",
       return $ raw_exprs.update_nth pos lambda_raw_expr) <|> return raw_exprs) raw_exprs,
-    when_tracing `simps.verbose trace!"[simps] > generated projections for {str}:\n        > {raw_exprs}",
+    when_tracing `simps.verbose trace!
+      "[simps] > generated projections for {str}:\n        > {raw_exprs}",
     simps_str_attr.set str (raw_univs, raw_exprs) tt,
     return (raw_univs, raw_exprs)
 
@@ -222,7 +237,8 @@ meta def simps_get_projection_exprs (e : environment) (tgt : expr)
     projections are applied in a lemma. When this is `ff` (default) all projection names will be
     appended to the definition name to form the lemma name, and when this is `tt`, only the
     last projection name will be appended.
-  * if `simp_rhs` is `tt` then the right-hand-side of the generated lemmas will be put simp-normal form
+  * if `simp_rhs` is `tt` then the right-hand-side of the generated lemmas will be put in simp-normal
+    form.
   * `type_md` specifies how aggressively definitions are unfolded in the type of expressions
     for the purposes of finding out whether the type is a function type.
     Default: `instances`. This will unfold coercion instances (so that a coercion to a function type
@@ -256,7 +272,8 @@ meta def simps_add_projection (nm : name) (type lhs rhs : expr) (args : list exp
   let decl_type := eq_ap.pis args,
   let decl_value := prf.lambdas args,
   let decl := declaration.thm decl_name univs decl_type (pure decl_value),
-  when_tracing `simps.verbose trace!"[simps] > adding projection\n        > {decl_name} : {decl_type}",
+  when_tracing `simps.verbose trace!
+    "[simps] > adding projection\n        > {decl_name} : {decl_type}",
   decorate_error ("failed to add projection lemma " ++ decl_name.to_string ++ ". Nested error:") $
     add_decl decl,
   b ← succeeds $ is_def_eq lhs rhs,
@@ -332,17 +349,21 @@ meta def simps_add_projections : ∀(e : environment) (nm : name) (suffix : stri
               ff cfg new_todo
     else do
       when must_be_str $
-        fail!"Invalid `simps` attribute. The body is not a constructor application:\n{rhs_ap}\nPossible solution: add option {{rhs_md := semireducible}.",
+        fail!"Invalid `simps` attribute. The body is not a constructor application:\n{rhs_ap}
+Possible solution: add option {{rhs_md := semireducible}.",
       when (todo_next ≠ []) $
-        fail!"Invalid simp-lemma {nm.append_suffix $ suffix ++ todo_next.head}. The given definition is not a constructor application:\n{rhs_ap}\nPossible solution: add option {{rhs_md := semireducible}.",
+        fail!"Invalid simp-lemma {nm.append_suffix $ suffix ++ todo_next.head}.
+The given definition is not a constructor application:\n  {rhs_ap}
+Possible solution: add option {{rhs_md := semireducible}.",
       if cfg.fully_applied then
         simps_add_projection new_nm tgt lhs_ap rhs_ap new_args univs cfg else
         simps_add_projection new_nm type lhs rhs args univs cfg
   else do
     when must_be_str $
       fail "Invalid `simps` attribute. Target is not a structure",
     when (todo_next ≠ [] ∧ str ∉ [`prod, `pprod]) $
-        fail!"Invalid simp-lemma {nm.append_suffix $ suffix ++ todo_next.head}. Projection {(todo_next.head.split_on '_').tail.head} doesn't exist, because target is not a structure.",
+        fail!"Invalid simp-lemma {nm.append_suffix $ suffix ++ todo_next.head}.
+Projection {(todo_next.head.split_on '_').tail.head} doesn't exist, because target is not a structure.",
     if cfg.fully_applied then
       simps_add_projection new_nm tgt lhs_ap rhs_ap new_args univs cfg else
       simps_add_projection new_nm type lhs rhs args univs cfg

test/simps.lean

@@ -1,5 +1,6 @@
 import tactic.simps
 
+universe variables v u w
 -- set_option trace.simps.verbose true
 -- set_option trace.app_builder true
 
@@ -233,14 +234,16 @@ run_cmd do
   guard $ 12 = e.fold 0 -- there are no other lemmas generated
     (λ d n, n + if d.to_name.components.init.ilast = `specify then 1 else 0),
   success_if_fail_with_msg (simps_tac `specify.specify1 {} ["fst_fst"])
-    "Invalid simp-lemma specify.specify1_fst_fst. Projection fst doesn't exist, because target is not a structure.",
+    "Invalid simp-lemma specify.specify1_fst_fst.
+Projection fst doesn't exist, because target is not a structure.",
   success_if_fail_with_msg (simps_tac `specify.specify1 {} ["foo_fst"])
     "Invalid simp-lemma specify.specify1_foo_fst. Projection foo doesn't exist.",
   success_if_fail_with_msg (simps_tac `specify.specify1 {} ["snd_bar"])
     "Invalid simp-lemma specify.specify1_snd_bar. Projection bar doesn't exist.",
   success_if_fail_with_msg (simps_tac `specify.specify5 {} ["snd_snd"])
-    "Invalid simp-lemma specify.specify5_snd_snd. The given definition is not a constructor application:
-prod.map (λ (x : ℕ), x) (λ (y : ℕ), y) (2, 3)
+    "Invalid simp-lemma specify.specify5_snd_snd.
+The given definition is not a constructor application:
+  prod.map (λ (x : ℕ), x) (λ (y : ℕ), y) (2, 3)
 Possible solution: add option {rhs_md := semireducible}."
 
 
@@ -308,7 +311,6 @@ run_cmd do
   e.get `pprod_equiv_prod_inv_fun_snd
 
 /- Tests with universe levels -/
-universe variables v u
 class has_hom (obj : Type u) : Type (max u (v+1)) :=
 (hom : obj → obj → Type v)
 
@@ -478,23 +480,30 @@ def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm
 @[simps {simp_rhs := tt}] protected def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
 
+example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : γ) : (e₁.trans e₂).symm x = e₁.symm (e₂.symm x) :=
+by simp only [equiv.trans_inv_fun]
+
 end manual_coercion
 
-namespace failty_manual_coercion
-variables {α β γ : Sort*}
+namespace faulty_manual_coercion
 
 structure equiv (α : Sort*) (β : Sort*) :=
 (to_fun    : α → β)
 (inv_fun   : β → α)
 
-local infix ` ≃ `:25 := failty_manual_coercion.equiv
+local infix ` ≃ `:25 := faulty_manual_coercion.equiv
+
+variables {α β γ : Sort*}
 
 /-- See Note [custom simps projection] -/
 noncomputable def equiv.simps.inv_fun (e : α ≃ β) : β → α := classical.choice ⟨e.inv_fun⟩
 
-run_cmd do e ← get_env, success_if_fail (simps_get_raw_projections e `faulty_manual_coercion.equiv)
+run_cmd do e ← get_env, success_if_fail_with_msg (simps_get_raw_projections e `faulty_manual_coercion.equiv)
+"Invalid custom projection:
+  λ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β), classical.choice _
+Expression is not definitionally equal to equiv.inv_fun."
 
-end failty_manual_coercion
+end faulty_manual_coercion
 
 namespace manual_initialize
 /- defining a manual coercion. -/
@@ -524,6 +533,59 @@ run_cmd has_attribute `_simps_str `manual_initialize.equiv
 
 end manual_initialize
 
+namespace faulty_universes
+
+variables {α β γ : Sort*}
+
+structure equiv (α : Sort u) (β : Sort v) :=
+(to_fun    : α → β)
+(inv_fun   : β → α)
+
+local infix ` ≃ `:25 := faulty_universes.equiv
+
+instance : has_coe_to_fun $ α ≃ β := ⟨_, equiv.to_fun⟩
+
+def equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun⟩
+
+/-- See Note [custom simps projection] -/
+-- test: intentionally using different names for the universe variables for equiv.symm than for
+-- equiv
+def equiv.simps.inv_fun {α : Type u} {β : Type v} (e : α ≃ β) : β → α := e.symm
+
+run_cmd do e ← get_env,
+  success_if_fail_with_msg (simps_get_raw_projections e `faulty_universes.equiv)
+"Invalid custom projection:
+  λ {α : Type u} {β : Type v} (e : α ≃ β), ⇑(e.symm)
+Expression has different type than equiv.inv_fun. Given type:
+  Π {α : Type u} {β : Type v} (e : α ≃ β), has_coe_to_fun.F e.symm
+Expected type:
+  Π {α : Sort u} {β : Sort v}, α ≃ β → β → α"
+
+end faulty_universes
+
+namespace manual_universes
+
+variables {α β γ : Sort*}
+
+structure equiv (α : Sort u) (β : Sort v) :=
+(to_fun    : α → β)
+(inv_fun   : β → α)
+
+local infix ` ≃ `:25 := manual_universes.equiv
+
+instance : has_coe_to_fun $ α ≃ β := ⟨_, equiv.to_fun⟩
+
+def equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun⟩
+
+/-- See Note [custom simps projection] -/
+-- test: intentionally using different unvierse levels for equiv.symm than for equiv
+def equiv.simps.inv_fun {α : Sort w} {β : Sort u} (e : α ≃ β) : β → α := e.symm
+
+-- check whether we can generate custom projections even if the universe names don't match
+initialize_simps_projections equiv
+
+end manual_universes
+
 -- test transparency setting
 structure set_plus (α : Type) :=
 (s : set α)
@@ -591,6 +653,7 @@ end
 
 end nested_non_fully_applied
 
+
 /- fail if you add an attribute with a parameter. -/
 run_cmd success_if_fail $ simps_tac `foo.rfl { attrs := [`higher_order] }