... | ... | @@ -63,6 +63,7 @@ Those with an MR actually have code. |
|
|
- How do we call the empty \theta? \epsilon (neutral element of constraint list) seems misleading compared to \emptyset (neutral element of union).
|
|
|
- What are FV (the things we bind in Gamma) of Theta? Only the match variables or also let-bound stuff? We don't have any binding constructs in our representation of theta, so probably the latter? That is quite weird, because Gamma will bind stuff from other closed lexical scopes. See `h` in #17378, where in the second equation, Gamma would have to bind `y` although it's only a thing in the first equation.
|
|
|
- Having the condensed form `Redundant | Inaccessible | Reachable` is inconsequential, because then we need to concern `pmcheck` with inhabitation testing (\cup_C and \cup_D, for example), when in the rest of the checking function we don't test for inhabitants eagerly. I think we should commit to either early or late inhabitation testing, not this in-between stuff. Also we need the Covered set for long distance info anyway. But where should we attach Gamma then? To the ClauseResult triple? To the incoming uncovered set? Both need it. But for `pmcheck` we can just take Gamma as a parameter, so we should be fine. But also Gamma is specific to each theta. Yuck!!!
|
|
|
- So: Gamma must be part of theta/we should name the list of constraints delta and have `\theta ::= \Gamma \vdash \Delta`.
|
|
|
- Think about how to fix "regression" in T11822
|
|
|
- SG bets a smart `CoreMap` would do
|
|
|
- Maybe pattern-match check typed TH quotations? SG doesn't think this is a good idea, because they might not even end up in that form in spliced code.
|
... | ... | |