diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 5ddc047415..d9e11f2ada 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -712,6 +712,8 @@ where
       checkLetRecsToLiftTypes funFVars letRecsToLift
       withUsed vars headers values letRecsToLift fun vars => do
         let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+        for preDef in preDefs do
+          trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
         let preDefs ← levelMVarToParamPreDecls preDefs
         let preDefs ← instantiateMVarsAtPreDecls preDefs
         let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index d8541cacb4..eea29d2920 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -9,6 +9,7 @@ import Lean.Meta.Basic
 import Lean.Meta.Instances
 import Lean.Meta.AbstractMVars
 import Lean.Meta.WHNF
+import Lean.Meta.Check
 import Lean.Util.Profile
 
 namespace Lean.Meta
@@ -682,6 +683,32 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
           let resultType ← inferType result
           if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then
             let result ← instantiateMVars result
+            /- We use `check` to propogate universe constraints implied by the `result`.
+               Recall that we use `ignoreLevelMVarDepth := true` which allows universe metavariables in the current depth to be assigned,
+               but these assignments are discarded by `withNewMCtxDepth`.
+
+               TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
+                     a universe metavariable from previous universe levels have been assigned or not during TC resolution.
+                     We only need to perform the `check` if this kind of assignment have been performed.
+
+               The example in the issue #796 exposed this issue.
+               ```
+                structure A
+                class B (a : outParam A) (α : Sort u)
+                class C {a : A} (α : Sort u) [B a α]
+                class D {a : A} (α : Sort u) [B a α] [c : C α]
+                class E (a : A) where [c (α : Sort u) [B a α] : C α]
+                instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
+
+                def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
+               ```
+               The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
+               resolution produces the result `@c.{u} a e α b`.
+               Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
+               but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
+               but this assignment is lost.
+            -/
+            check result
             pure (some result)
           else
             trace[Meta.synthInstance] "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index b150b2d7c9..5517447647 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,33 +1,3 @@
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
 jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
 context:
@@ -62,8 +32,12 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
+  @EGrfl
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -77,12 +51,8 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
+jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -131,3 +101,33 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
diff --git a/tests/lean/run/796.lean b/tests/lean/run/796.lean
new file mode 100644
index 0000000000..338c6649bc
--- /dev/null
+++ b/tests/lean/run/796.lean
@@ -0,0 +1,59 @@
+namespace Ex1
+structure A
+class B (a : outParam A) (α : Sort u)
+class C {a : A} (α : Sort u) [B a α]
+class D {a : A} (α : Sort u) [B a α] [c : C α]
+class E (a : A) where [c (α : Sort u) [B a α] : C α]
+instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
+
+def d {a : A} [E a] (α : Sort u) [B a α] : D α := ⟨⟩
+end Ex1
+
+namespace Ex2
+class C where f : Sort u → Nat
+class D extends C
+def a [C] := C.f Nat
+def b [D] := D.toC.f Nat
+def c [D] := C.f Nat
+end Ex2
+
+namespace Ex3
+section
+variable (N : Type _)
+class Zero where
+  zero : N
+export Zero (zero)
+class Succ where
+  succ : N → N
+export Succ (succ)
+class Succ_Not_Zero [Zero N] [Succ N] where
+  succ_not_zero {n : N} : succ n ≠ zero
+export Succ_Not_Zero (succ_not_zero)
+class Eq_Of_Succ_Eq_Succ [Succ N] where
+  eq_of_succ_eq_succ {n m : N} (h : succ n = succ m) : n = m
+export Eq_Of_Succ_Eq_Succ (eq_of_succ_eq_succ)
+class Nat_Induction [Zero N] [Succ N] where
+  nat_induction {P : N → Sort _}
+    (P0 : P zero)
+    (ih : (k : N) → P k → P (succ k))
+    (n : N) : P n
+export Nat_Induction (nat_induction)
+end
+
+section
+variable (N : Type _)
+class Natural
+extends Zero N, Succ N, Succ_Not_Zero N, Eq_Of_Succ_Eq_Succ N, Nat_Induction N
+end
+
+section
+variable {ℕ} [Natural ℕ]
+def pred_with_proof (n : ℕ) (h : n ≠ zero) : Σ' m, n = succ m :=
+  by
+  revert h
+  let P (k : ℕ) := k ≠ zero → Σ' m, k = succ m
+  exact (nat_induction (by simp ; exact False.elim) (λ k _ _ => ⟨k, rfl⟩) n : P n)
+
+def pred (n : ℕ) (h : n ≠ zero) : ℕ := (pred_with_proof n h).fst
+end
+end Ex3