[ new ] Support arbitrary Name in IBindVar

[spcfox]

Description

Replaces String with Name in the IBindVar signature. This makes IBindVar more consistent and allows the binding of machine-generated names. Using machine-generated names in IBindVar can be useful in compiler and elaborator scripts.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[spcfox]

This PR is ready to review. The fixes in LSP-lib, elab-util, frex and idrall (for katla) should be enough for a green CI

[spcfox]

The status of the pack collection with this branch:

[ warning ] The following packages failed to build:
            - barbies
            - bounded-doubles-hedgehog-generators(failing dependencies: pretty-show, sop)
            - chem-generators(failing dependencies: pretty-show, sop)
            - cyby-draw(failing dependencies: json-simple)
            - dependent-map(failing dependencies: pretty-show, sop)
            - deptycheck
            - dom-mvc(failing dependencies: json-simple)
            - dom-mvc-extra(failing dependencies: json-simple, barbies)
            - hedgehog(failing dependencies: pretty-show, sop)
            - http(failing dependencies: sop)
            - json
            - json-simple
            - lana(failing dependencies: json, json-simple)
            - node
            - parser-tsv
            - parser-webidl(failing dependencies: sop)
            - pretty-show
            - refined-json(failing dependencies: json-simple)
            - refined-tsv(failing dependencies: parser-tsv)
            - sop
            - sqlite3
            - sqlite3-rio(failing dependencies: sqlite3)
            - stellar-http(failing dependencies: node)
            - stellar-sql(failing dependencies: sqlite3, json)
            - tls(failing dependencies: sop)
            - tyttp-adapter-node(failing dependencies: node)
            - tyttp-json(failing dependencies: json, sop, node)
            - webidl(failing dependencies: sop)
[ warning ] 28 packages failed to build.

[stefan-hoeck]

Looking at the failing pack libraries, this will require quite a bit of work till the pack collection is up and running again. Many of the failing packages are my own, so they should be fine. deptycheck and node are not, so we probably should get in touch with their maintainers.

I for my part am ready to go with this and merge the adjustments made to elab-util as soon as reviewers are ready to merge this.

Thanks, spcfox, for going through the trouble and also checking the pack collection!

[spcfox]

I'm working with @buzden, we're ready to make changes to deptycheck

[buzden]

As a comment beside libraries changes, I've talked about this change with Edwin in 2021 and he agreed that this should be done and said that he didn't remember why the current design of IBindVar was chosen.

[dunhamsteve]

I believe we need to bump the TTC version in src/Core/Binary.idr. Otherwise, it will fail with "file: Corrupt TTC data for Name" when it reads .ttc files made by the current Idris.

[spcfox]

I'm not sure if this kind of code is supposed to work. It doesn't right now

definition : Decl
definition =
   IDef EmptyFC `{ foo }
        [ PatClause EmptyFC `( foo ~(IBindVar EmptyFC $ UN $ Basic "x") )
                             (IVar EmptyFC (DN "y" $ UN $ Basic "x"))]

[buzden]

I'm not sure if this kind of code is supposed to work. It doesn't right now

definition : Decl
definition =
   IDef EmptyFC `{ foo }
        [ PatClause EmptyFC `( foo ~(IBindVar EmptyFC $ UN $ Basic "x") )
                             (IVar EmptyFC (DN "y" $ UN $ Basic "x"))]

I think it should, because I understand DN as a purely pretty-printing thing, which should not influence on typechecking

[spcfox]

I'm not sure if this kind of code is supposed to work. It doesn't right now

definition : Decl
definition =
   IDef EmptyFC `{ foo }
        [ PatClause EmptyFC `( foo ~(IBindVar EmptyFC $ UN $ Basic "x") )
                             (IVar EmptyFC (DN "y" $ UN $ Basic "x"))]

Ok, this is not related to the current PR, created an issue #3542 on this behavior

[spcfox]

List of packages requiring fixes:

CI:

• elab-util
• lsp-lib
• idrall
• frex

Pack collection:

@stefan-hoeck:

• barbies
• hedgehog
• json & json-simple
• parser-tsv & parser-webidl
• pretty-show
• sop
• sqlite3

other:

• deptycheck
• node

Failed due to dependencies:

• bounded-doubles-hedgehog-generators
• chem-generators
• cyby-draw
• dependent-map
• dom-mvc & dom-mvc-extra
• http
• lana
• refined-json & refined-tsv
• sqlite3-rio
• stellar-http & stellar-sql
• tls
• tyttp-adapter-node & tyttp-json
• webidl

[spcfox]

I've prepared patches to all the libraries. This PR is ready for review and merge.

[buzden]

I'm really for merging this PR. In order to make Idris CI to become green, we need besides e.g. me, one of @ohad or @gallais for frex, and one of @mattpolzin or @alexhumphreys for idrall, which is a dependency for katla. All that we need is to merge corresponding pull requests adapting to this one.

In order the next pack collection won't fail building next day, we need also @stefan-hoeck and @kbertalan to be ready to merge compat pull requests to their repos.

Guys, can we syncronise, say, today to do all that?

[stefan-hoeck]

I'm ready to update my packages as soon as this is merged. Today would be fine, tomorrow also.

[mattpolzin]

Works for me.

[kbertalan]

I can merge the changes to my project when this is merged within a 12 hours window any week day this week.

[spcfox]

@ohad, @gallais, @stefan-hoeck, @mattpolzin, @kbertalan, @buzden
How about this week?