인스턴스 인자

인스턴스 인자 (Instance Arguments)

• 사용법 (Usage)
• 중복과 백트래킹 (Overlap and backtracking)
• 인스턴스 해석 (Instance resolution)

인스턴스 인자는 일반 암시 인자에 사용되는 통일(unification) 알고리즘이 아니라 특별한 인스턴스 해석 알고리즘에 의해 해결되는 특별한 종류의 암시 인자예요.

인스턴스 인자는 하스켈 타입 클래스 제약의 Agda 버전이며 같은 많은 목적에 사용될 수 있어요. 인스턴스 인자는 그 타입이 이름 붙은 타입(즉 데이터 타입이나 레코드 타입)이거나 변수 타입(즉 이전에 바인딩된 Set ℓ 타입의 변수)이고, 선언된 인스턴스와 현재 문맥에서 요구된 타입의 유일한 인스턴스가 만들어질 수 있을 때 해결돼요.

사용법 (Usage)

인스턴스 인자는 이중 중괄호 {{ }}로 둘러싸여 있어요. 예: {{x : T}}. 대안으로 적절한 공백과 함께 유니코드 중괄호 ⦃ ⦄(U+2983과 U+2984, Emacs 모드에서 \{{와 }}로 입력 가능)로 둘러쌀 수 있어요.

예를 들어 함수 _==_가 주어졌을 때

_==_ : {A : Set} {{eqA : Eq A}} → A → A → Bool

적절한 타입 Eq에 대해, 다음과 같이 정의할 수 있어요:

elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
elem x (y ∷ xs) = x == y || elem x xs
elem x []       = false

여기서 _==_에 대한 인스턴스 인자는 elem의 대응 인자로 해결돼요. 일반 암시 인자처럼 인스턴스 인자를 명시적으로 줄 수 있어요. 위 정의는 다음과 동등해요:

elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
elem {{eqA}} x (y ∷ xs) = _==_ {{eqA}} x y || elem {{eqA}} x xs
elem         x []       = false

이것을 활용하는 매우 유용한 함수는 임의의 목표를 해결하기 위해 인스턴스 해석을 적용할 수 있게 하는 함수 it이에요:

it : ∀ {a} {A : Set a} → {{A}} → A
it {{x}} = x

마지막 예제가 보여주듯이 인스턴스 인자의 이름은 타입 시그니처에서 생략할 수 있어요:

_==_ : {A : Set} → {{Eq A}} → A → A → Bool

타입 클래스 정의하기 (Defining type classes)

인스턴스 인자의 타입은 {Γ} → C vs 형태여야 하는데, 여기서 C는 postulate 이름, 바인딩된 변수, 또는 데이터/레코드 타입의 이름이고, {Γ}는 임의 개수의 암시 또는 인스턴스 인자를 나타내요 (비어 있지 않은 {Γ}의 예는 아래의 의존 인스턴스 참고).

명시적 인자를 가진 인스턴스도 받아들여지지만, 명시적 인자의 값은 자동으로 유도될 수 없으므로 인스턴스로 간주되지 않아요. 그러한 인스턴스를 갖는 것은 효과가 없어서 경고를 발생시켜요.

타입이 다른 어떤 것으로 끝나는 인스턴스 인자도 현재 받아들여지지만 인스턴스 탐색으로 해결될 수 없으므로 손으로 줘야 해요. 이러한 이유로 그러한 인스턴스 인자를 사용하는 것은 권장되지 않아요. 그렇게 해도 경고가 발생해요.

그 외에 인스턴스 인자의 타입에 대한 요구사항은 없어요. 특히 타입이 "타입 클래스"라고 말하는 특별한 선언은 없어요. 대신 하스켈 스타일 타입 클래스는 보통 레코드 타입으로 정의돼요. 예를 들어:

record Monoid {a} (A : Set a) : Set a where
  field
    mempty : A
    _<>_   : A → A → A

레코드의 필드를 인스턴스 인자를 취하는 함수로 사용 가능하게 만들기 위해 특별한 모듈 적용을 사용할 수 있어요:

open Monoid {{...}} public

이것은 다음을 스코프로 가져와요:

mempty : ∀ {a} {A : Set a} → {{Monoid A}} → A
_<>_   : ∀ {a} {A : Set a} → {{Monoid A}} → A → A → A

