diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 7f471f416f..ac69df5ff1 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -47,7 +47,7 @@ namespace Lean.Meta.DiscrTree
   2- Distinguish partial applications `f a`, `f a b`, and `f a b c`.
 -/
 
-def Key.ctorIdx : Key → Nat
+def Key.ctorIdx : Key s → Nat
   | .star     => 0
   | .other    => 1
   | .lit ..   => 2
@@ -56,17 +56,17 @@ def Key.ctorIdx : Key → Nat
   | .arrow    => 5
   | .proj ..  => 6
 
-def Key.lt : Key → Key → Bool
+def Key.lt : Key s → Key s → Bool
   | .lit v₁,      .lit v₂      => v₁ < v₂
   | .fvar n₁ a₁,  .fvar n₂ a₂  => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂)
   | .const n₁ a₁, .const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
   | .proj s₁ i₁,  .proj s₂ i₂  => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂)
   | k₁,           k₂           => k₁.ctorIdx < k₂.ctorIdx
 
-instance : LT Key := ⟨fun a b => Key.lt a b⟩
-instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
+instance : LT (Key s) := ⟨fun a b => Key.lt a b⟩
+instance (a b : Key s) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
 
-def Key.format : Key → Format
+def Key.format : Key s → Format
   | .star                   => "*"
   | .other                  => "◾"
   | .lit (Literal.natVal v) => Std.format v
@@ -76,41 +76,41 @@ def Key.format : Key → Format
   | .fvar k _               => Std.format k.name
   | .arrow                  => "→"
 
-instance : ToFormat Key := ⟨Key.format⟩
+instance : ToFormat (Key s) := ⟨Key.format⟩
 
-def Key.arity : Key → Nat
+def Key.arity : (Key s) → Nat
   | .const _ a => a
   | .fvar _ a  => a
   | .arrow     => 2
   | .proj ..   => 1
   | _          => 0
 
-instance : Inhabited (Trie α) := ⟨.node #[] #[]⟩
+instance : Inhabited (Trie α s) := ⟨.node #[] #[]⟩
 
-def empty : DiscrTree α := { root := {} }
+def empty : DiscrTree α s := { root := {} }
 
-partial def Trie.format [ToFormat α] : Trie α → Format
+partial def Trie.format [ToFormat α] : Trie α s → Format
   | .node vs cs => Format.group $ Format.paren $
     "node" ++ (if vs.isEmpty then Format.nil else " " ++ Std.format vs)
     ++ Format.join (cs.toList.map fun ⟨k, c⟩ => Format.line ++ Format.paren (Std.format k ++ " => " ++ format c))
 
-instance [ToFormat α] : ToFormat (Trie α) := ⟨Trie.format⟩
+instance [ToFormat α] : ToFormat (Trie α s) := ⟨Trie.format⟩
 
-partial def format [ToFormat α] (d : DiscrTree α) : Format :=
+partial def format [ToFormat α] (d : DiscrTree α s) : Format :=
   let (_, r) := d.root.foldl
     (fun (p : Bool × Format) k c =>
       (false, p.2 ++ (if p.1 then Format.nil else Format.line) ++ Format.paren (Std.format k ++ " => " ++ Std.format c)))
     (true, Format.nil)
   Format.group r
 
-instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩
+instance [ToFormat α] : ToFormat (DiscrTree α s) := ⟨format⟩
 
 /-- The discrimination tree ignores implicit arguments and proofs.
    We use the following auxiliary id as a "mark". -/
 private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
 private def tmpStar := mkMVar tmpMVarId
 
-instance : Inhabited (DiscrTree α) where
+instance : Inhabited (DiscrTree α s) where
   default := {}
 
 /--
@@ -240,12 +240,12 @@ we could not even compile `Init` with this setup.
 Remark: rnote it is not sufficient to just unfold reducible definitions and perform
 beta-reduction, we must also instantiate assgined metavariables, and perform zeta-reduction.
 -/
-partial def reduce (e : Expr) : MetaM Expr := do
-  let e ← whnfCore e (iota := false)
+partial def reduce (e : Expr) (simpleReduce : Bool) : MetaM Expr := do
+  let e ← whnfCore e (iota := !simpleReduce)
   match (← unfoldDefinition? e) with
-  | some e => reduce e
+  | some e => reduce e simpleReduce
   | none => match e.etaExpandedStrict? with
