Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

타입 시스템의 불변 조건

FIXME: 이 파일은 솔버만이 아니라 타입 시스템 전체의 불변 조건을 다룹니다

다른 언어와 타입 시스템에서는 불변 조건, 즉 타입 시스템이 항상 참임을 보장하는 사항이 많이 있으며 이러한 조건은 바람직하게 여겨지거나 당연히 기대됩니다. 안타깝게도 그중 상당수는 현재 Rust에서 성립하지 않습니다. 이는 설계상 근본적인 이유 때문이거나 버그 때문이며, 앞으로 바뀔 수도 있습니다.

타입 시스템 자체를 작업하거나 타입 시스템을 활용하여 작업할 때 무엇을 가정할 수 있는지 아는 것이 중요합니다. 그래서 핵심 타입 시스템의 불변 조건을 정리한 불완전하고 비공식적인 목록을 아래에 제시합니다:

  • ✅: 이 불변 조건은 몇 가지 이상한 예외나 현재 존재하는 버그를 제외하면 대체로 성립합니다
  • ❌: 이 불변 조건은 성립하지 않으며, 앞으로도 성립할 가능성이 낮습니다. 건전성을 위해 이에 의존하지 마십시오. 의존해야 한다면 극도로 주의하십시오

wf(X)는 wf(normalize(X))를 함의합니다 ✅

별칭을 포함하는 타입이 적격이라면, 해당 별칭을 정규화한 후에도 적격이어야 합니다. 그렇지 않으면 이러한 타입에 대해 적격성을 다시 검사해야 하므로 우리는 이 성질에 의존합니다.

이는 현재 타입 시스템의 불건전성 문제 때문에 성립하지 않습니다: #84533.

리전을 무시한 구조적 동등성은 의미적 동등성을 함의합니다 ✅

어떤 타입이 있을 때 lhs와 rhs 양쪽에서 모든 리전을 고유한 추론 변수로 치환한 뒤 그 타입을 자기 자신과 동등하게 만들면, 이제 구조적으로 달라졌을 수 있는 두 타입은 여전히 서로 동등해야 합니다.

이는 목표가 HIR typeck에서는 성공했다가 MIR borrowck에서 실패하는 것을 방지하기 위해 필요합니다. 이 불변 조건이 깨지면 MIR 타입 검사가 결국 ICE와 함께 실패합니다.

목표에서 얻은 추론 결과를 적용해도 그 목표의 결과는 바뀌지 않습니다 ❌

TODO: 이 불변 조건은 이상한 방식으로 서술되어 있어 더 자세히 설명해야 합니다. 요컨대, 이 검사는 솔버 버그가 있을 때에만 실패하기를 바랍니다: https://github.com/rust-lang/rust/blob/2ffeb4636b4ae376f716dc4378a7efb37632dc2d/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs#L391-L407. 이 검사를 다시 추가하고 어디에서 깨지는지 확인해 봅시다 :3

어떤 목표를 증명하거나 타입을 동등하게 만드는 등의 작업을 수행하고, 그 결과로 나온 추론 제약을 적용한 다음 원래 작업을 다시 수행하면 결과가 같아야 합니다.

안타깝게도 이는 몇 가지 골치 아픈 이유로 인해 적어도 새 솔버에서는 성립하지 않습니다.

트레이트 솔버는 지역적으로 건전해야 합니다 ✅

이는 impl이 존재하지 않는 목표에 대해 절대로 성공을 반환해서는 안 된다는 뜻입니다. 그렇게 하면 구현되지 않은 트레이트를 구현되었다고 가정하게 되며, 이는 실제 불건전성으로 이어질 가능성이 매우 높습니다. where 바운드를 사용하여 목표를 증명할 때에는 해당 항목의 사용자가 impl을 제공합니다.

이 불변식은 영역 제약을 검사하는 경우에만 성립합니다. coherence의 암묵적 부정 중첩 검사 중에는 영역 제약을 검사하지 않으므로, 그곳에서는 이 불변식이 깨집니다. 이 검사는 트레이트 솔버의 완전성에 의존하므로, 타입 outlives 목표에 대한 처리가 불완전한 현재의 영역 제약 검사인 InferCtxt::resolve_regions를 사용할 수 없습니다.

