... | ... | @@ -62,6 +62,7 @@ Those with an MR actually have code. |
|
|
- But if we have the "\Theta = union of \theta" idea, then how does \theta look? -> Just a list of constraints, of course (which are `all` true at the same time). Then \oplus just lifts adding a constraint over all the thetas.
|
|
|
- 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 (U_C and U_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.
|
|
|
- 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.
|
... | ... | |