List uniqueness predicate decidability

I'd like to define a predicate for list uniqueness and its decidability function in Coq. My first try was:

Section UNIQUE.
  Variable A : Type.
  Variable P : A -> Prop.
  Variable PDec : forall (x : A), {P x} + {~ P x}.


  Definition Unique (xs : list A) := exists! x, In x xs /\ P x.

Here I just have specified that predicate Unique xs will hold if there's just one value x in list xs such that P x holds. Now, comes the problem. When I've tried to define its Unique decidability:

  Definition Unique_dec : forall xs, {Unique xs} + {~ Unique xs}.
    induction xs ; unfold Unique in *.
    +
      right ; intro ; unfold unique in * ; simpl in * ; crush.
    +
      destruct IHxs ; destruct (PDec a).
      destruct e as [y [Hiy HPy]].
  ...

I've got the following nasty error message:

Error: Case analysis on sort Set is not allowed for inductive definition ex.

I've googled this message and seen several similar problems in different contexts. At least to me, it seems that such problem is related to some restrictions on Coq pattern matching, right?

Now that the problem is settled, my questions:

1) All I want is to define a decidability for a uniqueness test based on a decidable predicate. In the standard library, there are similar tests for existencial and universal quantifiers. Both can be defined as inductive predicates. Is there a way to define "exists unique" as an inductive predicate on lists?

2) It is possible to define such predicate in order to it match the standard logic meaning of exists unique? Like exists! x, P x = exists x, P x /\ forall y, P y -> x = y?

Solution

What you're running into is that you can't pattern match on ex (the underlying inductive for both exists and exists!) in order to produce a value of type sumbool (the type for the {_} + {_} notation), which is a Type and not a Prop. The "nasty error message" isn't terribly helpful in figuring this out; see this bug report for a proposed fix.

To avoid this issue, I think you should prove a stronger version of Unique that produces something in Type (a sig) rather than Prop:

Definition Unique (xs : list A) := exists! x, In x xs /\ P x.
Definition UniqueT (xs : list A) := {x | unique (fun x => In x xs /\ P x) x}.

Theorem UniqueT_to_Unique : forall xs,
    UniqueT xs -> Unique xs.
Proof.
  unfold UniqueT, Unique; intros.
  destruct X as [x H].
  exists x; eauto.
Qed.

You can then prove decidability for this definition in Type, and from there prove your original statement if you want:

Definition UniqueT_dec : forall xs, UniqueT xs + (UniqueT xs -> False).

As mentioned in Anton's answer, this proof will require decidable equality for A, also in Type, namely forall (x y:A), {x=y} + {x<>y}.