클로저 제약 전파

클로저 본문 안에서 타입 테스트와 보편 영역(universal region)을 검사하다 보면 아직 증명할 수 없는 제약을 만날 수 있습니다! 하지만 필요한 제약이 실제로는 성립할 수도 있습니다(아직 그 사실을 모를 뿐입니다). 따라서 클로저 내부에 있다면 아직 증명할 수 없는 제약을 모두 수집해서 반환하기만 합니다. 나중에 클로저를 생성한 MIR 노드를 빌림 검사할 때 이 제약들이 성립하는지도 함께 검사할 수 있습니다. 그때 제약이 성립함을 증명할 수 없으면 오류를 보고합니다.

구현 방식

RegionInferenceContext::solve 안에서 클로저를 빌림 검사하는 동안, type-outlives 제약과 region-outlives 제약을 지역적으로 증명할 수 없으면 두 제약을 각각 따로 부모에게 전파하려고 시도합니다.

region-outlives 제약

RegionInferenceContext::check_universal_regions가 어떤 outlives 제약 'longer_fr: 'shorter_fr를 증명하지 못하면 fn try_propagate_universal_region_error에서 이를 전파하려고 시도합니다. 이 두 보편 영역은 각각 클로저에 지역적인 영역이거나 외부 영역입니다.

'longer_fr가 지역 보편 영역이라면, 'longer_fr가 그보다 오래 사는, 즉 'longer_fr: 'fr_minus를 만족하는 가장 큰 외부 영역 'fr_minus를 찾습니다. 그러한 영역이 여러 개라면 mutual_immediate_postdominator를 선택합니다. 이는 모든 GLB의 GLB를 반복해서 계산하여 얻은 고정점이며, 자세한 내용은 TransitiveRelation::postdom_upper_bound를 참고하십시오.

'fr_minus가 존재하면 이 영역이 'shorter_fr의 모든 비지역 상한보다 오래 살 것을 요구합니다. 비지역 상한은 언제나 적어도 하나, 즉 'static이 존재합니다.

type-outlives 제약

type-outlives 제약은 check_type_tests에서 증명됩니다. 이 작업은 outlives 그래프를 계산한 뒤에 이루어지며, 이 시점부터 그래프는 변경할 수 없습니다.

클로저 내부에서 fn eval_verify_bound로 증명하지 못한 모든 타입 테스트에 대해 try_promote_type_test를 호출합니다. TypeTest는 type-outlives 바운드 generic_kind: lower_bound를 verify_bound와 함께 나타냅니다. VerifyBound가 lower_bound에 대해 성립하면 제약이 충족됩니다. try_promote_type_test는 verify_bound를 신경 쓰지 않습니다.

이 함수는 먼저 fn try_promote_type_test_subject를 호출합니다. 이 함수는 GenericKind를 받아 더 이상 클로저에 지역적인 어떤 것도 참조하지 않는 ClosureOutlivesSubject로 변환하려고 시도합니다. 이를 위해 해당 타입의 모든 자유 영역을 'static이나 그 자유 영역과 같은 영역 매개변수로 대체합니다. generic_kind에 대체할 수 없는 영역이 포함되어 있으면 이 작업은 실패합니다.

그런 다음 lower_bound를 호출자의 컨텍스트로 승격합니다. 하한이 플레이스홀더와 같으면 'static으로 대체합니다

그런 다음 lower_bound가 그보다 오래 살아야 하는 모든 보편 영역 uv, 즉 빌림 검사가 영역 제약을 추가한 보편 영역을 살펴봅니다. 그리고 이들 각각에 대해, uv보다 오래 산다고 알려진 모든 비지역 보편 영역에 대한 ClosureOutlivesRequirement를 생성합니다.

이 시점에는 이미 클로저의 영역 그래프를 구축했고 그 그래프가 일관적인지는 따로 검사하므로, 여기서는 outlives 제약 uv: lower_bound를 가정할 수도 있습니다.

따라서 T: 'local_infer처럼 증명할 수 없는 type-outlives 바운드가 있으면, 영역 그래프를 사용하여 'a: local_infer를 만족하는 보편 변수 'a로 이동합니다. 'a가 지역 영역이라면, 가정한 outlives 제약을 사용하여 비지역 영역으로 이동합니다.

그런 다음 승격된 타입 테스트 목록을 BorrowCheckResults에 저장합니다. 그런 다음 TypeChecker::prove_closure_bounds에서 클로저의 부모를 빌림 검사하는 동안 이를 적용합니다.

TODO: 이것이 정확히 어떻게 동작하는지 설명해야 합니다 :3