Dependent instance derivation

Stream: new members

[Johannes Tantow]

Hi,
when defining a new type via inductive I can ask Lean to automatically derive instances for type classes as in the example below:

section Basic
  structure Signature where
    (constants: Type u)
    (vars: Type u)
    (relationSymbols: Type w)
    (relationArity: relationSymbols → ℕ)

  inductive Term (τ: Signature) [DecidableEq τ.vars] [DecidableEq τ.relationSymbols] [DecidableEq τ.constants] [Hashable τ.constants] [Hashable τ.vars] [Hashable τ.relationSymbols] where
  | constant : τ.constants → Term τ
  | variableDL : τ.vars → Term τ
  deriving DecidableEq, Hashable
end Basic

This works perfectly well, but I dislike the cluttering with all the typeclasses as I only need hashable in very few functions, but have to state it everywhere to use my type. I would like to only specify the instances for e.g. τ.constantsin the functions where I actually need them.
Is there a way to tell Lean to only derive this instance if possible e.g. so that the following works:

  def isConstant {τ: Signature} (t: Term τ): Bool :=
    match t with
    |.constant _ => True
    |.variableDL _ => False

  def bothAreEqual {τ: Signature} [DecidableEq τ.vars] [DecidableEq τ.relationSymbols] [DecidableEq τ.constants] [Hashable τ.constants] [Hashable τ.vars] [Hashable τ.relationSymbols] (t1 t2: Term τ): Bool :=
  t1 = t2

[Johannes Tantow]

I can probably solve it by writing my own functions for it, but this has limits. I think I am able to write a good function to decide equality, but I am not so certain that I can write a good hash function for defined objects.

[Henrik Böving]

From office hours:

instance {τ : Signature} [DecidableEq τ.vars] [DecidableEq τ.constants] : DecidableEq (Term τ) :=
  fun l r =>
    match l, r with
    | .constant .., .variableDL .. => .isFalse (by simp)
    | .variableDL .., .constant .. => .isFalse (by simp)
    | .constant cs, .constant cs' =>
      if h : cs = cs' then
        .isTrue (by simp [h])
      else
        .isFalse (by simp [h])
    | .variableDL cs, .variableDL cs' =>
      if h : cs = cs' then
        .isTrue (by simp [h])
      else
        .isFalse (by simp [h])

[Henrik Böving]

set_option trace.Elab.Deriving.hashable true
inductive Term' where
  | constant : Nat → Term'
  | variableDL : String → Term'
  deriving Hashable