# Implicit arguments in non-top-level functions

**URL:** <https://discourse.rocq-prover.org/t/implicit-arguments-in-non-top-level-functions/761>\
**Category:** Using Rocq\
**Created:** [April 10, 2020, 9:35am UTC](https://discourse.rocq-prover.org/t/implicit-arguments-in-non-top-level-functions/761 "2020-04-10T09:35:08Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Urj8EN6U](https://avatars.discourse-cdn.com/v4/letter/u/8e7dd6/32.png) [@Urj8EN6U](https://discourse.rocq-prover.org/u/Urj8EN6U)\
**Post date:** [April 10, 2020, 9:35am UTC](https://discourse.rocq-prover.org/t/implicit-arguments-in-non-top-level-functions/761/1 "2020-04-10T09:35:08Z")

</div>

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:

```auto
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?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [April 15, 2020, 5:08am UTC](https://discourse.rocq-prover.org/t/implicit-arguments-in-non-top-level-functions/761/2 "2020-04-15T05:08:04Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Urj8EN6U](https://avatars.discourse-cdn.com/v4/letter/u/8e7dd6/32.png) [@Urj8EN6U](https://discourse.rocq-prover.org/u/Urj8EN6U)\
**Post date:** [April 15, 2020, 9:43am UTC](https://discourse.rocq-prover.org/t/implicit-arguments-in-non-top-level-functions/761/3 "2020-04-15T09:43:19Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Urj8EN6U](https://avatars.discourse-cdn.com/v4/letter/u/8e7dd6/32.png) [@Urj8EN6U](https://discourse.rocq-prover.org/u/Urj8EN6U)\
**Post date:** [April 24, 2020, 6:18pm UTC](https://discourse.rocq-prover.org/t/implicit-arguments-in-non-top-level-functions/761/4 "2020-04-24T18:18:05Z")

</div>

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](https://github.com/coq/coq/issues/12166#issue-606117493)).

@JasonGross took the time to [answer](https://github.com/coq/coq/issues/12166#issuecomment-619148869) 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.