Default toExpr instance

Stream: general

[Arnav Sabharwal]

Is there a way to make sure Lean uses a toExpr instance I've defined myself? The involved type is as follows:

inductive PropFormula (Connective : Type) where
  | tr : PropFormula Connective
  | fls : PropFormula Connective
  | var : String → (PropFormula Connective)
  | unary : Connective → (PropFormula Connective) → (PropFormula Connective)
  | binary : Connective → (PropFormula Connective) → (PropFormula Connective) → (PropFormula Connective)
  deriving Repr, DecidableEq

inductive Conn
  | conj : Conn
  | disj : Conn
  | impl : Conn
  | neg : Conn
  | biImpl : Conn
  deriving Repr, DecidableEq

And the toExpr instance is as follows:

instance : (ToExpr Conn) where
  toExpr mt := match mt with
  | Conn.conj => .const `Conn.conj []
  | Conn.disj => .const `Conn.disj []
  | Conn.neg => .const `Conn.neg []
  | Conn.impl => .const `Conn.impl []
  | Conn.biImpl => .const `Conn.biImpl []

  toTypeExpr := (.const `Conn [])

instance [ToExpr Conn] : (ToExpr (PropFormula Conn)) where
  toTypeExpr := Expr.app (.const `PropFormula []) (.const `Conn [])

  toExpr := go where go
  | .tr => .const `PropFormula.tr []
  | .fls => .const `PropFormula.fls []
  | .var (name) => Expr.app (.const `PropFormula.var []) (Lean.ToExpr.toExpr name)
  | .unary conn op => Lean.mkApp2 (.const `PropFormula.unary []) (Lean.ToExpr.toExpr conn) (go op)
  | .binary conn op1 op2 => Lean.mkApp3 (.const `PropFormula.binary []) (Lean.ToExpr.toExpr conn) (go op1) (go op2)

What I'm currently experiencing is that Lean isn't using the aforementioned instance whilst creating its AST (explicit calls to toExpr work as expected, but the "default" mechanism for converting custom datatypes to AST seem to not work). If I could obtain some guidance in this regard, or have any conceptual flaws in my question be pointed out, it would be great!

[Sebastian Ullrich]

Yes, I believe there is a fundamental conceptual flaw. toExpr converts runtime objects to core syntax. Elaboration translates surface syntax to core syntax. These two processes are essentially disjoint, elaboration itself never creates runtime objects of the represented data.

[Sebastian Ullrich]

In other words, it would be helpful to know what you're actually trying to accomplish