-    | some e => reduce e
+    | some e => reduce e simpleReduce
     | none   => return e
 
 /--
@@ -280,18 +280,18 @@ where
     | none    => return e
 
 /-- whnf for the discrimination tree module -/
-def reduceDT (e : Expr) (root : Bool) : MetaM Expr :=
-  if root then reduceUntilBadKey e else reduce e
+def reduceDT (e : Expr) (root : Bool) (simpleReduce : Bool) : MetaM Expr :=
+  if root then reduceUntilBadKey e else reduce e simpleReduce
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) := do
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key s × Array Expr) := do
   if hasNoindexAnnotation e then
     return (.star, todo)
   else
-    let e ← reduceDT e root
+    let e ← reduceDT e root (simpleReduce := s)
     let fn := e.getAppFn
-    let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do
+    let push (k : Key s) (nargs : Nat) : MetaM (Key s × Array Expr) := do
       let info ← getFunInfoNArgs fn nargs
       let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
       return (k, todo)
@@ -324,7 +324,7 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key 
     | _ =>
       return (.other, todo)
 
-partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do
+partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array (Key s)) : MetaM (Array (Key s)) := do
   if todo.isEmpty then
     return keys
   else
@@ -335,13 +335,13 @@ partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) : Met
 
 private def initCapacity := 8
 
-def mkPath (e : Expr) : MetaM (Array Key) := do
+def mkPath (e : Expr) : MetaM (Array (Key s)) := do
   withReducible do
     let todo : Array Expr := .mkEmpty initCapacity
-    let keys : Array Key  := .mkEmpty initCapacity
+    let keys : Array (Key s) := .mkEmpty initCapacity
     mkPathAux (root := true) (todo.push e) keys
 
-private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
+private partial def createNodes (keys : Array (Key s)) (v : α) (i : Nat) : Trie α s :=
   if h : i < keys.size then
     let k := keys.get ⟨i, h⟩
     let c := createNodes keys v (i+1)
@@ -352,7 +352,7 @@ private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α
 private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
   if vs.contains v then vs else vs.push v
 
-private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
+private partial def insertAux [BEq α] (keys : Array (Key s)) (v : α) : Nat → Trie α s → Trie α s
   | i, .node vs cs =>
     if h : i < keys.size then
       let k := keys.get ⟨i, h⟩
@@ -365,7 +365,7 @@ private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Tri
     else
       .node (insertVal vs v) cs
 
-def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
+def insertCore [BEq α] (d : DiscrTree α s) (keys : Array (Key s)) (v : α) : DiscrTree α s :=
   if keys.isEmpty then panic! "invalid key sequence"
   else
     let k := keys[0]!
@@ -377,12 +377,12 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTr
       let c := insertAux keys v 1 c
       { root := d.root.insert k c }
 
-def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do
+def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree α s) := do
   let keys ← mkPath e
   return d.insertCore keys v
 
-private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do
-  let e ← reduceDT e root
+private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
+  let e ← reduceDT e root (simpleReduce := s)
   match e.getAppFn with
   | .lit v         => return (.lit v, #[])
   | .const c _     =>
@@ -454,22 +454,22 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
   | _ =>
     return (.other, #[])
 
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key s × Array Expr) :=
   getKeyArgs e (isMatch := true) (root := root)
 
-private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key s × Array Expr) :=
   getKeyArgs e (isMatch := false) (root := root)
 
-private def getStarResult (d : DiscrTree α) : Array α :=
+private def getStarResult (d : DiscrTree α s) : Array α :=
   let result : Array α := .mkEmpty initCapacity
   match d.root.find? .star with
   | none                  => result
   | some (.node vs _) => result ++ vs
 
-private abbrev findKey (cs : Array (Key × Trie α)) (k : Key) : Option (Key × Trie α) :=
+private abbrev findKey (cs : Array (Key s × Trie α s)) (k : Key s) : Option (Key s × Trie α s) :=
   cs.binSearch (k, default) (fun a b => a.1 < b.1)
 
-private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
+private partial def getMatchLoop (todo : Array Expr) (c : Trie α s) (result : Array α) : MetaM (Array α) := do
   match c with
   | .node vs cs =>
     if todo.isEmpty then
@@ -489,7 +489,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
           getMatchLoop todo first.2 result
         else
           return result