빈 환경에서 의미적으로 동등한 별칭들을 정규화하면 하나의 고유한 타입이 나옵니다 ✅

별칭 타입/상수의 정규화는 유일한 결과를 가져야 합니다. 그렇지 않으면 안전한 코드에서 transmute를 쉽게 구현할 수 있습니다. 다음 함수가 주어졌을 때, 입력 타입과 출력 타입이 항상 같은 구체 타입으로 정규화되도록 보장해야 합니다.

#![allow(unused)]
fn main() {
fn foo<T: Trait>(
    x: <T as Trait>::Assoc
) -> <T as Trait>::Assoc {
    x
}
}

현재 알려진 건전성 문제 중 상당수는 결국 이 불변식이 깨진다는 점에 기대고 있습니다. 그러나 이 불변식 없이 건전한 타입 시스템을 상상하기는 매우 어려우므로, 문제는 우리가 이 불변식에 잘못 의존하는 것이 아니라 불변식이 깨져 있다는 점입니다.

타입 시스템은 완전합니다 ❌

타입 시스템은 완전하지 않습니다. 타입 시스템은 불필요한 추론 제약을 추가하는 경우가 많으며, 목표(goal)가 성립할 수 있는데도 오류를 냅니다.

  • 메서드 선택
  • 불투명 타입 추론
  • 타입 outlives 제약 처리
  • 트레이트 솔버의 후보 선택 과정에서 Impl 후보보다 ParamEnv 후보를 우선하는 것

목표는 HIR 타입 검사(typeck) 이후에도 그 결과를 유지합니다 ✅

HIR typeck 중에는 성공하지만 MIR borrowck 중에 다시 평가될 때 실패하는 목표가 있으면 ICE가 발생합니다. 예를 들어 #140211이 있습니다.

HIR 타입 검사 중에는 성공하지만 인스턴스화된 후에 실패하는 목표가 있으면 건전하지 않습니다. 예: #140212.

이 제약을 유지하면서도 트레이트 솔버에서 어느 정도의 불완전성을 허용한다는 점은 흥미롭습니다. “허용된 불완전성“을 이 불변식을 깨뜨리는 동작과 명확하게 구분할 방법이 있다면 좋을 것입니다.

정규화는 결과를 바꾸어서는 안 됩니다

제네릭 별칭의 정규화를 허용하기 위해 이 불변식에 의존합니다. 이를 깨뜨리면 쉽게 건전성 문제로 이어질 수 있습니다. 예: #57893.

목표는 인스턴스화 후에도 여전히 오버플로할 수 있습니다

이는 재귀 한도에 도달하기 시작할 때 발생합니다. 또한 엉망인 발산하는 별칭도 있습니다. 이들을 어떻게 처리해야 할지는 불분명합니다 :3

빈 환경에서의 트레이트 목표는 유일한 impl에 의해 증명됩니다 ✅

트레이트 목표가 빈 환경에서 성립한다면, 그 목표를 증명하는 데 사용되는 impl이 사용자 정의든 내장이든 유일하게 존재해야 합니다. 이는 유일한 메서드와 연관 항목을 선택하는 데 필요합니다.

그러나 몇몇 경우에는 이 불변식을 깨뜨리는데, 일부는 버그 때문이고 일부는 의도된 설계입니다:

  • 마커 트레이트는 연관 항목이 없으므로 겹치는 것이 허용됩니다
  • 특수화는 특수화하는 impl이 부모 impl과 겹치는 것을 허용합니다
  • 내장 트레이트 객체 트레이트 구현은 사용자 정의 impl과 겹칠 수 있습니다: #57893

비어 있지 않은 환경에서 증명될 수 있는 목표는 단형화 중에도 성립합니다 ✅

제네릭 환경에서 어떤 목표를 증명할 수 있다면, 그 목표를 완전히 구체적인 타입으로 인스턴스화하고 스코프에 where 절이 없는 상태에서도 그 목표는 여전히 성립해야 합니다.

