Closure property for multiple home units is not enforced nor checked

[mpickering]

The blog post [The Interface for Multiple Home Units](https://well-typed.com/blog/2022/01/multiple-home-units/#closure-property-for-home-units) explains the closure property needed for setting up a multiple component session.

HLS does not ensure this holds which leads to broken sessions when loading multiple components. For example.. random overlapping instance errors, panics in checkFamConst etc etc. It is critical that any session which HLS constructs obeys the closure property.

Stated simply the closure property is:

Any dependency which is not a home unit must not (transitively) depend on a home unit.

And in terms of implementation there is a function in GHC called checkHomeUnitsClosed which implements this check and reports the reason why it's not closed.

My proposal is

• If a new unit is added and the closure property doesn't hold, then the error is reported prominently to the user and the new component is ignored completely by the IDE.
• If a user then subsequently adds the units needed for closure then the session can resume in a multi-component manner.

My experience is that multi-component works without problem as long as the closure property. I spent the last week using the support whilst developing cabal-install, which has 5 components.

In the future:

There should be a better interface for initialising a session which contains multiple components rather than having to create the session incrementally one component at a time.

[michaelpj]

Users don't "add units", so I'm not sure that the workflow you lay out can map into HLS. I guess the closest thing that would correspond to is:

• If a user opens a file in a unit such that adding it would break the closure property, then we give them an error and ignore the file.
• If a user later opens a different files (leading to more units being added) such that the original file is now fine, then when they revisit it we should try to load it again and succeed.

This is a slightly odd situation anyway: it supposes that we have two units A and B such that A depends on B and the user can open files from both. In that scenario why would we not immediately load B as a home unit as soon as the user opens a file in A?

The problematic case is I guess where we have A -> B -> C where A and C are local but B is not. That does seem tricky and we'll probably have to give an error. But if all the units are local I don't see why we can't just load them all as home units to begin with?

[pepeiborra]

I made a similar proposal a while ago: haskell/hie-bios#269

The problem back then is that the user doesn't really know which dependency is breaking the closure property. It sounds like checkHomeUnitsClosed addresses this, which is awesome.

Agree with Michael, it would be best if HLS could parse the result of checkHomeUnitsClosed and automatically load the necessary units to restore the closure property, where possible, otherwise report the error.