-      let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
+      let visitNonStar (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
         match findKey cs k with
         | none   => return result
         | some c => getMatchLoop (todo ++ args) c.2 result
@@ -504,12 +504,12 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
       | .arrow => visitNonStar .other #[] (← visitNonStar k args result)
       | _      => visitNonStar k args result
 
-private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
+private def getMatchRoot (d : DiscrTree α s) (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
   match d.root.find? k with
   | none   => return result
   | some c => getMatchLoop args c result
 
-private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
+private def getMatchCore (d : DiscrTree α s) (e : Expr) : MetaM (Key s × Array α) :=
   withReducible do
     let result := getStarResult d
     let (k, args) ← getMatchKeyArgs e (root := true)
@@ -522,13 +522,13 @@ private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α)
 /--
   Find values that match `e` in `d`.
 -/
-def getMatch (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+def getMatch (d : DiscrTree α s) (e : Expr) : MetaM (Array α) :=
   return (← getMatchCore d e).2
 
 /--
   Similar to `getMatch`, but returns solutions that are prefixes of `e`.
   We store the number of ignored arguments in the result.-/
-partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α × Nat)) := do
+partial def getMatchWithExtra (d : DiscrTree α s) (e : Expr) : MetaM (Array (α × Nat)) := do
   let (k, result) ← getMatchCore d e
   let result := result.map (·, 0)
   if !e.isApp then
@@ -538,8 +538,8 @@ partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α 
   else
     go e.appFn! 1 result
 where
-  mayMatchPrefix (k : Key) : MetaM Bool :=
-    let cont (k : Key) : MetaM Bool :=
+  mayMatchPrefix (k : Key s) : MetaM Bool :=
+    let cont (k : Key s) : MetaM Bool :=
       if d.root.find? k |>.isSome then
         return true
       else
@@ -556,7 +556,7 @@ where
     else
       return result
 
-partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+partial def getUnify (d : DiscrTree α s) (e : Expr) : MetaM (Array α) :=
   withReducible do
     let (k, args) ← getUnifyKeyArgs e (root := true)
     match k with
@@ -567,7 +567,7 @@ partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
       | none   => return result
       | some c => process 0 args c result
 where
-  process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
+  process (skip : Nat) (todo : Array Expr) (c : Trie α s) (result : Array α) : MetaM (Array α) := do
     match skip, c with
     | skip+1, .node _  cs =>
       if cs.isEmpty then
@@ -589,7 +589,7 @@ where
             process 0 todo first.2 result
           else
             return result
-        let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
+        let visitNonStar (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
           match findKey cs k with
           | none   => return result
           | some c => process 0 (todo ++ args) c.2 result
diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean
index a8f49bbaa1..f100a857bf 100644
--- a/src/Lean/Meta/DiscrTreeTypes.lean
+++ b/src/Lean/Meta/DiscrTreeTypes.lean
@@ -10,18 +10,20 @@ namespace Lean.Meta
 /-! See file `DiscrTree.lean` for the actual implementation and documentation. -/
 
 namespace DiscrTree
-
-inductive Key where
-  | const : Name → Nat → Key
-  | fvar  : FVarId → Nat → Key
-  | lit   : Literal → Key
-  | star  : Key
-  | other : Key
-  | arrow : Key
-  | proj  : Name → Nat → Key
+/--
+Discrimination tree key. See `DiscrTree`
+-/
+inductive Key (simpleReduce : Bool) where
+  | const : Name → Nat → Key simpleReduce
+  | fvar  : FVarId → Nat → Key simpleReduce
+  | lit   : Literal → Key simpleReduce
+  | star  : Key simpleReduce
+  | other : Key simpleReduce
+  | arrow : Key simpleReduce
+  | proj  : Name → Nat → Key simpleReduce
   deriving Inhabited, BEq, Repr
 
-protected def Key.hash : Key → UInt64
+protected def Key.hash : Key s → UInt64
   | Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)
   | Key.fvar n a  => mixHash 3541 $ mixHash (hash n) (hash a)
   | Key.lit v     => mixHash 1879 $ hash v
@@ -30,16 +32,55 @@ protected def Key.hash : Key → UInt64
   | Key.arrow     => 17
   | Key.proj s i  => mixHash 11 $ mixHash (hash s) (hash i)
 
-instance : Hashable Key := ⟨Key.hash⟩
+instance : Hashable (Key s) := ⟨Key.hash⟩
 