코드 생성은 이를 전제로 하며, 오버플로가 아닌 모호성을 만나면 ICE를 일으킵니다. 이 불변식은 현재 특수화(#147507)와 마커 트레이트(#149502)로 인해 깨져 있습니다.

일관성(coherence) 검사의 암묵적 부정 중첩 검사 중에는 타입 시스템이 완전합니다 ✅

중첩 검사에 대한 자세한 내용은 일관성 장을 참고하십시오.

일관성 검사의 암묵적 부정 중첩 검사 중에는 증명할 수 있는 목표에 대해 절대로 오류를 반환해서는 안 됩니다. 그렇게 되면 서로 다른 연관 항목을 가질 수 있는 impl들이 중첩될 수 있게 되어, 다른 여러 불변식이 깨집니다.

이 불변식은 실제로 우리가 의존하는 것임에도 현재 여러 가지 방식으로 깨져 있습니다. 이 불변식은 깨지기 매우 쉬우므로 주의해야 합니다:

  • 별칭의 일반화
  • 서브타이핑 바인더 중의 일반화 (다행히 일관성 검사에서는 악용할 수 없습니다)

트레이트 해결은 라이프타임이 서로 다르다는 사실에 의존해서는 안 됩니다 ✅

라이프타임이 서로 다를 때 어떤 목표가 성립한다면, 그 라이프타임들이 같을 때에도 성립해야 합니다. 그렇지 않으면 코드 생성 중에 단형화 이후 오류가 발생하거나, 잘못된 vtable로 인해 건전성이 깨집니다.

또한 서로 다른 라이프타임으로 목표를 먼저 증명한 뒤 나중에 그 라이프타임들이 같도록 제약되면 일관되지 않은 동작이 나타날 수도 있습니다.

본문에서의 트레이트 해결은 라이프타임이 같다는 사실에 의존해서는 안 됩니다 ✅

또한 트레이트 솔버에서 영역의 동등성에 의존하는 것에도 주의해야 합니다. 코드 생성에서는 지워진 영역을 모두 같은 것으로 취급하므로 이는 문제가 되지 않습니다. 하지만 HIR 타입 검사에서 MIR 타입 검사로 넘어가는 과정에서 동등성 정보를 잃을 수 있습니다.

이는 현재 새 솔버에서는 성립하지 않습니다: trait-system-refactor-initiative#27.

모호성을 제거하면 엄밀히 더 많은 코드가 컴파일됩니다 ❌

이상적으로는 코드가 컴파일되기 위해 모호성에 의존해서는 안 됩니다. 그렇게 하지 않으면 향후의 개선이 호환성을 깨는 변경이 됩니다.

불완전성 때문에 실제로는 그렇지 않으며, 추론을 개선하면 추론 결과가 바뀌어 기존 프로젝트가 깨질 수 있습니다.

의미적 동등성은 구조적 동등성을 함의합니다 ✅

타입 시스템에서 두 타입이 같다는 것은 제네릭 매개변수를 구체적인 인자로 인스턴스화한 뒤 두 타입이 같은 TypeId를 가진다는 뜻이어야 합니다. 그렇지 않으면 서로 다른 TypeId를 이용해 트레이트 선택에 영향을 줄 수 있습니다.

코드 생성 중에는 구조적 동등성을 사용해 타입을 조회하지만, 이것이 반드시 건전성을 깨는 것은 아닙니다

  • 중복된 메서드 코드 생성이나 백엔드 타입 검사 오류를 일으킬 수 있습니까?
  • CTFE 단언에서도 이에 의존합니다

의미적으로 다른 타입은 서로 다른 TypeId를 가집니다 ✅

의미적으로 다른 'static 타입은 transmute를 막기 위해 서로 다른 TypeId를 가져야 합니다. 예를 들어 for<'a> fn(&'a str)와 fn(&'static str)는 서로 다른 TypeId를 가져야 합니다.

상수 항목의 평가는 결정적입니다 ✅

상수 항목의 값은 타입 시스템에 반영될 수 있으므로, 상수 항목의 값이 모든 크레이트에서 항상 동일한 것이 중요합니다. 그렇지 않다면 “동일한” 상수 인자를 가져서 “동일한” 연관 타입이 되는 연관 타입이 생길 수 있지만, 서로 다른 크레이트에서 코드 생성 중에 정규화하면 실제로는 서로 다른 타입이 될 수 있습니다.

특히 이는 상수 함수로는 확장되지 않습니다. 타입 시스템은 상수 항목의 결과만을 다루므로, 상수 항목의 최종 값에 영향을 주지 않는 한 상수 함수가 비결정적이어도 실제로는 문제가 없습니다.