The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> Hi,
> 
> Activating display of implicit and low-level information ("Set Printing
> All" or Alt-A in menu Display of CoqIDE, or correspondingly in
> ProofGeneral) gives the answer:
> 
> The type of poly_out is
> 
> match j return Type with | 0 => unit | S _ => nat end
> 
> while poly_in expects
> 
> match j return Set with | 0 => unit | S _ => nat end
> 
> You may write explicitly "match x return Set with | O => unit | _ => nat
> end" in poly_out, so as to circumvent the solution found by the type 
> inference mechanism algorithm.

Ah, that makes sense.  Specifying Set makes it work properly.
Thanks!

Compute (fun j => poly_in j (poly_out j)) 3.
     = 1

> Inference of "i" in poly_in seems to work for me in (at least) 8.3pl2.

I meant that while I can do

Compute poly_in 0 tt.
     = 0

I can't do

Compute poly_in _ tt.
                  ^^
Error: The term "tt" has type "unit" while it is expected to have type
 "match ?22 with
  | 0 => unit
  | S _ => nat
  end".

or even

Compute poly_in _ (tt : match 0 return Set with | 0 => unit | S _ => nat end).
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The term "tt:match 0 with
                    | 0 => unit
                    | S _ => nat
                    end" has type "match 0 with
                                   | 0 => unit
                                   | S _ => nat
                                   end" while it is expected to have type
 "match ?25 with
  | 0 => unit
  | S _ => nat
  end".


> Hugo Herbelin
> 
> On Sat, Nov 17, 2012 at 04:20:25PM -0800, S3 wrote:
>> 
> 
> ********* *BEGIN ENCRYPTED or SIGNED PART* *********
> 
>> Definition poly_out x := match x return match x with | O => unit | _ =>
>> nat end with | O => tt | S _ => 0 end .
>> 
>> Definition poly_in i (x : match i with | 0 => unit | _ => nat end) := 
>> match i as j return (match j with | 0 => unit | _ => nat end -> nat)
>> with | 0 => fun u => match u with | tt => 0 end | _ => fun n => match n
>> with | 0 => 1 | _ => 2 end end x .
>> 
>> (* Compute (fun j => poly_in j (poly_out j)).
>> 
>> The term "poly_out j" has type "match j with | 0 => unit | S _ => nat 
>> end" while it is expected to have type "match j with | 0 => unit | S _ =>
>> nat end".
>> 
>> Is there a way to write that expression to make it type check? What is it
>> unhappy about?
>> 
>> I also found that Coq (8.3pl1) doesn't want to infer the value for i in
>> poly_in, so leaving it implicit doesn't work.
>> 
>> I realize that normally I would just declare a new tagged union type, 
>> which would handle the tag i parameter automatically, but I wanted to see
>> what happens if I go this way. *)

- -- 
*********************.************************************..|
**..*.*...*..**....**....*....**....***.**...*..***.......*.|
*..**.**...**.***...*...*..*.**..****...*...*.*.....**..*...|
.*..*..*.*..*.....******...*.*..*.*.**...*.**.*..*..***..*..|
...*.*..*..***..*.*****...*...*....****.....***.*...**..**..|
..*.....**..***.*.........*.*...*..**..**game*.....*........|
*....*..**..*.*.*.*..*.**.*..*..*..**..**of**......**.***...|
*.**.*..**..*.*.**.**..**.**.****..***life.**.****..*.****..|
**********************************************************..|
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAlCoSdAACgkQxzVgPqtIcfvcDQCfUsDy7KwI0hvwYq+qTk3eL+VG
YOwAn26ak38+eGyNSYGqlZ5pO2rXOHXL
=kt+S
-----END PGP SIGNATURE-----