The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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.

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

Hugo Herbelin

On Sat, Nov 17, 2012 at 04:20:25PM -0800, S3 wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
> 
> 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/
> 
> iEYEARECAAYFAlCoKckACgkQxzVgPqtIcfsX5QCfYP3vdjrJvCFg+X51ardCgc4I
> 6PIAniT9tPcSiczmHWjhjnzlyyMX1lbS
> =LZz5
> -----END PGP SIGNATURE-----