슈퍼클래스 의존성은 레코드와 인스턴스 탐색을 사용해 구현할 수 있어요. 모듈 적용이 어떻게 디슈가되는지에 대한 자세한 내용은 모듈 적용과 레코드 모듈을 참고하세요. 손으로 정의하면 mempty는 다음과 같을 거예요:

mempty : ∀ {a} {A : Set a} → {{Monoid A}} → A
mempty {{mon}} = Monoid.mempty mon

레코드 타입이 하스켈 스타일 타입 클래스에 자연스럽게 맞지만, 데이터 타입과 함께 인스턴스 인자를 잘 사용할 수도 있어요. 아래의 예제들을 참고하세요.

인스턴스 선언하기 (Declaring instances)

위에서 보았듯이 문맥의 인스턴스 인자는 인스턴스 인자를 해결할 때 사용 가능하지만, 구체적인 타입에 대한 최상위 인스턴스도 정의할 수 있어야 해요. 이것은 instance 키워드로 하는데, 이 키워드는 각 정의가 인스턴스 해석에 사용 가능한 인스턴스로 표시되는 블록을 시작해요. 예를 들어 Monoid (List A) 인스턴스는 다음과 같이 정의할 수 있어요:

instance
  ListMonoid : ∀ {a} {A : Set a} → Monoid (List A)
  ListMonoid = record { mempty = []; _<>_ = _++_ }

또는 동등하게 코패턴을 사용해:

instance
  ListMonoid : ∀ {a} {A : Set a} → Monoid (List A)
  mempty {{ListMonoid}} = []
  _<>_   {{ListMonoid}} xs ys = xs ++ ys

최상위 인스턴스는 이름 붙은 타입(이 경우 Monoid)을 목표로 해야 하며, 문맥의 타입에 대해 선언될 수 없어요.

let-표현식에서 최상위 인스턴스와 같은 방식으로 로컬 인스턴스를 정의할 수 있어요. 예를 들어:

mconcat : ∀ {a} {A : Set a} → {{Monoid A}} → List A → A
mconcat [] = mempty
mconcat (x ∷ xs) = x <> mconcat xs

sum : List Nat → Nat
sum xs =
  let instance
        NatMonoid : Monoid Nat
        NatMonoid = record { mempty = 0; _<>_ = _+_ }
  in mconcat xs

인스턴스는 인스턴스 인자 자신을 가질 수 있는데, 이것은 인스턴스 해석 중에 재귀적으로 채워져요. 예를 들어:

record Eq {a} (A : Set a) : Set a where
  field
    _==_ : A → A → Bool

open Eq {{...}} public

instance
  eqList : ∀ {a} {A : Set a} → {{Eq A}} → Eq (List A)
  _==_ {{eqList}} []       []       = true
  _==_ {{eqList}} (x ∷ xs) (y ∷ ys) = x == y && xs == ys
  _==_ {{eqList}} _        _        = false

  eqNat : Eq Nat
  _==_ {{eqNat}} = _≡ᵇ_  -- Data.Nat.Base에서 임포트

ex : Bool
ex = (1 ∷ 2 ∷ 3 ∷ []) == (1 ∷ 2 ∷ []) -- false

두 번째 절의 오른쪽 변에 있는 _==_의 두 호출에 주목하세요. 첫 번째는 Eq A 인스턴스를 사용하고 두 번째는 eqList에 대한 재귀 호출을 사용해요. 예제 ex에서 인스턴스 해석은 Eq (List Nat) 타입의 값이 필요하므로 eqList 인스턴스를 사용하려고 시도하고, 그것이 Eq Nat 타입의 인스턴스 인자가 필요하다는 것을 발견한 다음 그것을 eqNat으로 해결해 해 eqList {{eqNat}} 해를 반환해요.

참고: 현재 인스턴스에 대한 종료 검사는 없으므로 loop : ∀ {a} {A : Set a} → {{Eq A}} → Eq A 같은 비정상적인 인스턴스를 만들 수 있어요. 이런 경우의 루프를 방지하기 위해 인스턴스 탐색의 검색 깊이가 제한되어 있고, 최대 깊이에 도달하면 타입 오류가 발생해요. --instance-search-depth 플래그로 최대 깊이를 설정할 수 있어요.

인스턴스 탐색 제한하기 (Restricting instance search)

인스턴스를 현재 모듈로 제한하려면 private으로 표시할 수 있어요. 예를 들어:

record Default (A : Set) : Set where
  field default : A

