Explain why we currently cannot mark degeneralization in when headers

This commit is contained in:
Ayaz Hafiz 2023-01-10 11:30:59 -06:00
parent c2cb94a927
commit 5db82ad965
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58

View file

@ -1055,7 +1055,17 @@ pub fn constrain_expr(
pattern_headers,
pattern_constraints,
body_constraints,
// TODO(weakening)
// NB(weakening): ideally we never explicitly mark generalizability here, but we
// must currently do so to handle cases like
//
// ```
// \x -> when x is
// Red -> Red
// ```
//
// because we ultimately want `[Red]*` to be generalized at the level the function
// argument `x` is and not pulled down into a lower rank. However we don't yet have
// a way to express that requirement.
Generalizable(true),
);
@ -2283,7 +2293,17 @@ fn constrain_when_branch_help(
[],
guard_constraint,
ret_constraint,
// TODO(weakening)
// NB(weakening): ideally we never explicitly mark generalizability here, but we
// must currently do so to handle cases like
//
// ```
// \x -> when x is
// Red -> Red
// ```
//
// because we ultimately want `[Red]*` to be generalized at the level the function
// argument `x` is and not pulled down into a lower rank. However we don't yet have
// a way to express that requirement.
Generalizable(true),
);