update elab for WithFC

[andrevidela]

fix for idris-lang/Idris2#3423

[mattpolzin]

This looks good. Since CI isn't set up to test against an arbitrary upstream commit of the compiler I'll test this compiles for me locally on my laptop before approving.

[alexhumphreys]

Thanks for the PR! It's been a while, and that derive/ folder is maybe the most complicated part of the code, so I don't remember how it works 😅
At least the CI test suite is pretty extensive, so if you can get those passing that should be good enough to merge. Right now it looks like this PR is failing to compile with this error:

 6/21: Building Idrall.Derive.Common (Idrall/Derive/Common.idr)
Error: While processing right hand side of mkTy. Undefined name MkFCVal. 

Idrall.Derive.Common:20:23--20:30
 16 | |||
 17 | ||| This is an alias for `MkTyp EmptyFC`.
 18 | export
 19 | mkTy : (n : Name) -> (ty : TTImp) -> ITy
 20 | mkTy = MkTy EmptyFC . MkFCVal EmptyFC
                            ^^^^^^^

[alexhumphreys]

Ah, looks like the tests are building against the docker image snazzybucket/idris2, which hasn't been updated in 11 months. So if you're testing against an open idris2 PR that's gonna be trickier, can see now why @mattpolzin offered to test locally!

[mattpolzin]

Tested locally.

./build/exec/runtests idrall --interactive --only

------------------------------------------------------------------------
dhall-lang tests
------------------------------------------------------------------------

idrall/idrall001: success
idrall/idrall002: success
idrall/idrall003: success
idrall/idrall004: success
idrall/idrall005: success

------------------------------------------------------------------------
dhall-lang expected fail tests
------------------------------------------------------------------------

failure/failure001: success

------------------------------------------------------------------------
derive tests
------------------------------------------------------------------------

derive/derive001: success
derive/derive002: success
derive/derive003: success

------------------------------------------------------------------------
examples tests
------------------------------------------------------------------------

examples/example001: success
examples/example002: success
examples/example003: success
examples/inigo001: success
13/13 tests successful

[andrevidela]

Thank you so much!

[mattpolzin]

upstream has merged; I'll merge this. Sounds like Alex was discovering the Docker image this CI uses has not been updated recently so we will have broken CI going forward until that is fixed, but that's a problem for a separate PR.

[andrevidela]

Thanks