WithFC elab

[andrevidela]

Description

Update reflected TTImp to replicate the change that were made in the compiler's tree.

This is also needed as part of a fix for #3417

Unfortunately, I suspect this is going to break a number of elaboration scripts. Hopefully this is something #3421 can help with in the future.

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

[andrevidela]

Alrighty, as expected, lots of breakage with elaboration. I've gotten some PRs ready to fix the changes, can their author confirm the fix is ok?

@stefan-hoeck for elab-utils, @alexhumphreys for idrall and maybe @mattpolzin for LSP-lib?

[mattpolzin]

I've got merge rights for both the LSP and idrall so we should be covered even if Alex isn't available.

[buzden]

elab-util tests are still failing at the state of this PR (we have special CI job for checking breaking upstream changes)

[mattpolzin]

2/3 downstream projects are ready to go now (LSP-lib and idrall).

[buzden]

elab-util is ready too

[andrevidela]

Time to merge everything

[joelberkeley]

did a bug slip through here? I'm seeing this on today's pack build

[ build ] Error: Error during reflection: While processing right hand side of prettyValITy. Can't find an implementation for PrettyVal (WithFC Name).
[ build ] 
[ build ] Text.Show.PrettyVal.Derive:72:57--72:78
[ build ]  68 | 
[ build ]  69 | parameters (nms : List Name)
[ build ]  70 |   arg : BoundArg 1 Explicit -> TTImp
[ build ]  71 |   arg (BA (MkArg M0 _ _ _) _   _) = `(Chr "_")
[ build ]  72 |   arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(prettyVal ~(varStr x))
[ build ]            

[mattpolzin]

There wouldn't be a PrettyVal implementation yet since I believe that is a type within the given package that you're referencing.

Andre updated the known breaking third party packages in response to this PR, but that was only the few packages that run in CI for the compiler repo so there are other third party packages that have broken and will need to be fixed to get pack's full collection back to green.

[joelberkeley]

ah, I saw Text. and assumed it was stdlib. Have raised a ticket with the library stefan-hoeck/idris2-pretty-show#32