I was working through Chapter 2 of CPDT ( http://adam.chlipala.net/cpdt/html/Cpdt.StackMachine.html ) and playing around with implicit argument inference.

I found out that a statement like this will infer correctly:

```
Theorem tcompile_correct : forall {t} (e : texp t), tprogDenote (tcompile e []) tt = (texpDenote e, tt).
```

but not this:

```
Theorem tcompile_correct : forall e, tprogDenote (tcompile e []) tt = (texpDenote e, tt).
ERROR: Cannot infer the implicit parameter t of texpDenote whose type is "type".
```

My definition of `texpDenote`

looks like: `Fixpoint texpDenote {t} (e : texp t) : typeDenote t := ...`

Is there an obvious reason why Coq shouldn't be able to infer the existence of a type `t0`

for which `e : texp t0`

, and identify the `t`

from the signature of `texpDenote`

with this `t0`

?

Coq never infers implicit arguments by default. You can use Implicit Generalization for that. Example:

```
Parameter f : forall (A : Type), A -> Prop.
Generalizable Variables a.
Definition w : forall `(a), f _ a. (* would fail without the backquotes-parenthesis *)
```

Hm, I see. If I understand correctly, arguments in a function may be implicitly inferred from the types of other arguments of the function, but free variables in a `forall`

binder will not be implicitly inferred from the types of other free variables, unless Implicit Generalization is turned on.

At any rate, I'm not sure Implicit Generalization is even smart enough to cover this case, since it complains:

```
Theorem tcompile_correct : forall `(e : texp t), tprogDenote (tcompile e []) tt = (texpDenote e, tt).
ERROR: The term "t" has type "Set" while it is expected to have type "type".
```

(Recalling that `type`

in this part of CPDT is a custom Inductive type we made, not the base `Type`

.)

I guess `t`

is bound to some definition or inductive so it's not considered for generalization

Last updated: Jun 13 2024 at 19:02 UTC