Unused variable catches more than one case is printed multiple times for unused variables that do not catch multiple cases

[JasonGross]

Description of the problem

Inductive type {base_type : Type} := base (t : base_type) | arrow (s d : type).
Global Arguments type : clear implicits.
Fixpoint interp {base_type} (base_interp : base_type -> Type) (t : type base_type) : Type
  := match t with
     | base t => base_interp t
     | arrow s d => @interp _ base_interp s -> @interp _ base_interp d
     end.
Axiom admit : forall {T}, T.
Section with_base.
  Context {base_type : Type}
          {base_interp : base_type -> Type}.
  Local Notation type := (@type base_type).

  Fixpoint default {t} : interp base_interp t
    := match t with
       | base x => admit
       | arrow s d => fun _ => @default d
       end.
  (* Warning: Unused variable s catches more than one case. [unused-pattern-matching-variable,pattern-matching]
Warning: Unused variable s catches more than one case. [unused-pattern-matching-variable,pattern-matching]
*)
End with_base.

What's up with this? cc @herbelin

I assume it has something to do with trying to elaborate the match in multiple ways, since adding return interp _ t suppresses the error message?

Coq Version

master (bba5713)

[herbelin]

Yes, this is due to several possible return types being tried when compiling. Thanks for telling. Fixed in #14261.

[JasonGross]

Thanks! Though I don't think that PR fully fixes this issue; the variable s does not in fact catch multiple cases

[herbelin]

Ah I see, the PR only fixes the repetition.

About a more precise detection, this is more complicated, as the dependency is in an existential variable...

[JasonGross]

About a more precise detection, this is more complicated, as the dependency is in an existential variable...

It's not the dependency I'm complaining about (I think the computation there is correct), but the claim that it matches multiple cases.

When I Set Printing All. Print default., the code I see is

default =
fix default (t : B.type base_type) : @interp base_type base_interp t :=
  match t as t0 return (@interp base_type base_interp t0) with
  | base x => @admit (@interp base_type base_interp (@base base_type x))
  | arrow s d =>
      fun
        _ : (fix interp (base_type : Type) (base_interp : forall _ : base_type, Type) (t0 : B.type base_type) {struct t0} : Type :=
               match t0 return Type with
               | base t1 => base_interp t1
               | arrow s0 d0 => forall _ : interp base_type base_interp s0, interp base_type base_interp d0
               end) base_type base_interp s => default d
  end
     : forall t : B.type base_type, @interp base_type base_interp t

Arguments default {t}

I thought that maybe it's complaining about s being matched on, but in fact getting rid of the bare fix with

  Fixpoint default {t} : interp base_interp t
    := match t with
       | base x => admit
       | arrow s d => fun _ : interp _ _ => @default d
       end.
  Set Printing All.
  Print default.

gives

default =
fix default (t : B.type base_type) : @interp base_type base_interp t :=
  match t as t0 return (@interp base_type base_interp t0) with
  | base x => @admit (@interp base_type base_interp (@base base_type x))
  | arrow s d => fun _ : @interp base_type base_interp s => default d
  end
     : forall t : B.type base_type, @interp base_type base_interp t

Arguments default {t}

If I annotate the return type myself with interp _ t then the warning goes away, without changing the final code. While the "is the variable used" can depend on which things are evars and which are not, I expect the detection of multiple cases vs single case to only depend on the spine(?) of the match, or at the very least to only depend on the final code and not on which things are evars and which are not. Am I mistaken?

[herbelin]

Sorry for being slow in understanding. The wrong reporting is also due to side effects (there is a backtracking inside the algorithm which is counting s twice).

I updated #14261 so that it does not use a side effect.

[JasonGross]

Awesome, thanks!