-inductive Trie (α : Type) where
-  | node (vs : Array α) (children : Array (Key × Trie α)) : Trie α
+/--
+Discrimination tree trie. See `DiscrTree`.
+-/
+inductive Trie (α : Type) (simpleReduce : Bool) where
+  | node (vs : Array α) (children : Array (Key simpleReduce × Trie α simpleReduce)) : Trie α simpleReduce
 
 end DiscrTree
 
 open DiscrTree
 
-structure DiscrTree (α : Type) where
-  root : PersistentHashMap Key (Trie α) := {}
+/--
+Discrimination trees. It is an index from terms to values of type `α`.
+
+If `simpleReduce := true`, then only simple reduction are performed while
+indexing/retrieving terms. For example, `iota` reduction is not performed.
+
+We use `simpleReduce := false` in the type class resolution module,
+and `simpleReduce := true` in `simp`.
+
+Motivations:
+- In `simp`, we want to have `simp` theorem such as
+```
+@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
+    Quot.liftOn (Quot.mk r a) f h = f a := rfl
+```
+If we enable `iota`, then the lhs is reduced to `f a`.
+
+- During type class resolution, we often want to reduce types using even `iota`.
+Example:
+```
+inductive Ty where
+  | int
+  | bool
+
+@[reducible] def Ty.interp (ty : Ty) : Type :=
+  Ty.casesOn (motive := fun _ => Type) ty Int Bool
+
+def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
+  f x y
+
+def f (a b : Ty.bool.interp) : Ty.bool.interp :=
+  -- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
+  -- if we do not reduce `Ty.bool.interp` to `Bool`.
+  test (.==.) a b
+```
+-/
+structure DiscrTree (α : Type) (simpleReduce : Bool) where
+  root : PersistentHashMap (Key simpleReduce) (Trie α simpleReduce) := {}
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 149baa4750..05d512e944 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -9,8 +9,32 @@ import Lean.Meta.DiscrTree
 
 namespace Lean.Meta
 
+/-
+Note: we want to use iota reduction when indexing instaces. Otherwise,
+we cannot elaborate examples such as
+```
+inductive Ty where
+  | int
+  | bool
+
+@[reducible] def Ty.interp (ty : Ty) : Type :=
+  Ty.casesOn (motive := fun _ => Type) ty Int Bool
+
+def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
+  f x y
+
+def f (a b : Ty.bool.interp) : Ty.bool.interp :=
+  -- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
+  -- if we do not reduce `Ty.bool.interp` to `Bool`.
+  test (.==.) a b
+```
+See comment at `DiscrTree`.
+-/
+
+abbrev InstanceKey := DiscrTree.Key (simpleReduce := false)
+
 structure InstanceEntry where
-  keys        : Array DiscrTree.Key
+  keys        : Array InstanceKey
   val         : Expr
   priority    : Nat
   globalName? : Option Name := none
@@ -24,8 +48,10 @@ instance : ToFormat InstanceEntry where
     | some n => format n
     | _      => "<local>"
 
+abbrev InstanceTree := DiscrTree InstanceEntry (simpleReduce := false)
+
 structure Instances where
-  discrTree     : DiscrTree InstanceEntry := DiscrTree.empty
+  discrTree     : InstanceTree := DiscrTree.empty
   instanceNames : PHashSet Name := {}
   erased        : PHashSet Name := {}
   deriving Inhabited
@@ -49,7 +75,7 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
     addEntry := addInstanceEntry
   }
 
-private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
+private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
   let type ← inferType e
   withNewMCtxDepth do
     let (_, _, type) ← forallMetaTelescopeReducing type
@@ -74,7 +100,7 @@ builtin_initialize
       modifyEnv fun env => instanceExtension.modifyState env fun _ => s
   }
 
-def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
+def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry (simpleReduce := false)) :=
   return Meta.instanceExtension.getState (← getEnv) |>.discrTree
 
 def getErasedInstances : CoreM (PHashSet Name) :=
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 3cc8781d19..f0862794d1 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -134,7 +134,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
 /--
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
-def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
+def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
   let candidates ← s.getMatchWithExtra e
   if candidates.isEmpty then
     trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 819fbac9fe..87cea99d20 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -50,6 +50,19 @@ def Origin.key : Origin → Name
 instance : BEq Origin := ⟨(·.key == ·.key)⟩
 instance : Hashable Origin := ⟨(hash ·.key)⟩
 
