why is this happening

Stream: general

[Koundinya Vajjha]

open tactic expr

meta def wat : tactic unit :=
do ctx ← local_context,
  let a := app ctx.head (list.reverse ctx).head,
  type ← infer_type a,
  trace type,
  skip

lemma begins  (f : ℕ → ℕ) (a : bool) : Prop :=
begin
wat,  -- returns ℕ
end

But

variables (a : bool) (g : ℕ  → ℕ )
#check g a

returns a type mismatch error?

[Kenny Lau]

namespace tactic.interactive
open tactic lean.parser interactive expr
meta def wat : tactic unit :=
do ctx ← local_context,
  let a := app ctx.head (list.reverse ctx).head,
  type ← infer_type a,
  trace type,
  skip
end tactic.interactive

lemma begins  (f : ℕ → ℕ) (a : bool) : Prop :=
begin
wat,  -- returns ℕ
end

[Kenny Lau]

more info:

namespace tactic.interactive
open tactic lean.parser interactive expr
meta def wat : tactic unit :=
do ctx ← local_context,
  let a := app ctx.head (list.reverse ctx).head,
  type ← infer_type a,
  tactic.interactive.let none none ``(%%a),
  skip
end tactic.interactive

lemma begins  (f : ℕ → ℕ) (a : bool) : Prop :=
begin
wat,
sorry
end

tactic state after wat:

f : ℕ → ℕ,
a : bool,
this : ℕ := f a
⊢ Prop

and error message of lemma after I put sorry:

type mismatch at application
  f a
term
  a
has type
  bool
but is expected to have type
  ℕ

[Reid Barton]

You manually built an expr= supposedly fully elaborated expression, but the expr you constructed is not actually valid. I guess that infer_type assumes the expression is valid and then according to the typing rules its type must be the return type of f. You didn't get an error because you didn't do anything with the expr.

[Rob Lewis]

Yeah, infer_type doesn't completely type check the expression, otherwise it would be very expensive. There's another tactic called type_check that should fail if you call it on a.

[Reid Barton]

If you used tactic.exact a (supposing you change the goal to nat) then I imagine the tactic would succeed but then you would get a type error at a later stage.

[Koundinya Vajjha]

@Reid Barton yeah seems like that's what is happening.

[Kenny Lau]

well it's meta so it can be unsound anyway

[Koundinya Vajjha]

type_check is exactly what I needed.

[Kenny Lau]

you aren't actually changing the partially generated proof by trace

[Rob Lewis]

In general, making applications manually can be difficult. Do it if you're confident in what you're doing, since it will be more efficient. Otherwise mk_app and mk_mapp are your friends. In particular the error messages will be more helpful.

[Koundinya Vajjha]

I'm having trouble figuring out how to use mk_app. I have f : ℕ → ℝ and b : ℕ. How do I use this to make the application f b?

[Kenny Lau]

namespace tactic.interactive
open tactic lean.parser interactive expr
meta def wat : tactic unit :=
do ctx ← local_context,
  let a := expr.mk_app ctx.head [ctx.reverse.head],
  tactic.type_check a,
  type ← infer_type a,
  trace type,
  tactic.interactive.let none none ``(%%a),
  skip
end tactic.interactive

lemma begins  (f : ℕ → ℕ) (a : ℕ) : ℕ :=
begin
wat,  -- returns ℕ
end

[Koundinya Vajjha]

Okay that was silly. Thanks @Kenny Lau