... | ... | @@ -138,7 +138,7 @@ GHC will also have applied the renaming to any wanteds via `SEQSAME`. |
|
|
## Generating "Hidden" Givens While Solving Wanteds
|
|
|
|
|
|
|
|
|
If I recall correctly, new givens cannot be generated while simplifying wanteds (the comment on [ \`TcInteract.runTcPluginsWanted\`](https://github.com/ghc/ghc/blob/57858fc8b519078ae89a4859ce7588adb39f6e96/compiler/typecheck/TcInteract.hs#L269) sounds like I'm recalling correctly). I think this should be allowed, if only as a convenience to plugin authors. They could at least use it to memoize any forwarding chaining/reasoning done by their plugin as it solves wanteds. (For my particular plugin, it might also be nice if these hidden givens could be accompanied by similarly hidden universally quantified variables; in other words, binding this evidence might reveal an existentially quantified variable. This seems like a bigger ask...)
|
|
|
If I recall correctly, new givens cannot be generated while simplifying wanteds (the comment on [\`TcInteract.runTcPluginsWanted\`](https://github.com/ghc/ghc/blob/57858fc8b519078ae89a4859ce7588adb39f6e96/compiler/typecheck/TcInteract.hs#L269) sounds like I'm recalling correctly). I think this should be allowed, if only as a convenience to plugin authors. They could at least use it to memoize any forwarding chaining/reasoning done by their plugin as it solves wanteds. (For my particular plugin, it might also be nice if these hidden givens could be accompanied by similarly hidden universally quantified variables; in other words, binding this evidence might reveal an existentially quantified variable. This seems like a bigger ask...)
|
|
|
|
|
|
|
|
|
It might also enable the plugin to cache state specific to the givens, based on an otherwise unused constraint like `MyStateCacheIdentifier 42`. (This is probably only wise for memoization.) And if that cached state contains type variable uniques, then another otherwise unused constraint `Rename '[v1,v2,...]`, would let the plugin track how the uniques on the type variables `v1,v2,...` during GHC's turn. Uniques on evidence variables could not be similarly tracked, which is problematic. That deficiency of this workaround suggests that reporting updated uniques to a plugin deserves genuine support in the API.
|
... | ... | @@ -237,7 +237,7 @@ The basic task is to add a given equality `lr .& le0 .& le1 .& ... .& leN ~ rr . |
|
|
### `Lacks` Phase
|
|
|
|
|
|
|
|
|
In addition to the equality store, we also build a canonical representation of the `Lacks` constraints. In order to explain the invariants, we'll need to understand arithmetic on `Lacks` dictionaries. A `Lacks x b` dictionary evidences that a type `b` is not an element of `x`, but the evidence for that contains more information than is strictly necessary. In particular it is a non-negative integer that supports an efficient implementation of records/variants etc. The semantics of `d :: Lacks x b` is that exactly `d`-many elements in `x` are "less than" `b`. This details of this ordering are arbitrary, but it is total for types with no free variables. (I implement it using a partial deterministic variation on [ Type.nonDetCmpTypeX](https://github.com/ghc/ghc/blob/21e1a00c0ccf3072ccc04cd1acfc541c141189d2/compiler/types/Type.hs#L2177).)
|
|
|
In addition to the equality store, we also build a canonical representation of the `Lacks` constraints. In order to explain the invariants, we'll need to understand arithmetic on `Lacks` dictionaries. A `Lacks x b` dictionary evidences that a type `b` is not an element of `x`, but the evidence for that contains more information than is strictly necessary. In particular it is a non-negative integer that supports an efficient implementation of records/variants etc. The semantics of `d :: Lacks x b` is that exactly `d`-many elements in `x` are "less than" `b`. This details of this ordering are arbitrary, but it is total for types with no free variables. (I implement it using a partial deterministic variation on [Type.nonDetCmpTypeX](https://github.com/ghc/ghc/blob/21e1a00c0ccf3072ccc04cd1acfc541c141189d2/compiler/types/Type.hs#L2177).)
|
|
|
|
|
|
|
|
|
Instead of a substitution like the equality store, `Lacks` constraints are represented as a set of nested maps. A constraint `d :: Lacks (x .& u .& v) b`, becomes a sequence of mappings `b := m0` such that `m0` includes `x := m1` such that `m1` includes `{u,v} := d`. The key invariant for this store is that the recorded mappings cannot be simplified (compare to the idempotency of the equality store). In particular, if `b , x , {u,v} , d1` is in the store, then `b , x , {u,v,w} , d2` cannot be in the store, but `b , Set0 , {w} , (d2 - d1)` should be instead. These are the possible simplifications that the store must be canonical wrt:
|
... | ... | |