+/-
+Note: we want to use iota reduction when indexing instaces. Otherwise,
+we cannot use simp theorems such as
+```
+@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
+    Quot.liftOn (Quot.mk r a) f h = f a := rfl
+```
+If we use `iota`, then the lhs is reduced to `f a`.
+See comment at `DiscrTree`.
+-/
+
+abbrev SimpTheoremKey := DiscrTree.Key (simpleReduce := true)
+
 /--
   The fields `levelParams` and `proof` are used to encode the proof of the simp theorem.
   If the `proof` is a global declaration `c`, we store `Expr.const c []` at `proof` without the universe levels, and `levelParams` is set to `#[]`
@@ -60,7 +73,7 @@ instance : Hashable Origin := ⟨(hash ·.key)⟩
   Then, we use `abstractMVars` to abstract the universe metavariables and create new fresh universe parameters that are stored at the field `levelParams`.
 -/
 structure SimpTheorem where
-  keys        : Array DiscrTree.Key := #[]
+  keys        : Array SimpTheoremKey := #[]
   /--
     It stores universe parameter names for universe polymorphic proofs.
     Recall that it is non-empty only when we elaborate an expression provided by the user.
@@ -137,9 +150,11 @@ def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : S
 instance : BEq SimpTheorem where
   beq e₁ e₂ := e₁.proof == e₂.proof
 
+abbrev SimpTheoremTree := DiscrTree SimpTheorem (simpleReduce := true)
+
 structure SimpTheorems where
-  pre          : DiscrTree SimpTheorem := DiscrTree.empty
-  post         : DiscrTree SimpTheorem := DiscrTree.empty
+  pre          : SimpTheoremTree := DiscrTree.empty
+  post         : SimpTheoremTree := DiscrTree.empty
   lemmaNames   : PHashSet Origin := {}
   toUnfold     : PHashSet Name := {}
   erased       : PHashSet Origin := {}
@@ -202,7 +217,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | s, t => return s == t
 
 private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
-  let lhs ← DiscrTree.reduceDT lhs (root := true)
+  let lhs ← DiscrTree.reduceDT lhs (root := true) (simpleReduce := true)
   if lhs == rhs && lhs.isFVar then
     throwError "invalid `simp` theorem, equation is equivalent to{indentExpr (← mkEq lhs rhs)}"
 
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 9d2a8384f8..19e7247f02 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -10,13 +10,17 @@ import Lean.Meta.SynthInstance
 
 namespace Lean.Meta
 
+abbrev UnificationHintKey := DiscrTree.Key (simpleReduce := true)
+
 structure UnificationHintEntry where
-  keys        : Array DiscrTree.Key
+  keys        : Array UnificationHintKey
   val         : Name
   deriving Inhabited
 
+abbrev UnificationHintTree := DiscrTree Name (simpleReduce := true)
+
 structure UnificationHints where
-  discrTree       : DiscrTree Name := DiscrTree.empty
+  discrTree : UnificationHintTree := DiscrTree.empty
   deriving Inhabited
 
 instance : ToFormat UnificationHints where
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index 1c227f9399..b5bed1dff2 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -32,7 +32,7 @@ def succ := mkConst `Nat.succ
 def add  := mkAppN (mkConst `Add.add [levelZero]) #[nat, mkConst `Nat.add]
 
 def tst1 : MetaM Unit :=
-do let d : DiscrTree Nat := {};
+do let d : DiscrTree Nat true := {};
    let mvar ← mkFreshExprMVar nat;
    let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
    let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;
diff --git a/tests/lean/run/stuckTC.lean b/tests/lean/run/stuckTC.lean
index ec65d2c100..ef58060470 100644
--- a/tests/lean/run/stuckTC.lean
+++ b/tests/lean/run/stuckTC.lean
@@ -45,6 +45,12 @@ inductive Ty where
 @[reducible] def Ty.interp (ty : Ty) : Type :=
   Ty.casesOn (motive := fun _ => Type) ty Int Bool
 
+/-
+The discrimination tree module does not perform iota reduction. Thus, it does
+not reduce the definition above, and we cannot synthesize `BEq Ty.bool.interp`.
+We can workaround using `match` as in the ex
+-/
+
 def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
   f x y