Magically assign mvar by unification

Stream: general

[Marcus Rossel]

Is there some way to have Lean magically determine a correct value for ?m in the #eval?

import Lean
open Lean Meta Elab Term

inductive Rel where
  | eq
  | iff

abbrev Rel.dom : Rel → Type _ → Type _
  | eq,  α => α
  | iff, _ => Prop

/-
`Rel.mk` is supposed to represent either `Eq` of `Iff` depending on the value of the `Rel` argument.
That is:
* Rel.mk .eq  x y ≡ Eq  x y
* Rel.mk .iff p q ≡ Iff p q
-/
abbrev Rel.mk : (rel : Rel) → rel.dom α → rel.dom α → Prop
  | eq  => Eq
  | iff => Iff

/- prints:
e₁: false
e₂: true
-/
#eval do
  let tgt ← elabTerm (← `(True = False)) none

  let e₁ ← elabTerm (← `(Rel.mk ?m True False)) none
  withAssignableSyntheticOpaque do logInfo m!"e₁: {← isDefEq e₁ tgt}"

  let e₂ ← elabTerm (← `(Rel.mk .eq True False)) none
  withAssignableSyntheticOpaque do logInfo m!"e₂: {← isDefEq e₂ tgt}"

That is, is there a way to get it to print e₁: true?

[Mario Carneiro]

that's not normally how unification works, it won't try to guess rel in that context. However, a unification hint might work there

[Mario Carneiro]

There are other ways to set it up via typeclasses so that it will work things out in that direction

[Mario Carneiro]

class ToRel (α : Type) (rel : outParam Rel) where
  relMk : α → α → Prop
  relMk_eq : (⟨_, relMk⟩ : Σ α, α → α → Prop) = ⟨rel.dom α, rel.mk⟩

instance : ToRel α .eq where
  relMk := Eq
  relMk_eq := rfl

instance : ToRel Prop .iff where
  relMk := Iff
  relMk_eq := rfl

example : ToRel.relMk True False = (True ↔ False) := rfl
example : ToRel.relMk 0 1 = (0 = 1) := rfl

[Mario Carneiro]

Here's the unification hint version:

unif_hint (rel : Rel) (α : Type) where rel ≟ .iff ⊢ rel.dom α ≟ Prop
unif_hint (rel : Rel) (α : Type) where rel ≟ .eq ⊢ rel.dom α ≟ α

#check Rel.mk _ True False -- Rel.iff.mk True False : Prop
#check Rel.mk _ 0 1        -- Rel.eq.mk 0 1 : Prop

[Marcus Rossel]

Thanks! Unfortunately, the approaches you give don't quite capture the behaviour I need. I don't want Props to always be related by ↔, but instead for the procedure to figure out whether it needs ↔ or = depending on the term it's unifying with. So for example:

example : ToRel.relMk True False = (True = False) := rfl -- fails

... should also work and infer rel := .eq.
(Similar problem when using the given unification hints.)