From 4c34eecfd94292cd506930ed82c26ea6e16f731b Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 20 May 2026 14:42:55 +0200
Subject: [PATCH] failing deriving test

---
 Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean b/Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean
index 254b66d74a2519..833e6e587acae5 100644
--- a/Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean
+++ b/Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean
@@ -52,13 +52,17 @@ namespace AffineEtale
 protected def mk {R : CommRingCat.{u}} (f : Spec R ⟶ S) [Etale f] : AffineEtale S :=
   MorphismProperty.CostructuredArrow.mk ⊤ f ‹_›
 
+set_option trace.Elab.Deriving true
 /-- The `Spec` functor from the small affine étale site of `S` to the small étale site of `S`. -/
 @[simps! obj_left obj_hom map_left]
 protected def Spec (S : Scheme.{u}) : S.AffineEtale ⥤ S.Etale :=
   MorphismProperty.CostructuredArrow.toOver _ _ _
+deriving Functor.Full, Functor.Faithful
 
-instance : (AffineEtale.Spec S).Faithful :=
-  inferInstanceAs <| (MorphismProperty.CostructuredArrow.toOver _ _ _).Faithful
+#check instFaithfulCostructuredArrowOppositeCommRingCatEtaleTopMorphismPropertySpecOverSpec
+set_option trace.Meta.synthInstance true in
+instance : (AffineEtale.Spec S).Faithful := inferInstance
+  -- inferInstanceAs <| (MorphismProperty.CostructuredArrow.toOver _ _ _).Faithful
 
 instance : (AffineEtale.Spec S).Full :=
   inferInstanceAs <| (MorphismProperty.CostructuredArrow.toOver _ _ _).Full