The Coq mailing list

[Yannick <yannick.zakowski AT irisa.fr>]

Dear Coq list,

Say I have functions of two arguments whose type of the second argument
depends on the value of the first. Assuming appropriate instances of
EqDec, I defined in my development a generic function to update such
functions.

However, trying to apply this generic update to functions whose second
argument actually does not depend on the first, I encountered issues
around which I can't quite wrap my head.

I tracked the problem down to the smallest example I could, that you
will find enclosed.

Essentially, the question boils down to proving:
forall _:K1, EqDec K2 eq
Knowing an instance of:
EqDec K2 eq

Which Coq manages by itself as long as K1 and K2 are variables, but
fails as soon as K2 is a "real" type, the vacuous one here for instance.

Please find in the attached file the more detailed situation.

Would anyone understand what is going on here, and hopefully know how to
fix it?

Many thanks,
Best,

Yannick
Require Import Classes.EquivDec.
Require Import Eqdep_dec.
Require Import Utf8.

Definition rognudju {K1: Type} {K2: K1 -> Type} `{forall x, EqDec (K2 x) eq} 
           (f: forall (x1: K1) (x2: K2 x1), True) := True. 

Set Printing Implicit.
Set Typeclasses Debug.

Section Test1.

  (** Normal use, nothing to see here, everything works as expected **)

  Variable K1: Type.
  Variable K2: K1 -> Type.
  Variable ED2: forall (k1: K1), EqDec (K2 k1) eq.
  Variable f: forall (k1: K1) (k2: K2 k1), True.

  Check (rognudju f).
  Definition bar1 := rognudju f.

End Test1.

Section Test2.

  (** Here K2 actually does not depend on K1. However, things are still going great! Sounds good **)

  Variable K1 : Type.
  Variable K2: Type. 
  Variable ED2: EqDec K2 eq.
  Definition map := forall (k1: K1) (k2: K2), True.
  Variable f: map.

  Check (rognudju f).
  Definition bar2 := rognudju f.

End Test2.

Section Test3.

  (** A quite modest change: K2 is not a Variable anymore, but a vacuous type **)

  Variable K1 : Type.
  Inductive K2: Type :=. 
  Variable ED2: EqDec K2 eq.
  Definition map3 := forall (k1: K1) (k2: K2), True.
  Variable f: map3.

  (** But that breaks everything **)
  Check (rognudju f).
  Fail Definition bar3 := rognudju f.
  Definition bar3 := rognudju (H := λ _:K1, ED2) f.

  (** Even worse, adding the exact desired instance does not satisfies it **)
  Instance test: forall x:K1, @EqDec ((λ _ : K1, K2) x) (@eq ((λ _ : K1, K2) x)) (@eq_equivalence ((λ _ : K1, K2) x)) := λ _: K1, ED2.
  Fail Definition really := rognudju f.

End Test3.