open Default {{...}} public

module M where

  private
    instance
      defaultNat : Default Nat
      defaultNat .default = 6

  test₁ : Nat
  test₁ = default

  _ : test₁ ≡ 6
  _ = refl

open M

instance
  defaultNat : Default Nat
  defaultNat .default = 42

test₂ : Nat
test₂ = default

_ : test₂ ≡ 42
_ = refl

대안으로 --no-qualified-instances 플래그를 활성화해 Agda가 열린 모듈의 인스턴스만 고려하게 할 수 있어요 (자세한 내용은 아래 참고).

생성자 인스턴스 (Constructor instances)

인스턴스 인자는 레코드 타입에 대해 가장 흔히 사용되며 하스켈 스타일 타입 클래스를 흉내내지만, 데이터 타입과도 사용할 수 있어요. 이 경우 생성자를 인스턴스로 만들고 싶을 때가 많은데, 그것들을 instance 블록 안에 선언하면 이뤄져요. 생성자는 모든 인자가 암시 또는 인스턴스 인자인 경우에만 인스턴스로 선언될 수 있어요. 자세한 내용은 아래의 인스턴스 해석을 참고하세요.

인스턴스로 만들 수 있는 생성자의 단순한 예는 동등성 타입의 반사성(reflexivity) 생성자예요:

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x

이것은 사소한 동등성 증명이 인스턴스 해석으로 추론되게 해서, 전제 조건이 있는 함수로 작업하는 부담을 줄여줘요. 예를 들어, 자연수를 받아 Fin n(n보다 작은 자연수의 타입)을 돌려주는 함수를 정의하는 데 이것을 사용하는 방법은 다음과 같아요:

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

mkFin : ∀ {n} (m : Nat) → {{suc m - n ≡ 0}} → Fin n
mkFin {zero}  m {{}}
mkFin {suc n} zero    = zero
mkFin {suc n} (suc m) = suc (mkFin m)

five : Fin 6
five = mkFin 5 -- OK

mkFin의 첫 번째 절에서 불가능한 가정 suc m ≡ 0을 처리하기 위해 부정 패턴을 사용해요. 생성자 인스턴스의 또 다른 예는 다음 섹션을 참고하세요.

레코드 필드도 인스턴스로 선언할 수 있는데, 그러면 대응하는 투영 함수가 최상위 인스턴스로 간주되는 효과가 있어요.

한정된 인스턴스 (Qualified instances)

기본적으로 Agda는 한정된 이름(scoped qualified name)으로만 스코프에 있더라도 모든 인스턴스를 후보로 간주해요. 특히 임포트되었지만 열리지 않은 모듈의 인스턴스도 여전히 인스턴스 탐색에 고려된다는 뜻이에요. --no-qualified-instances 플래그를 사용해 Agda가 한정되지 않은 이름으로 스코프에 있는 인스턴스만 고려하게 할 수 있어요.

예를 들어 다음 Agda 코드를 생각해 봐요:

record MyClass (A : Set) : Set where
  field
    myFun : A → A
open MyClass {{...}}

module Instances where

  instance myNatInstance : MyClass Nat
  myFun {{myNatInstance}} = suc

-- --no-qualified-instances 없이
test1 : Nat
test1 = myFun 41

기본적으로 이 예제는 Agda가 받아들이지만, --no-qualified-instances가 활성화되면 먼저 Instances 모듈을 열어야 해요:

-- --no-qualified-instances 사용
open Instances

test2 : Nat
test2 = myFun 41

이 플래그는 모듈이 내보내는 모든 인스턴스를 반드시 사용하지 않고 모듈을 임포트하려고 할 때 특히 유용할 수 있어요.

예제 (Examples)

의존 인스턴스 (Dependent instances)

인자가 같을 때 동등성 함수가 증명을 만드는 Eq 클래스의 변형을 생각해 봐요:

record Eq {a} (A : Set a) : Set a where
  field
    _==_ : (x y : A) → Maybe (x ≡ y)

open Eq {{...}} public

간단한 불리언 값 동등성 함수는 Σ-타입 같은 의존성이 있는 타입에는 문제가 돼요:

data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  _,_ : (x : A) → B x → Σ A B

