The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Hi Jonathan,

Thanks for the reply, and for the suggested workaround. I’ll see if I can get 
something like that to work.

The reason this looks like a bug to me, though, is that I think, if I’m not 
mistaken, that what I am actually trying solve is the problem

?T2 x = ?B

(Technically, I think Coq writes the left-hand side as something like 
?T2@{__:=x}, but it’s the same thing.) This problem has the solution ?T2 = 
(fun _ => ?B). It falls into the higher-order pattern fragment, since ?T2 is 
fully applied to distinct bound variables, and I thought Coq would solve this 
fragment.

Also, either way, the fact that the unify tactic is not commutative also 
seems like a bug...

-Eddy

> On Dec 2, 2016, at 12:22 PM, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
> 
> 
> 
> On 12/02/2016 02:50 PM, Eddy Westbrook wrote:
>> 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.
> 
> Wait - what?  You want unification to remove the dependency of ?T2 on x?  
> That's unifying a function of one var with a constant (function of 0 vars). 
>  They don't have the same type.
> 
> However, you can explicitly remove the dependency yourself, like this:
> 
> Definition foo A B : (A -> B) = (A -> B) := eq_refl.
> 
> Goal { T:Type | T=T }.
>  refine (exist _ (forall (x:?[T1]), ?[T2]) _).
>  instantiate (T2:=ltac:(clear x)). (*remove dependency of ?T2 on x*)
>  apply foo.
> 
> Note that using the instantiate tactic this way is considered a bit of a 
> hack...
> 
> -- Jonathan
> 
>