Add support for data constructors attributes

[W95Psp]

Hi,

This PR adds support for decorating data constructors (and records) with attributes, as @TWal was suggesting a few days ago on Slack. The syntax follows the one for binders, that is:

type test0 =
  | [@@@ someAttribute1; someAttribute2] A
  | ...
type test1 = [@@@ someAttribute] { foo: int; }

This PR also adds prettyprinting for attributes on binders & constructors. It also adds two test modules: one functional test ConstructorAttributes and one prettyprinting test.

Most of the changes are about adding a _ to TyconRecord or constructors.

Is there a reason attributes on binders are typechecked as unit specifically, while top-level attributes are just untyped terms? ~For now, I didn't add any such checks for binders on constructors. Should I change that?~

EDIT: the CI fail, but that's because I changed parse.mly. I'll push an ocaml snapshot, but I guess that's not ideal for merging afterward.

[aseemr]

Thanks for the PR @W95Psp! I have left some comments, the main one is for the AST change in FStar.Syntax.Syntax, wonder if we can do without it.

[W95Psp]

Thanks @aseemr! I rewrote the desugaring part to use the sigattrs field, it is indeed way simpler.

However, type checking attributes on sigelt breaks some things:

• attributes with universe polymorphic terms (here in Steel for instance) cannot be typechecked;
• I had to add an unpleasant hack for the attribute Substitute that gets inserted before being declared (see my comment on FStar.TypeChecker.Tc)

Do you have any idea about those issues?

[W95Psp]

I think this PR is ready now.

A few notes about the changes I made recently:

• in Typechecker.Normalize, deep_compress was actually not enough, after testing more thoroughly. So, as you suggested @mtzguido, I dropped the useless deep_compress and kept only elim_uvars_aux_t.
• 12794d49b15342772bfb3375f989fc3d00cda409 drops most of the code of handle_postprocess_with_attr, which I think is now useless since every attributes are elaborated and typechecked. @guido I saw you added that code because of #2132, do you think my change is okay? In the same theme, this PR solves #2132, and more particularly, now this passes, uncommented: https://github.com/FStarLang/FStar/blob/1601c00aed53cf38baae5744ebde8704a7d8a7a9/tests/bug-reports/Bug2132.fst#L26-L27
• Also, while modifying test case for #2132, I figured it would be nice to be able to use expect_failure for errors happening on attributes, so commit cf319df3d331a21c8d79e25002aa29b1fb1f2e1f allows that. (I also added a test case for that)

What do you think @mtzguido and @nikswamy?

[mtzguido]

Hi Lucas,

• in Typechecker.Normalize, deep_compress was actually not enough, after testing more thoroughly. So, as you suggested @mtzguido, I dropped the useless deep_compress and kept only elim_uvars_aux_t.

Sounds good. Actually, I hadn't really paid attention to the fact this is introducing typechecking of all attributes for sigelts. If uvars can appear and be resolved in the attributes, then this is indeed the right to thing to do.

• 12794d4 drops most of the code of handle_postprocess_with_attr, which I think is now useless since every attributes are elaborated and typechecked. @guido I saw you added that code because of Failure("Impossible: missing universe instantiation on unroll") #2132, do you think my change is okay?

Yes, I think it's great. If all attributes are typechecked then all the better IMO. I don't remember if there was a rationale for not checking them, though.

In the same theme, this PR solves Failure("Impossible: missing universe instantiation on unroll") #2132, and more particularly, now this passes, uncommented: https://github.com/FStarLang/FStar/blob/1601c00aed53cf38baae5744ebde8704a7d8a7a9/tests/bug-reports/Bug2132.fst#L26-L27

Awesome. I can't really explain why that is.. since the tactic was already being checked, but all the better!