conditional mk_instance

Stream: general

[Floris van Doorn]

I'm trying to write a small metaprogram that finds an instance of tgt : expr, and being able to use an instance of cond : expr.

For example, I might want to find an "instance" of semigroup α → has_mul α.

Here is what I tried, but the printed expressions look very wrong.

• Am I doing something wrong?
• Is there a better way of doing this?

import algebra.group.defs tactic.core
open tactic
universe variable u

open tactic
/- finds an instance of an implication `cond → tgt`.
  Returns a pair of a local constant `e` of type `cond`, and an instance of `tgt` that can mention `e`. -/
meta def mk_conditional_instance (cond tgt : expr) : tactic (expr × expr) := do
f ← mk_meta_var cond,
e ← assertv `c cond f, swap,
reset_instance_cache,
inst ← mk_instance tgt,
trace $ pformat!"({e} : {infer_type e})",
trace $ format!"raw local type of {e}: {e.local_type.to_raw_fmt}",
trace $ pformat!"({inst} : {infer_type inst})",
trace $ pformat!"({inst.bind_lambda e} : {infer_type $ inst.bind_lambda e})",
type_check inst,
return (e, inst)

set_option pp.implicit true
example {α : Type u} : unit :=
by do e ← get_local `α,
  (f, inst) ← mk_conditional_instance
    ((expr.const `semigroup [level.param `u]).app e)
    ((expr.const `has_mul [level.param `u]).app e),
  g ← mk_mapp `has_mul.mul [e, inst],
  trace pformat!"({g} : {infer_type g})",
  trace pformat!"({g.bind_lambda f} : {infer_type $ g.bind_lambda f})"

[Floris van Doorn]

I get expressions that look like

(λ (c : 1), @semigroup.to_has_mul α c : 1 → has_mul α)

Here 1 is const 1 [], which is the local_type of the local constant e.

[Floris van Doorn]

1 should be semigroup α, which is what I get if I run infer_type e (but not if I run infer_type `inst.bind_lambda e)

[Jannis Limperg]

local_type is useless precisely because of this issue. (The docs for expr mention this.) You need to use infer_type to get the type of a local const or mvar.

[Floris van Doorn]

But bind_lambda puts this useless field in my expression. What should I be using instead of bind_lambda?

[Floris van Doorn]

I don't know if my expression is incorrect, or that this is still an issue of "the pretty printer is showing the wrong thing". I suspect the former.

[Rob Lewis]

There's docs#tactic.lambdas which I believe is a tactic mode version of bind_lambda

[Floris van Doorn]

That looks a lot better. I will try that. Thanks!

[Floris van Doorn]

That indeed solved my problem.

[Jannis Limperg]

Ah that's what those variants are for! Thanks Rob, now I can kill my workaround for this issue.