Stream: Coq users

Topic: Can't this type be inferred?


view this post on Zulip Justin Kelm (Sep 06 2023 at 23:22):

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?

view this post on Zulip Li-yao (Sep 07 2023 at 00:44):

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 *)

view this post on Zulip Justin Kelm (Sep 07 2023 at 01:08):

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.)

view this post on Zulip Gaëtan Gilbert (Sep 07 2023 at 07:24):

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