Skip to content

Automatic tracking of CallsFed constraints#3083

Merged
pcapriotti merged 21 commits intowireapp:developfrom
isovector:transitive-anns
Feb 23, 2023
Merged

Automatic tracking of CallsFed constraints#3083
pcapriotti merged 21 commits intowireapp:developfrom
isovector:transitive-anns

Conversation

@isovector
Copy link
Contributor

@isovector isovector commented Feb 14, 2023

This PR uses a new GHC plugin to automatically track CallsFed constraints across the codebase without manual programmer intervention. At a high level, it introduces a couple of new constructs:

Adding Annotations

class AddAnnotation (loc :: LocalOrRemote) (api :: Symbol) (method :: Symbol) x

Adding an AddAnnotation loc api method constraint to a function will instruct GHC to track this function call across the call-graph. Any other function which transitively calls this function will also acquire an AddAnnotation loc api method constraint. This is completely analogous to the old CallsFed constraint, except that the plugin prevents us from needing to move the constraints around ourselves.

The x parameter is an implementation detail, and should always be filled with an ambiguous, unspecified type variable.

Exposing Annotations

exposeAnnotations :: ToHasAnnotations x => a -> a

The exposeAnnotations f function lets us reintroduce AddAnnotation loc api method x constraints attached to f, rewriting them as HasAnnotation loc api method constraints. By calling this function at the edge of each servant handler, the constraints GHC sees are exactly the same as if we had manually pushed the CallsFed constraints all the way to servant. These constraints get immediately handled via callsFed as before, ensuring we get an unsolved instance error if a codepath makes a federated call that isn't documented in the servant API.

Misc

The plugin itself is currently a little messy. I'd like to clean it up before merging this PR, but would like confirmation that this is an approach we'd like to take before I invest that time into it.

Unfortunately, this PR requires reverting #3030, since we are now running at too low-level to use type information to help drive the analysis.

Checklist

  • Add a new entry in an appropriate subdirectory of changelog.d
  • Read and follow the PR guidelines

@isovector isovector marked this pull request as draft February 14, 2023 17:17
Copy link
Contributor

@pcapriotti pcapriotti left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks great! I'm looking forward to having this applied everywhere and to error constraints as well.

I don't quite understand the meaning of the Location parameter of HasAnnotation. Could the Location thing and Symbols be replaced by an arbitrary kind, like
class HasAnnotation a (x :: a)? That would make the plugin more general, and allow us to use it for errors too.

The constraint-discharging mechanism using the empty dictionary trick could be moved to the plugin itself and ported to HasAnnotation constraints, right?

Somewhat relatedly, could this be improved by adding an extra type variable to the constraint? Then we could solve it directly by writing an empty instance of the HasAnnotation class for a new type. This could have been slightly annoying before, because the variable had to be specified on every function, but now it would be fine.

@isovector
Copy link
Contributor Author

The location parameter is for my followup step of tracking non-federated calls across the codebase. I am open to better naming for the constructors here :)

I explored making the annotation generic, but it's a no-go unfortunately. The compiler doesn't have enough information at compile-time to easily reify everything we need. Eg, we need a Data instance to push these things into ANNs, as well as a function of the form a -> CoreExpr. However, we can turn Annotation into a sum type and use it for other things too.

The constraint-discharging mechanism using the empty dictionary trick could be moved to the plugin itself and ported to HasAnnotation constraints, right?

I haven't explored this idea. It's plausible, depending on GHC's plugin architecture. However, I'd prefer to get a smaller plugin merged and battle-hardened before putting in more surface for things to go wrong.

Somewhat relatedly, could this be improved by adding an extra type variable to the constraint? Then we could solve it directly by writing an empty instance of the HasAnnotation class for a new type. This could have been slightly annoying before, because the variable had to be specified on every function, but now it would be fine.

I don't quite understand the suggestion here, but am all ears!

@pcapriotti
Copy link
Contributor

pcapriotti commented Feb 16, 2023

I don't quite understand the suggestion here, but am all ears!

If CallsFed constraints looked like

foo :: CallsFed Brig "blah" x => ...

Then we could avoid the unsafeCoerce to make an instance, because we could make a new type and give it an instance in the normal way

data X

instance CallsFed c api X

Then say mkNamedAPI or callsFed or similar would instantiate x to X and the constraint would be solved normally.

This would be annoying right now because this x type would need to be passed around with type applications everywhere. But with the plugin it's fine.

Actually, I think we could have taken this approach even without the plugin, by using the r in Sem r instead of a new variable. This is pretty much how error constraints are propagated and handled at the end.

@isovector isovector marked this pull request as ready for review February 17, 2023 00:06
Copy link
Contributor

@pcapriotti pcapriotti left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Thanks for this!

@elland elland added the ok-to-test Approved for running tests in CI, overrides not-ok-to-test if both labels exist label Feb 20, 2023
isovector and others added 4 commits February 20, 2023 09:35
changes after running
```
./hack/bin/generate-local-nix-packages.sh
```
@pcapriotti pcapriotti merged commit ba3a3e7 into wireapp:develop Feb 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ok-to-test Approved for running tests in CI, overrides not-ok-to-test if both labels exist

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants

Comments