Proposal: Remove FC from Elab trees

[andrevidela]

• I have read CONTRIBUTING.md.
• I have checked that there is no existing PR/issue about my proposal.

Summary

When working on elaboration scripts, users are expected to write trees for the programs they wish to generate. Those tress carry around file context information. However, this location is almost always empty.

Motivation

The trees built during elaboration reflection closely match the internal trees of the compiler, including file location information. Because the trees built during elaboration reflection are not written from syntax, they often carry an empty file location. See:

• elab-utils: https://github.com/stefan-hoeck/idris2-elab-util/blob/main/src/Language/Reflection/Syntax.idr
• All the deriving scripts: https://github.com/idris-lang/Idris2/blob/main/libs/base/Deriving/Foldable.idr#L330

File location is not a necessary part of building trees. And having it produces heavy breaking changes whenever code relating to file location changes. What's more, breaking elaboration can come from unrelated changes to syntax highlighting, or error reporting, which greatly increases code the burden of changes to the compiler, and create code churn for downstream libraries.

The proposal

Remove all FC reference in the Language/Reflection/TTImp trees. Replace error reporting from failAt : FC -> String -> m a and warnAt : FC -> String -> m () by functions fail : TTImp -> String -> m a and warn : TTImp -> String -> m ()

Where the m monad keeps track of locations for every term. This way users can keep the ability to emit errors and warnings at precise locations, without relying on manually keeping track of file locations.

Alternatives considered

We could keep the current state since location information could be used for better error reporting. However, such usage seems to be the exception rather that the rule. Something else we could do is write an engine that will generate appropriate file locations but this is a lot of work, and could be done after the file locations have been removed from the trees.

Conclusion

This change would bring Idris in line with Haskell and Agda that do not expose any location information during elaboration reflection. It will also make changes to TTImp easier to perform, and reduce the entry barrier to elaboration reflection.

[buzden]

Elab trees are there not only for producing code, but also for getting already present code from the compiler. This allows us to fail elaborator scripts pointing at specific parts of hand-written code. This includes involved data declarations and signatures of functions where particular elaborator scripts are used. For example, when some type of argument is not supported, now elaborator scripts can point to this particular argument using failAt, because TTImps received from the compiler contain correct FCs.

I can suggest another alternative -- to make FCs to be default-implicits with EmptyFC set as default. This would keep values from the compiler to have correct FCs without bothering users too much.

[andrevidela]

This allows us to fail elaborator scripts pointing at specific parts of hand-written code.

Do you have an example of this? I wonder if this is something we could automate instead of making the script writer do it

[buzden]

This allows us to fail elaborator scripts pointing at specific parts of hand-written code.

Do you have an example of this? I wonder if this is something we could automate instead of making the script writer do it

Sure, a lot of them!

There are couple of examples even in tests:
https://github.com/idris-lang/Idris2/blob/main/tests/idris2/reflection/reflection024/src/TypeProviders.idr#L64
and
https://github.com/idris-lang/Idris2/blob/main/tests/idris2/reflection/reflection020/FromTTImp.idr#L18

I have a lot of such behaviour in my elaborator scripts:
https://github.com/buzden/idris2-mk/blob/master/src/Language/Mk.idr#L17
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr#L47
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr#L52-L53
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L71
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L75
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L79
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L102
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L141
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L170-L176
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L237
https://github.com/buzden/deptycheck/blob/master/src/Deriving/DepTyCheck/Gen/Entry.idr#L241

[andrevidela]

Thank you for all those links. It seems to me like there are essentially two kinds of error locations:

• point to the original spot in the file where the code was quoted
• point to some subpart of it that's been carried through the elaborator script.

Is that right? Or is there something else?

[buzden]

Something else. FC can be got from TTImps originating not only from quote, but from goal or type too. Plus, their subparts, surely

[andrevidela]

so to recap, FC come from:

• original place where the code was quoted
• some subpart from the original quote
• some fragment from goal or type

Is that right?

If so, it seems like all the places where FC are being used and generated already come from the compiler, and so, given some term, the compiler should be able to already generate an appropriate location for it. This could allow the failAt and warnAt methods to rely on a TTImp term rather than an arbitrary location.

[buzden]

so to recap, FC come from:

• original place where the code was quoted
• some subpart from the original quote
• some fragment from goal or type

Is that right?

Seems right, yes

If so, it seems like all the places where FC are being used and generated already come from the compiler, and so, given some term, the compiler should be able to already generate an appropriate location for it. This could allow the failAt and warnAt methods to rely on a TTImp term rather than an arbitrary location.

Well, maybe, but I don't understand how can this be implemented, since compiler does not hold back-references to original RawImp' when quoting them to TTImps and I'm not sure this is easy to do

[elseLuna]

I've done some experiments implementing whole new syntax (notably a tactic mode) by having an elaboration script transform a quoted term, and manipulating FCs (for better error reporting, showing the correct type on hover, etc.) was an important part of it. This is an edge case of course, but I wouldn't want it to be impossible.

Personally, I see TTImp as a kind of low-level, raw term structure for building abstractions over, such as those in elab-util. If the goal is to make elaborator reflection easier to use out of the box, I'd rather leave TTImp how it is, and move some of the utilities from elab-util into the compiler itself, although I'm not sure that's necessary.

[andrevidela]

manipulating FCs (for better error reporting, showing the correct type on hover, etc.)

Do you have examples of this that we can study?

I'm going to update the motivation of the proposal because

I'd rather leave TTImp how it is

Is essentially impossible with an evolving programming language, removing FCs makes a lot more changes easier to do since they won't introduce breaking in all the libraries using elab reflection

[elseLuna]

manipulating FCs (for better error reporting, showing the correct type on hover, etc.)

Do you have examples of this that we can study?

Here's a minified example: https://gist.github.com/elseLuna/23c595bfa59b1235baa7abf82e7c4491

This is a huge hack though, so if there's good reason to remove FCs don't let this stop you.

EDIT: Actually, after thinking about it for a bit, even if FCs were removed from TTImp, if a way to copy the internal FC from one term to another were added, this hack would still be possible.