Force reduction of type

Stream: lean4

[Marcus Rossel]

When using dependent types, is there a way to force Lean to reduce a given type?
For example:

class Typable (α) where
  type : α → Type

open Typable

inductive Var
  | a
  | b

instance : Typable Var where
  type
    | .a => Nat
    | .b => String

example (x : type Var.a) : Nat :=
  x + 1 -- Error

Here x + 1 doesn't work because:

failed to synthesize instance
  HAdd (type Var.a) Nat ?m.651

That is, Lean doesn't "see through" type Var.a being Nat. Is there a way I can help/force Lean to see this?

[Jannis Limperg]

This works:

class Typable (α) where
  type : α → Type

attribute [reducible] Typable.type

open Typable

inductive Var
  | a
  | b

@[reducible]
instance typableVar : Typable Var where
  type
    | .a => Nat
    | .b => String

example (x : type Var.a) : Nat :=
  x + 1

In general, typeclass resolution only unfolds reducible definitions.