The Coq mailing list

[Dan Synek <synek AT cs.ru.nl>]

Below is a simple definition of a function "test" which works. However 
if the comment around
the type specification is uncommented then coq outputs the error below. 
Since this is the type that coq outputs anyway when asked using Check, 
it is quiet confusing:

The term
"match t in (Test b1) return (if b1 then bool else nat) with
 | ta => true
 | tb => 1
 end" has type "if c then bool else nat" while it is expected to have type
"if c then bool else nat"

-----


Inductive Test:bool-> Set := ta:Test true | tb : Test false.

Definition test (c:bool)(t:Test c)  (* : if c then bool else nat*) :=
  match t in Test b1 return (if b1 then bool else nat) with
    ta => true
  | tb => 1
  end.

Check test.

(* Outputs test
    : forall c : bool, Test c -> if c then bool else nat *)