[m-rev.] for review: allow higher-order inst info in equivalence types

Julien Fischer jfischer at opturion.com
Tue Jul 23 20:58:11 AEST 2024


On Tue, 23 Jul 2024 at 19:34, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
> For review by anyone.
>
> This diff starts the process of allowing higher-order inst info in types.
> It specifically allows them on the right hand side of equivalence type
> definitions, which is enough for an important use case. getopt_io.m,
> which normally uses *lots* of insts to specify higher order inst info,
> can now get *all* of its higher-order inst info purely from the types.
> (The attached new version of getopt_io.m still uses four insts,
> but it uses them for another purpose.)
>
> The process that this diff starts has a long way to go. The type
> why_no_ho_inst_info in parse_type_name.m lists many more places where
> higher-order inst infos are syntactically possible but are also semantically
> prohibited, at least for now. In some cases, the prohibition should probably
> stay (I see no point in lifting it for ctgc/sharing/reuse pragmas, since
> they are not yet operational); in others, such as pred and func args and
> mutable decls, it should go. But even in the cases where we want to lift
> the prohibition, we need to agree on what the updated semantics is
> of the construct in question, and create test cases for the proper
> implementation of that semantics.
>
> The only practical way to do this is lifing each restriction piece-by-piece,
> and so that is what I propose to do. If I find the semantics of lifting
> a restriction unclear, I will describe the issues and wait for a consensus
> before proceeding. Are there any objections?

Not from me.

> I don't think there is any point in announcing each step to users. I think
> any announcements should wait until the end, because only then will the
> picture for users be simple again.

Agreed.

The diff looks fine.

Julien.


More information about the reviews mailing list