feat: new deriving framework

[Rob23oba]

This PR adds a new framework for deriving handlers that uses MetaM operations directly instead of going through syntax.

The new framework is currently unused but will soon become used for the new deriving handlers for BEq, Ord and DecidableEq in #14929 and more in the future. The test derivingMeta.lean however already shows how the framework is meant to be used and what is is capable of.

Depends on: #15318, #15319

[TwoFX]

Just an extremely superficial first look, actual comments will follow tomorrow.

[TwoFX]

Right now this framework would be really difficult to use for a new user owing to the lack of documentation. I think it would be very helpful to have docstrings on all of the functions that you expect users of the framework to actually call. Ideally these would have examples.

I'm sure that the reference manual should cover things like this in the future, but probably not yet.

[TwoFX]

This is really cool!

[TwoFX]

needSucc desperately needs a better name, but given that for every class there is at most one setting that actually works, I think it would be even better if the value was derived from the class. This should be possible if we pass the name of the class here?

[TwoFX]

Relatedly, there are classes like Lean.Server.RpcEncodable which take (α : Type). This one currently has a syntax-based deriving handler which will successfully derive RpcEncodable for a universe-polymorphic type, fixing universes as appropriate, but your framework cannot do it (i.e., it will send something to the kernel which will not typecheck).

[Rob23oba]

Having the class name available is probably anyways good for error messages; but I'm not sure if mkInductiveDerivingHandler should really assume anything about the shape of the class. Maybe it'd be more reasonable to provide a "level shape" to the function instead of a simple boolean which would more or less just be a function (lvl : Level) -> (levelParams : List Name) -> List Level. Then we could have simple implementations for .sortU, .typeU, .type and .prop.

Edit: I have implemented such a change now, what do you think?

[TwoFX]

Have you considered supporting classes which have multiple fields which are all of the correct shape? Not sure how often that comes up.

[Rob23oba]

It would certainly be nice to support ToExpr with this, yes; but since I added makeInstancesUsingMutualPartialBlock this is essentially a plumbing function covering the simple case of Repr / Hashable / ToJson. So it might make more sense to instead add more API for conveniently creating InstanceInfos to cover more complicated cases.

[TwoFX]

Almost all deriving handlers which cannot use deriveTransformationInstPerConstructor will still have to do the case splitting on the constructor, so perhaps it would make sense to factor out another helper here? Maybe something like def mkMatchFun (induct : Name) (resultType : Expr) (alt : ConstructorVal → Array Expr → DerivingM Expr) : DerivingM Expr?

[Rob23oba]

Sure! I made it monad-generic too (maybe there is a better place for it, though?)

[TwoFX]

Right now the state just monotonically collects instance hypotheses, so even if I have declarations in my mutual block which would require fewer hypotheses than some other declarations in the block, they get the full list of hypotheses. You can do set ({} : Deriving.State) in your handler for every inductive, but that is pretty terrible. Perhaps it would be good to offer a combinator which does this properly. To give an example:

module

public import Lean

open Lean Meta Elab Deriving

-- Clone of `Inhabited`
class Default (α : Sort u) where
  default : α

instance : Default Nat := ⟨0⟩
instance : Default String := ⟨""⟩
instance : Default (List α) := ⟨[]⟩
instance [Default β] : Default (α → β) := ⟨fun _ => Default.default⟩

def nonRecursiveCtor? (indVal : InductiveVal) : DerivingM (Option ConstructorVal) :=
  indVal.ctors.findSomeM? fun ctor => do
    let ctorVal ← getConstInfoCtor ctor
    forallTelescope ctorVal.type fun xs _ => do
      for x in xs[indVal.numParams...*] do
        if ← containsRecursiveDecl (← inferType x) then
          return none
      return some ctorVal

def defaultHandler : DerivingHandler :=
  mkInductiveDerivingHandler (needSucc := false) do
    let ctx ← read
    for name in ctx.names do
      set ({} : Deriving.State)
      let indVal ← getConstInfoInduct name
      unless indVal.numIndices = 0 do
        return false
      let some ctorVal ← nonRecursiveCtor? indVal
        | throwError "no non-recursive constructor for {.ofConstName name}"
      let typeApp := mkAppN (.const name ctx.lparams) ctx.indParams
      let mut val := mkAppN (.const ctorVal.name ctx.lparams) ctx.indParams
      for _ in 0...ctorVal.numFields do
        let .forallE _ fieldTy _ _ ← whnf (← inferType val)
          | throwError "unexpected constructor type"
        let u ← getLevel fieldTy
        let inst ← synthInstanceDeriving (mkApp (.const ``Default [u]) fieldTy)
        val := mkApp val (mkApp2 (.const ``Default.default [u]) fieldTy inst)
      let hyps ← produceInstanceHyps
      mkInstanceForDeriving hyps
        (mkApp (.const ``Default [ctx.indLevel]) typeApp)
        (mkApp2 (.const ``Default.mk [ctx.indLevel]) typeApp val)
    return true

mutual
  inductive LA (α β : Type) where | base (a : α) | step (b : LB α β)
  inductive LB (α β : Type) where | base (b : β) | step (a : LA α β)
end

run_cmd defaultHandler #[``LA, ``LB]

#check instDefaultLA -- instDefaultLA (α β : Type) [Default α] : Default (LA α β)
#check instDefaultLB -- instDefaultLB (α β : Type) [Default β] : Default (LB α β)

If we remove the set, we get instDefaultLB (α β : Type) [Default α] [Default β] : Default (LB α β) instead.

[Rob23oba]

I have considered making produceInstanceHyps reset the state; does that sound reasonable?

[TwoFX]

Suggested change

	msg := msg ++ .hint' m!"Multiple instance candidates usually indicates that one of the \
	msg := msg ++ .hint' m!"Multiple instance candidates usually indicate that one of the \

[Rob23oba]

I have changed the wording slightly differently. Does it sound right now?

[TwoFX]

Right now we get the same binders as the class, which is different from what the syntactic framework does (it makes type parameters implicit).

[Rob23oba]

I made it replace explicit binder infos with implicit ones per default, but added an option if this turns out to be undesirable for anyone (I've seen discussions about whether we should or shouldn't use implicits, so this allows anyone to choose to use either if they want to).