Weaken ability members behind let-bindings

This commit is contained in:
Ayaz Hafiz 2023-01-12 15:05:54 -06:00
parent 48049ed956
commit c3f1646274
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 44 additions and 7 deletions

View file

@ -3860,9 +3860,10 @@ fn is_generalizable_expr(mut expr: &Expr) -> bool {
| TypedHole(_) | TypedHole(_)
| RuntimeError(..) | RuntimeError(..)
| ZeroArgumentTag { .. } | ZeroArgumentTag { .. }
| Tag { .. } => return false, | Tag { .. }
| AbilityMember(_, _, _) => return false,
// TODO(weakening) // TODO(weakening)
Var(_, _) | AbilityMember(_, _, _) => return true, Var(_, _) => return true,
} }
} }
} }

View file

@ -6599,6 +6599,42 @@ mod solve_expr {
#^^{-1} #^^{-1}
main = main =
alias1 = \x -> id x
# ^^
alias2 = \x -> alias1 x
# ^^^^^^
a : A
a = alias2 (@A {})
# ^^^^^^
a
"#
),
@r###"
A#id(4) : A -[[id(4)]]-> A
Id#id(2) : a -[[] + a:id(2):1]-> a | a has Id
alias1 : a -[[alias1(6)]]-> a | a has Id
alias2 : A -[[alias2(7)]]-> A
"###
)
}
#[test]
fn resolve_lambda_set_weakened_ability_alias() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1}
main =
# Both alias1, alias2 should get weakened
alias1 = id alias1 = id
# ^^ # ^^
alias2 = alias1 alias2 = alias1
@ -6613,8 +6649,8 @@ mod solve_expr {
), ),
@r###" @r###"
A#id(4) : A -[[id(4)]]-> A A#id(4) : A -[[id(4)]]-> A
Id#id(2) : a -[[] + a:id(2):1]-> a | a has Id Id#id(2) : A -[[id(4)]]-> A
alias1 : a -[[] + a:id(2):1]-> a | a has Id alias1 : A -[[id(4)]]-> A
alias2 : A -[[id(4)]]-> A alias2 : A -[[id(4)]]-> A
"### "###
) )
@ -6744,8 +6780,8 @@ mod solve_expr {
#^^{-1} #^^{-1}
main = main =
alias = id alias = \x -> id x
# ^^ # ^^
a : A a : A
a = (alias (@A {})) {} a = (alias (@A {})) {}
@ -6757,7 +6793,7 @@ mod solve_expr {
@r#" @r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8]]-> {}) A#id(5) : {} -[[id(5)]]-> ({} -[[8]]-> {})
Id#id(3) : a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) | a has Id Id#id(3) : a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) | a has Id
alias : {} -[[id(5)]]-> ({} -[[8]]-> {}) alias : {} -[[alias(9)]]-> ({} -[[8]]-> {})
"# "#
print_only_under_alias: true print_only_under_alias: true
) )