The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear all,

Try the following code in Coq (I was using a home-compiled 8.2pl1):

Inductive type: Set
:= | int: type
  | Cbool: type
  | ref: type -> type.

Definition value_set
  : type -> Set
  := fun type: type
     => match type with
        | int => nat
        | Cbool => bool
        | ref t => nat
        end.

Inductive test:
  forall t: type,
  forall v: value_set t,
  Prop
:= | test1:
       forall t: type,
       test (ref t) 3
  | test2:
       test Cbool true.

Check (
  fun H2: test int 5 =>
  match H2 as H2' in test t' v''
  return
     forall t'': type,
     t' = t'' ->
     False
  with
  | test1 t''' => 3
  | test2 => 2
  end).

In the final Check command Coq says that the 3 in the first branch of
the match is wrong (it is of course right about that!).
It says:
Error: In environment
H2 : test int 5
t''' : type
The term "3" has type "nat" while it is expected to have type
 "forall t'' : type, ref t'' = t'' -> False".

However, the type that Coq proposes is not right either!
The pattern of this branch is test1 t''' and that is of type  test (ref t''') 
3.
Hence in this case, to obtain the return type we should do the
substitutions t' -> ref t''' and v'' -> 3.
Hence the type that should be expected becomes
     forall t'': type,
     ref t''' = t'' ->
     False
However, Coq is requesting the type with t''' replaced with t''!

This is a simplification of the actual development. In that I am
trying to apply the refine tactic with the 3 in the above example
replaced by _ and that leads to an equally weird error that I traced
back to this problem.

All the best,
Chris