두 쌍 x , y와 x₁ , y₁이 주어졌을 때 두 번째 성분 y와 y₁의 타입이 완전히 다르고 동등성 검사를 허용하지 않을 수 있기 때문이에요. x와 x₁이 정말 같을 때만 y와 y₁을 비교할 수 있기를 바랄 수 있어요. 동등성 함수가 증명을 반환하게 하는 것은 x와 x₁이 같다고 비교될 때 정말 같다는 것이 보장되고, y와 y₁을 비교하는 것이 말이 되는 것을 보장해요.

Σ에 대한 Eq 인스턴스는 다음과 같이 정의할 수 있어요:

instance
  eqΣ : ∀ {a b} {A : Set a} {B : A → Set b} → {{Eq A}} → {{∀ {x} → Eq (B x)}} → Eq (Σ A B)
  _==_ {{eqΣ}} (x , y) (x₁ , y₁) with x == x₁
  _==_ {{eqΣ}} (x , y) (x₁ , y₁)    | nothing = nothing
  _==_ {{eqΣ}} (x , y) (.x , y₁)    | just refl with y == y₁
  _==_ {{eqΣ}} (x , y) (.x , y₁)    | just refl    | nothing   = nothing
  _==_ {{eqΣ}} (x , y) (.x , .y)    | just refl    | just refl = just refl

B에 대한 인스턴스 인자가 임의의 x : A에 대해 B x에 대한 Eq 인스턴스가 있어야 한다고 명시한다는 점에 주목하세요. 인자 x는 암시적이어야 해서, B 인스턴스를 사용할 때마다 통일로 추론되어야 함을 나타내요. 자세한 내용은 아래의 인스턴스 해석을 참고하세요.

중복과 백트래킹 (Overlap and backtracking)

기본적으로 인스턴스 해석은 인스턴스 사이에서 강요되지 않은 선택을 하지 않아요. 실제로 이것은 인스턴스가 중복되지 않을 수 있음을 의미해요: 인스턴스 목표를 해결하는 데 사용될 수 있는 후보가 여러 개 있으면 타입 오류가 발생해요.

예를 들어 디버그 표현을 출력하는 Show와 예쁘게 출력하는 Pretty라는 두 개의 별도 출력 클래스가 있다고 상상해 봐요. 꽤 많은 타입(예: 정수)이 동일한 디버그와 예쁜 표현을 가지므로, Show로 Pretty에 대한 "기본" 인스턴스를 가질 수 있습니다:

record Show (A : Set) : Set where
  field show : A → String
open Show ⦃ ... ⦄

record Pretty (A : Set) : Set where
  field pretty : A → String
open Pretty ⦃ ... ⦄

instance
  pretty-show : ∀ {a} ⦃ _ : Show a ⦄ → Pretty a
  pretty-show = record { pretty = show }

물론 어떤 값은 구별되는 표현을 가져요. 예를 들어 리스트를 cons-셀로 출력하는 대신 대괄호 안에 예쁘게 출력하고 싶을 수 있어요. 인스턴스를 씁니다:

postulate instance
  show-nat : Show Nat
  pretty-list : ∀ {a} ⦃ _ : Pretty a ⦄ → Pretty (List a)

하지만 숫자 리스트를 출력하려고 하면 Agda가 중복에 대해 불평해요! pretty-list 인스턴스가 pretty-show보다 엄격하게 더 구체적이지만, 이 상황에서 어느 후보도 적용 불가능하지 않으므로 Agda는 선택하기를 거부해요.

Failed to solve the following constraints:
  Resolve instance argument _r_273 : Pretty (List Nat)
  Candidates
    pretty-show : {a : Set} ⦃ _ : Show a ⦄ → Pretty a
    pretty-list : {a : Set} ⦃ _ : Pretty a ⦄ → Pretty (List a)

중복 인스턴스 (Overlapping instances)

위의 Pretty 같은 상황을 지원하기 위해 Agda는 여러 후보가 사용 가능할 때 무엇이 일어나야 하는지를 인스턴스마다 지정할 수 있게 해줘요. 이것은 다음 네 개의 프래그마 중 하나로 해요:

• OVERLAPPABLE 인스턴스는 엄격하게 더 구체적인 인스턴스를 위해 버려질 수 있어요.
• OVERLAPPING 인스턴스는 엄격하게 덜 구체적인 인스턴스가 버려지게 할 수 있어요.
• 편의 프래그마 OVERLAPS는 OVERLAPPABLE과 OVERLAPPING과 동등해요. 이것은 덜 구체적인 인스턴스가 버려지게 할 수도 있고, 더 구체적인 후보가 있으면 버려질 수도 있음을 의미해요.
• INCOHERENT 인스턴스는 다른 가능한 후보를 위해 임의로 버려질 수 있어요.

