diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28a97bb91af5..0ccc4fd9f921 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -503,14 +503,23 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
           | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
             (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
               (position_problem true pbty,ev,term2) with
-	      | UnifFailure (_,OccurCheck _) -> 
-		(* Eta-expansion might apply *) default ()
+              | UnifFailure (_,(OccurCheck _ | NotClean _)) ->
+                (* Eta-expansion might apply *)
+                (* OccurCheck: eta-expansion could solve
+                     ?X = {| foo := ?X.(foo) |}
+                   NotClean: pruning in solve_simple_eqn is incomplete wrt
+                     Miller patterns *)
+                default ()
 	      | x -> x)
           | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
             (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
               (position_problem false pbty,ev,term1) with
-	      | UnifFailure (_, OccurCheck _) ->
-		(* Eta-expansion might apply *) default () 
+              | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
+                (* OccurCheck: eta-expansion could solve
+                     ?X = {| foo := ?X.(foo) |}
+                   NotClean: pruning in solve_simple_eqn is incomplete wrt
+                     Miller patterns *)
+                default ()
 	      | x -> x)
           | _ -> default ()
         end
diff --git a/test-suite/bugs/closed/bug_9663.v b/test-suite/bugs/closed/bug_9663.v
new file mode 100644
index 000000000000..b5fa6012781d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9663.v
@@ -0,0 +1,2 @@
+Definition id_depfn S T (f : forall x : S, T x) := f.
+Definition idn : nat -> nat := @id_depfn _ _ (fun x => x).