The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Dear Coq club list,

I feel like the following should work, but it doesn’t, and something like it 
keeps coming up in some typeclass programming I am trying to do:

Definition foo A B : (A -> B) = (A -> B) := eq_refl.

Goal { T:Type | T=T }.
  refine (exist _ (forall (x:?[T1]), ?[T2]) _).
  apply foo.


Somehow, it seems like Coq does not want to apply foo because it works on 
non-dependent function types, even though all it has to do is to unify ?T2, 
which depends on x, with the B argument of foo, which does not.


I tried to boil the problem down further, and ended up with this, which also 
exposes some cases where the unify tactic is not commutative:

Goal { T:_ & T }.
  refine (existT _ (forall (x:?[T1]) (y:?[T2]), ?T1) _).
  evar (Tnew:Type).

  (* OK: unify (fun (x:?T1) => ?T2) (fun (x:?T1) => ?Tnew). *)
  (* FAILS: unify (fun (x:?T1) => ?Tnew) (fun (x:?T1) => ?T2). *)

  (* OK: unify (forall (x:?T1), ?T2) (forall (x:?T1), ?Tnew). *)
  (* FAILS: unify (forall (x:?T1), ?Tnew) (forall (x:?T1), ?T2). *)

  (* FAILS: unify (forall (x:?T1) (y:?T2), ?T1) (forall (x:?T1), ?Tnew). *)
  (* FAILS: unify (forall (x:?T1), ?Tnew) (forall (x:?T1) (y:?T2), ?T1). *)


Does anyone know of a workaround for this problem, where I can tell Coq to 
instantiate all the evars in the body of a forall with fresh evars that are 
not dependent?

Thanks,
-Eddy