인스턴스 c1 : ∀ {Γ} → C xs는, 변수 Δ의 인스턴스화가 ys를 xs에 정의적으로 같게 만드는 것이 있으면 인스턴스 T2 : ∀ {Δ} → C ys보다 더 구체적이에요. c2가 c1보다 더 구체적이지 않고 c1이 c2보다 더 구체적이면 c1이 c2보다 엄격하게 더 구체적이라고 말해요.

Pretty 예제로 돌아가서, pretty-show 인스턴스를 OVERLAPPABLE로 표시하면 더 구체적인 인스턴스가 선택되게 할 수 있어요:

{-# OVERLAPPABLE pretty-show #-}
_ : String
_ = pretty (1 ∷ 2 ∷ 3 ∷ [])

pretty-list 인스턴스를 OVERLAPPING으로 표시하는 것도 가능했을 거예요.

중복 해석은 Agda가 강요되지 않은 선택을 하지 않도록 엄격한 구체성을 고려해요. 여러 후보가 "같은 구체성"을 가지면, 둘 다 겹칠 수 있는지 여부와 무관하게 인스턴스 제약은 여전히 해결되지 않은 채 남아요. 다음 상황이 예예요:

postulate
  C   : Set → Set → Set
  instance
    CIa : ∀ {a} → C Int a
    CaI : ∀ {a} → C a Int
  {-# OVERLAPS CIa CaI #-}

목표 C Int Int를 해결할 때 어느 후보도 다른 쪽을 위해 버려질 수 없어요. OVERLAPS 대신 사용해서는 안 되는 후보를 INCOHERENT로 표시해 직접 선택할 수 있어요.

백트래킹 (Backtracking)

기본적으로 Agda는 인스턴스가 적용 가능한지 고려할 때 인스턴스의 최종 반환 타입만 고려해요. 특히 인스턴스 탐색 알고리즘은 백트래킹하지 않고, 인스턴스의 제약이 충족되는지 여부는 중복 해석에 반영되지 않아요.

예를 들어 아래 코드에서 인스턴스 zero와 suc는 목표 ex₁에 대해 중복돼요. 어느 쪽이든 적절한 인자를 주어졌을 때 목표를 해결하는 데 사용될 수 있기 때문이에요. 따라서 인스턴스 탐색은 실패해요.

infix 4 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
  instance
    zero : ∀ {xs} → x ∈ x ∷ xs
    suc  : ∀ {y xs} → {{x ∈ xs}} → x ∈ y ∷ xs

ex₁ : 1 ∈ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []
ex₁ = it  -- 겹치는 인스턴스

하지만 중복을 확인하기 전에 적절한 인자를 찾았다면 위 목표는 유일한 해를 가질 거예요. --backtracking-instance-search 옵션은 인스턴스가 적용 가능한지 확인하기 전에 인스턴스에 대한 인스턴스 인자를 채워야 하는지 제어해요.

경고: Agda는 인스턴스의 제약을 확인하기 위해 순진한 백트래킹을 사용하는데, 최악의 경우 지수적 성능을 가져요. --backtracking-instance-search를 활성화하면 인스턴스 탐색이 크게 느려지고, 겉보기에는 무한 루프처럼 보일 수도 있어요.

인스턴스 해석 (Instance resolution)

이 섹션은 인스턴스 해석 알고리즘의 정확한 명세를 제공해요.

첫 번째 단계는 목표 타입이 인스턴스 해석으로 해결되기에 올바른 모양을 가지는지 확인하는 것이에요.

인스턴스 탐색은 {Γ} → C vs 형태의 목표만 해결할 수 있는데, 여기서 목표 타입 C는 변수, 데이터 타입, 레코드 타입 또는 postulate이고, {Γ}는 암시 또는 인스턴스 인자의 수열을 나타내요. 이것이 해당하지 않으면 인스턴스 해석은 오류 메시지와 함께 실패해요.

두 번째 단계는 초기 후보 목록을 계산하는 것이에요.

let-바인딩 변수와 스코프의 최상위 정의는 인스턴스 블록에 정의된 경우 후보가 돼요. 람다, 함수 타입, 왼쪽 변 또는 모듈 매개변수에 바인딩된 로컬 변수는 {{ }}로 인스턴스 인자로 바인딩되면 후보가 돼요. 이것은 매칭된 귀납적 또는 레코드 타입의 생성자에 대한 인스턴스 인자를 포함해요.

문맥의 로컬 변수가 슈퍼클래스 필드를 가지면 슈퍼클래스 확장이 적용돼요. 로컬 인스턴스 변수가 확장의 대상인지 결정하려면 그 타입을 head-정규화해야 한다는 점에 유의하세요.

타입이 {Δ} → C us인 후보만 고려되는데, 여기서 C는 이전 단계에서 계산된 목표 타입이고 {Δ}는 암시 또는 인스턴스 인자만 포함해요.

후보의 타입이 올바른 모양인지 또는 eta 레코드인지 여부를 결정할 수 없다면 인스턴스 탐색은 실행되지 않아요. 이는 로컬 인스턴스 변수가 (반환) 타입으로 메타변수를 가지거나, 그 타입이 다른 메타변수에 의해 막혀 있을 때 발생할 수 있어요. 이 메타변수가 차단되지 않은 후보 중 하나를 선택함으로써 해결되더라도 그렇죠.

초기 후보 목록은 가능한 해 집합에 대한 과잉 근사예요. 다음 단계는 각 후보가 실제로 인스턴스 목표를 해결하는 데 사용될 수 있는지 차례로 확인하는 것이에요. 목표가 {Γ} → C vs 형태이면 다음 단계를 취해요:

• 로컬 문맥이 {Γ}로 확장돼요. 이것은 추가 후보를 스코프로 가져올 수 있어요.
• 후보의 타입, 예를 들어 c : {Δ} → A가 새 메타변수, 예를 들어 α로 인스턴스화돼요.
• 목표 타입 C vs가 A[α/Δ]와 통일돼요. 이것이 확실한 불일치를 초래하면 후보는 버려져요.
• 마지막으로 --backtracking-instance-search가 활성화되어 있으면 Δ에 있는 인스턴스 변수들에 인스턴스 탐색을 재귀적으로 적용해요.

이 모든 단계가 성공하면 항 λ {Γ} → c {α}를 잠재적 해로 기록해요.

이전 단계는 재귀 인스턴스 탐색이 활성화되었더라도 여러 잠재적 해를 남길 수 있어요. 이제 엄격하게 더 구체적인 후보에 의해 겹쳐진 잠재적 해를 제거해요. 즉, 후보 쌍 c1 : {Δ} → C xs와 c2 : {Γ} → C ys가 주어졌을 때, 다음 경우에만 c1을 목록에서 제거해요:

• Γ의 변수들로 Δ의 변수들에 대한 치환이 있어 C xs와 C ys를 정의적으로 같게 만들어요. c2가 c1보다 더 구체적이라고 말해요.
• Δ로 Γ에 대한 그러한 치환이 존재하지 않아요. 이것은 c2가 c1보다 엄격하게 더 구체적이게 해요.
• c1이 겹칠 수 있거나(overlappable) c2가 겹치는(overlapping) 중 어느 하나. OVERLAPS(또는 INCOHERENT)로 표시된 인스턴스는 겹칠 수도 있고 겹치게 할 수도 있다는 점을 명심하세요.

중복을 해결한 후 우리는 다섯 가지 상황에 있을 수 있어요:

• 비-비일관적(non-incoherent) 후보가 정확히 하나 있고, 몇 개의 비일관적 후보가 함께 (있을 수 있음). 비-비일관적 후보가 선택돼요.
• 모든 잠재적 해가 비일관적. Agda는 임의로 선택해요.
• 여러 후보가 있고, 모두 overlap 키워드로 표시된 인스턴스 필드에서 옴. Agda는 다시 임의로 선택해요.
• 여러 비-비일관적 후보가 있음. 인스턴스 제약은 목표 또는 후보에 대한 더 많은 정보가 있을 때까지 연기돼요.
• 후보가 전혀 없음. 이것은 즉각적인 오류예요.

타입 체킹 끝에 남은 인스턴스 문제가 있으면 대응하는 메타변수가 그 타입과 소스 위치와 함께 Emacs 상태 버퍼에 출력돼요. 잠재적 해를 일으킨 후보는 show constraints 명령(C-c C-=)으로 출력할 수 있어요.

더 알아보기 (Learn more)

• Agda 문서: 인스턴스 인자 원문