I wonder whether it's possible to pull off this dependent pattern match. As you see, I'm trying to map multiple values to nul (and instructing the output to have the required type w/ a return clause). Type N is a garbage collector, I'm simply trying to get rid of all the values after
| P, c => phy
| P, b => phy
| Ii, b => inf
(In this particular setting, using an option type seemed very unwieldy.) Note that if Coercion is impossible here, I'd be also happy w/ Definition
Inductive R := P | Ii | S | N.
Parameter rp:> R -> Prop.
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X.
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N).
Check phy: id P.
Fail Coercion xi(y:R)(x:X): id y := match y, x with
| P, c => phy
| P, b => phy
| Ii, b => inf
| _, _ => match _ return N with _ => nul end end.
(* The term "nul" has type "rp N" while it is expected to have type "rp Ii". *)
A shorter solution w/ a definition returning a "match type":
Inductive R := P | Ii | S | N. Fail Check N: Type.
Parameter rp:> R -> Prop. Check N: Type.
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X.
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N).
Definition xi (y:R) := match y return (match y with (P|Ii) => y | _ => N end) with
| P => phy
| Ii => inf
| _ => nul end.
Eval hnf in xi S. (* = nul *)
Found the idea here