Coqのmatch文で場合分けするとき，対象に依存する型の対象のところが場合分けされないということがある．
(うまく書けない…)
以下のような例:

Definition func (S:Set)(P:list S->Prop)(g:P nil->S)
                (l:list S)(p:P l) : S :=
  match l with
    | nil => g p
    | s::ss => s
  end.

nilで分けた右側で，次のようなエラーになる．

The term "p" has type "P l" while it is expected to have type 
"P nil".

だから，lがnilの場合だって言ってるだろ，と言いたいところだがだめなようだ．

次のように考えれば良いらしい．

• match文でSを表現するのはあきらめて，P nil -> S を表現する．
• その関数を p に適用することで S を得る．
• s::ssの時には定数関数でよい．
• こう考えればmatch文の表す型が，「nil の時には P nil -> S で
  s::ss の時には P s::ss -> S だ」，と見なせるので，return を
  使って表現することができる

ということで，次のようになる:

Definition func (S:Set)(P:list S->Prop)(g:P nil->S)
                (l:list S)(p:P l) : S :=
  match l as x return P x -> S with
    | nil =>   g
    | s::ss => fun _ => s
  end p.

[2013.06.13追記] Chlipala の教科書で取り上げられていた。次のように書けばよいらしい。なるほど….

Definition func (S:Set)(P:list S->Prop)(g:P nil->S)
                (l:list S): P l -> S :=
  match l with
    | nil =>   fun p => g p
    | s::ss => fun _ => s
  end.