generating a has_coe_to_fun in a tactic

Stream: metaprogramming / tactics

[Yakov Pechersky]

How does one make this work?

import data.equiv.basic
import tactic

open tactic

set_option trace.app_builder true

example : true := by do
  try_inst ← mk_app `has_coe_to_fun [`(equiv.perm ℕ)],
  trace try_inst,
  admit

I've been trying things like:

  sic ← mk_instance_cache `(equiv.perm ℕ),
  (sic, coe_inst) ← sic.get `has_coe_to_fun,

but that get fails.

[Yakov Pechersky]

Very difficult, but there's an implicit second universe parameter, so this works:

example : true := by do
  try_inst ← pure `(has_coe_to_fun.{1 1} (equiv.perm ℕ)),
  trace try_inst,
  admit

[Simon Hudon]

get would need to generate meta universe variables for every universe that cannot be inferred from the arguments.

[Yakov Pechersky]

For some reason,

cls ← get_classes `(@equiv.{1 1} ℕ ℕ)

fails to get has_coe_to_fn too, with app builder complaining that [app_builder] failed to create an 'has_coe_to_fun'-application, there are missing implicit arguments. But what would those implicit arguments be? Another ℕ?

[Simon Hudon]

I think those would be universe parameters

[Yakov Pechersky]

For which things? Other than the already specified Sort 1 and Sort 1, what else is implicit?

[Simon Hudon]

#check @has_coe_to_fun
has_coe_to_fun : Sort u_1 → Sort (max u_1 (u_2+1))

This means that the function type that you're coercing to can be in different universes from the argument