provisional cache

When caching in the trait solver, we have to make sure that we consider everything that may impact the result. In the global cache this includes the remaining allowed depth and in case we cache the root of a cycle, other cycle participants.

The provisional cache is necessary as we can otherwise get hangs, e.g. when compiling syn. We have to make sure that the existence of the provisional cache does not impact behavior in undesirable ways.

how to think about cycles

Conceptionally, a solver cycle is simply an infinitely deep proof tree. A cycle A -> B -> A should therefore be equivalent to the cycle A -> B -> A -> B -> A. This is not quite the case due to incompleteness

This is achieved via a fixpoint algorithm for goals on the stack. However, we have to be careful when caching any goals which depend on the provisional result of goals still on the stack.

When caching these goals we have to make sure the cache does not impact behavior. Let's look at the following dependency tree:

graph TB
   A --> B
   B --> C
   C --> F
   F --> E'
   C --> D
   D --> E
   E -.-> D
   E -.-> G
   G -.-> A
   E -.-> B

We want to reuse the cache entry for D in the D' path. For this to be correct everything we possible relied upon when computing D must be handled:

• required depth (can actually ignore that one, because provisional cache is the same for the same goal, so while that means the provisional cache is observable, it is stable)
• used cycle roots: D, B and A
  • the provisonal result of these goals
  • whether the path from these cycle roots to the goal on the stack was coinductive or inductive
    • If B -> C -> D is coinductive but B -> C -> F -> D' is not, then the result of D' may differ from D.

cycle examples

Using any of all paths to decide whether a cycle is inductive or coinductive.

graph TB
    A -->|T| B
    B -.->|F| A
    A -->|F| B'
    B' -.->|F| A

graph TB
    A -->|T| B
    B -->|T| C
    C -.->|F| B
    C -.->|F| A
    B -->|F| C'
    C' -.->|F| B
    C' -.->|F| A
    A -->|F| C''
    C'' -.->|F| A
    C'' -->|F| B'
    B' -.->|T| C''
    B' -.->|F| C''

graph TB
    A -->|T| B
    B -.->|F| A
    B -->|T| B'
    B'' -.->|F| A
    A -->|F| B''
    B'' -->|T| B'''

impl II

We only track the highest cycle head h for a provisional entry for the goal g. After popping the highest head from the stack, we remove the provisional entry. Recomputing g will depend on h. This can use the provisional entry for h without needing a fixpoint computation. While this can observably result in a different result for g due to incompleteness, this is not unsound as g is not a cycle root, so its result does not get moved to the global cache.