diff --git a/tests/lean/run/newfrontend4.lean b/tests/lean/run/newfrontend4.lean
deleted file mode 100644
index 313e3de21b..0000000000
--- a/tests/lean/run/newfrontend4.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-new_frontend
-
--- set_option syntaxMaxDepth 100
--- set_option trace.Elab true
--- set_option trace.Meta true
--- set_option trace.Meta.synthInstance false
-
-def adapt1 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
-⟨fun split join => monadMap @(fun α => adaptState split join : forall (α : Type), m α → m' α)⟩ -- monadMap (adaptState split join : m α → m' α)⟩
-
-def adapt2 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
-⟨fun split join => monadMap @(fun α => (adaptState split join : m α → m' α))⟩ -- monadMap (adaptState split join : m α → m' α)⟩
-
-def adapt3 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
-⟨fun split join => monadMap (m:=m) (m':=m') (adaptState split join)⟩
-
-/-
-The following fails because we cannot synthesize the instance
-```
-  [MonadFunctorT
-     (λ (β : Type), m  (?m_1 σ'' α split join β))
-     (λ (β : Type), m' (?m_1 σ'' α split join β))
-     n
-     (λ {α : Type}, n' α)]
-```
-Note that we have an instance `[MonadFunctorT m m' n n']`. The TC procedure performs eta-reduction, and manage to reduce
-`(λ {α : Type}, n' α)` to `n'`, but it cannot eta-reduce the arguments
-```
-     (λ (β : Type), m  (?m_1 σ'' α split join β))
-     (λ (β : Type), m' (?m_1 σ'' α split join β))
-```
-The reduction is blocked by the metavariable applications `(?m_1 σ'' α split join β)`.
-Remark: eta-expansion would also not solve the problem. The TC procedure would convert the instance
-`[MonadFunctorT m m' n n']`
-into
-`[MonadFunctorT (fun β => m β) (fun β => m' β) (fun α => n α) (fun α => n' α)]`
-but it would fail trying to unify
-```
-?m_1 σ'' α split join β =?= β
-```
-since `?m_1` was not created by the TC procedure. It was created by the elaborator.
--/
--- def adapt4 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
--- ⟨fun split join => monadMap (adaptState split join : m _ → m' _)⟩ -- monadMap (adaptState split join : m α → m' α)⟩