Filling metavariables when given partial information

Stream: general

[Tomas Skrivan]

Let's have an expression (λ x : _, x), is there a way to turn it into (λ x : nat, x) if I know its type should be _ → nat?

My attempt:

run_cmd do
  pe ← tactic.to_expr  ``(λ x, x) tt ff,
  `(%%e : %%M → nat) ← pure pe,
  tactic.trace e

However this still prints λ (x : ?m_1), x. Is there a simple way to achieve this?

[Mario Carneiro]

run_cmd do
  let p : pexpr := ``(λ x, x),
  e ← tactic.to_expr ``(%%p : _ → nat),
  tactic.trace e

[Tomas Skrivan]

Thanks, but assuming nat → _ instead of _ → nat fails to infer the type. Why is that?

[Tomas Skrivan]

Also I would like to be able to partially infer types. E.g. for expression (λ x y, x) given it has the type _ → _ → natconcluding that it is (λ (x : nat) (y : _), x).

run_cmd do
  let p : pexpr := ``(λ x y, x),
  e ← tactic.to_expr ``(%%p : _ → _ → nat),
  tactic.trace e

[Mario Carneiro]

Lean will almost never let you write nat -> _

[Mario Carneiro]

because it produces a metavariable that depends on another variable, which doesn't unify with anything

[Mario Carneiro]

Note that lean is doing dependent type theory, even if you aren't

[Mario Carneiro]

so arrows are hard

[Mario Carneiro]

This has a slightly more comprehensible result:

run_cmd do
  let p : pexpr := ``(λ x y, x),
  expr.app (expr.app e _) _ ← tactic.to_expr ``(%%p _ _ : nat) tt tt,
  tactic.trace e

[Mario Carneiro]

and you can also do nat -> _ that way, e.g. using ``(%%p (_ : nat) _)

[Tomas Skrivan]

I see that with dependent types it gets really difficult. (You have a slight typo, there should be tactic.to_expr ... tt ff)