증명 트리

트레이트 솔버 자체는 목표가 성립하는지 여부와 필요한 제약 조건만 반환하지만, 때로는 그 목표를 증명하는 과정에서 무슨 일이 일어났는지도 알아야 할 때가 있습니다. 트레이트 솔버는 일반적으로 컴파일러의 나머지 부분에서 블랙박스로 취급되어야 하지만, 그 내부를 완전히 무시할 수는 없으므로 이를 위한 인터페이스로 “증명 트리“를 제공합니다. 이를 사용하려면 ProofTreeVisitor 트레이트를 구현하십시오. 예시는 기존 구현을 참고하십시오. 가장 대표적인 용도는 일관성 오류에 대한 크레이트 간 모호성 원인 계산, 트레이트 솔버 오류 개선, 그리고 클로저 시그니처의 조기 추론입니다.

증명 트리 계산하기

트레이트 솔버는 표준화를 사용하며, 각 중첩된 목표마다 완전히 별개의 InferCtxt를 사용합니다. 진단과 rustdoc의 자동 트레이트 모두 “중첩된 목표 들여다보기“를 올바르게 처리해야 합니다. Vec<Vec<?x>>: Debug와 같은 목표가 주어지면, 이를 exists<T0> Vec<Vec<T0>>: Debug로 정규화하고, 그 목표를 Vec<Vec<?0>>: Debug로 인스턴스화하여 중첩된 목표 Vec<?0>: Debug를 얻습니다. 이를 다시 정규화하여 exists<T0> Vec<T0>: Debug를 얻은 뒤 Vec<?0>: Debug로 인스턴스화하면, 결국 모호한 중첩 목표 ?0: Debug가 생깁니다.

트레이트 솔버의 평가 단계를 트리로 변환하는 탐색 그래프에 ProofTreeBuilder를 전달하여 증명 트리를 계산합니다. 추론 변수나 플레이스홀더를 사용하는 데이터를 저장할 때, 해당 데이터는 이 계산 중에 생성된 모든 제약되지 않은 추론 변수의 목록과 함께 정규화됩니다. 그런 다음 증명 트리를 순회하는 동안 이 CanonicalState가 부모 추론 컨텍스트에서 인스턴스화되며, 이때 추론 변수 목록을 사용하여 이 평가 중에 생성된 모든 정규화된 값을 연결합니다.

솔버 디버깅하기

이전에는 솔버 구현을 디버깅하는 데에도 증명 트리를 사용하려고 시도했습니다. 이는 솔버를 프로그래밍 방식으로 분석하는 것과는 설계 요구 사항이 다릅니다. 트레이트 솔버를 디버깅하는 권장 방법은 tracing을 사용하는 것입니다. 트레이트 솔버는 전반적인 ’형태’에는 debug 추적 수준만 사용하고, 추가적인 세부 사항에는 trace를 사용합니다. 따라서 RUSTC_LOG=rustc_next_trait_solver=debug는 전체적인 개요를 제공하며, 더 정밀한 정보가 필요한 경우에는 RUSTC_LOG=rustc_next_trait_solver=trace를 사용할 수 있습니다.