 Solution

Generate every permutation of the tail, then insert its missing head at every possible position. The helper preserves order among the elements already present:The first helper result inserts $x$ before $y$; the mapped recursive results put $y$ back at the front and insert $x$ farther along. For a list of length $k$, it yields exactly $k+1$ positions. The empty list has one permutation, itself, so the base result is [[]], not [].

For correctness, use structural induction. Any permutation of x :: xs has a unique position containing $x$. Removing that position leaves a permutation of xs, supplied by the induction hypothesis; reinserting $x$ at its unique position reconstructs the required output. With distinct input elements, neither the tail permutation nor the insertion position can be duplicated, so each output occurs once. Consequently a length-$n$ input yields exactly $n!$ permutations, in an unrestricted order. The explicit output is large; this is not a polynomial-time enumeration with respect to $n$ alone.