The usual argument for the minimality result for Sacks forcing uses choice.
Theorem (Sacks): Let $s \subseteq \mathbb S_\kappa$ be generic for the forcing to add a Sacks subset to $\kappa$, where $\kappa$ is either $\omega$ or inaccessible. Then for any set of ordinals $A \in V[s]$, either $A \in V$ or $s \in V[A]$.
The only proof of which I know for this result starts by considering $p \in \mathbb S_\kappa$ forcing that $\dot A \not \in V$. We find $q \le p$ and a set of ordinals $\{\xi_t : t \text{ a splitting node of } q\}$ so that $q \upharpoonright {t {}^\frown 0}$ and $q \upharpoonright {t {}^\frown 1}$ decide $\xi_t \in \dot A$ differently. From these and $A$ we can reconstruct $s$. We build $q$ as an intersection of a fusion sequence $\{p_\alpha\}$. Given $p_\alpha$, to get $p_{\alpha+1}$ we consider all the $\alpha$th splitting nodes $t$ of $p_\alpha$. For each such $t$, we pick an ordinal $\xi$ so that $p_\alpha \upharpoonright t$ does not decide $\xi \in \dot A$. We then pick $r_0 \le p_\alpha \upharpoonright t {}^\frown 0$ and $r_1 \le p_\alpha \upharpoonright t {}^\frown 1$ which decide $\xi \in \dot A$ differently. We amalgamate all these $r_i$ for all splitting nodes of $p_\alpha$ to produce $p_{\alpha+1} \le_{\alpha+1} p_\alpha$.
Picking an ordinal $\xi$ is of course unproblematic. This is not the case for picking the conditions $r_0$ and $r_1$. Here we need to appeal to choice as there are lots and lots of appropriate conditions below $p_\alpha \upharpoonright t {}^\frown i$.
My question is whether choice is necessary for the minimality result.
Question: Are there $M \models \mathsf{ZF} + \neg \mathsf{AC}$ and $s \subseteq \mathbb S_\kappa^M$ generic for $M$ so that $M[s]$ is not minimal over $M$? That is, are there $M$, $s$ as above and $A \in M[s]$ a set of ordinals so that $M \subsetneq M[A] \subsetneq M[s]$?
