Stream: Coq users

Topic: type_scope and higher order function arguments


view this post on Zulip spaceloop (Jun 03 2021 at 08:35):

I was a bit surprised to find out that the * notation in

Definition f (g : Type -> Type) := forall a b, g (a * b).

was interpreted in nat_scope instead of type_scope. Reading up on the docs, I found:

The scope type_scope has a special status. It is a primitive interpretation scope which is temporarily activated each time a subterm of an expression is expected to be a type.

My subterm (a * b) is clearly expected to be a type. What am I missing here?

view this post on Zulip Guillaume Melquiond (Jun 03 2021 at 08:38):

It is "clearly expected to be a type" after typing has occurred, but the resolution of notations happen before typing (for obvious reasons). If g had not been a local binder but a global symbol, then it would have worked.

view this post on Zulip spaceloop (Jun 03 2021 at 08:56):

Thanks, I see.

If g had not been a local binder but a global symbol, then it would have worked.

Is that because g can then be separately typed and have appropriate scopes bound to its arguments?

view this post on Zulip Guillaume Melquiond (Jun 03 2021 at 08:57):

Yes, exactly.


Last updated: Jan 29 2023 at 05:03 UTC