Implicit arguments in non-top-level functions

Using Coq
1

I am trying to define a function that evaluates to different functions depending on one of its
arguments. Some of the resulting functions refer to an implicit argument of the higher-order
function and some do not. My goal is to be able to evaluate the function without having to
provide the implicit argument even if it does not occur in the result.

Here is a contrived example of what I want to achieve:

Inductive foo : nat -> Type := Foo n : foo n.

Definition bar_type b n : Type :=
  match b with
  | true => nat -> nat
  | false => foo n -> nat
  end.

Definition bar b {n} : bar_type b n :=
  match b return bar_type b n with
  | true => fun _ => 38
  | false => fun _ => 42
  end.

The idea is to be able to call bar without having to provide a value for n for any value of b.

Eval cbv in bar true 17. is successfully evaluated resulting in

= 38
: nat

while Definition foobar_1 := Eval cbv in bar true 17. fails. (I expected
foobar_1 to be bound to 38 : nat.)

When I Set Debug Cbv. before evaluating the code snippets it shows that in case of
Eval term. bar is unfolded without problems. For Definition ident := Eval term.
Coq fails to do so as the implicit parameter n of bar cannot be inferred.

  • How can I make Definition ident := Eval term. work without having to give
    the implicit argument?
  • Is there a better way to get implicit arguments in non-top-level functions?
2

It might be easier to define bar_type to take an option nat, and return nat -> nat on None and foo n -> nat on Some n. Implicit arguments, even unused ones, must be filled in, and I don’t think there’s a robust way to avoid doing that in general.

3

Thanks @Blaisorblade for taking time to reply to my question.

It still leaves me wondering why Eval cbv in bar true 17.
results in

= 38
: nat

which does not depend on the implicit parameter n.

While Definition foobar_1 := Eval cbv in bar true 17.
fails to evaluate with

Cannot infer the implicit parameter n of bar whose type is “nat”.

Is this intended behavior?

4

Since I suspected my problem to be a bug in Coq I reported it as an issue
on GitHub (Evaluating a term works but binding the result fails #12166).

@JasonGross took the time to answer my question and I will sum up his
reply here:

  1. The behavior described above is intended.
  2. All evars occurring in definitions must be instantiated.