The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

If you do 
Set Printing All.

then you get the error message:

The term
 "match
    t in (Test b)
    return match b return Type with
           | true => bool
           | false => nat
           end
  with
  | ta => true
  | tb => S O
  end" has type "match c return Type with
                 | true => bool
                 | false => nat
                 end" while it is expected to have type
 "match c return Set with
  | true => bool
  | false => nat
  end"

...which is a bit more illuminative.

-Andrew

On Tue, 12 Apr 2005, Dan Synek wrote:
> 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 *)
> 
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>