The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Nikhil Swamy wrote:
> The example below illustrates what I’d like to accomplish.
>
> Inductive A : Type :=
>
> | One : A
>
> | Two : A.
>
> Inductive B : A -> Type := .
>
> Definition foo (b: B One) := tt.
>
> Definition bar (a:A) (b:B a) : unit :=
>
> match a with
>
> | One => foo b (* some way to coerce b's type to (B One)? *)
>
> | Two => tt
>
> end.

A simple rearrangement of the function definition gets this to go 
through. What looks like magic actually works because this change makes 
it possible to use an inferred [return] clause to express the dependency 
between [a] and [b].

Definition bar (a:A) : B a -> unit :=
match a with
| One => foo
| Two => fun _ => tt
end.

This and other dependent typing "tricks" are one of the main subjects of 
CPDT (http://adam.chlipala.net/cpdt/).