Импорт Cubical.Data.Nat прерывает isOfHLevel → isOfHLevelDep

Question

Следующие небольшие проверки типов программы Agda:

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

module _ (A : Type) (P : A → Type) (PIsProp : ∀ x → isProp (P x)) where
  r : isOfHLevelDep 2 P
  r = isOfHLevel→isOfHLevelDep 2 λ t → isOfHLevelSuc 1 (PIsProp t)

Однако, если я также добавлю import Cubical.Data.Nat (мне даже не нужно его открывать!), Это не удастся:

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
import Cubical.Data.Nat

module _ (A : Type) (P : A → Type) (PIsProp : ∀ x → isProp (P x)) where
  r : isOfHLevelDep 2 P
  r = isOfHLevel→isOfHLevelDep 2 λ t → isOfHLevelSuc 1 (PIsProp t)

{a0 a1 : A} (b0 : P a0) (b1 : P a1) →
isOfHLevelDep 1 (λ p → PathP (λ i → P (p i)) b0 b1)
!=
(b0 : P a0) (b1 : P a1) →
isOfHLevelDep 1 (λ p → PathP (λ i → P (p i)) b0 b1)
because one is an implicit function type and the other is an
explicit function type
when checking that the expression
isOfHLevel→isOfHLevelDep 2 λ t → isOfHLevelSuc 1 (PIsProp t) has
type
(b0 : P a0) (b1 : P a1) →
isOfHLevelDep 1 (λ p → PathP (λ i → P (p i)) b0 b1)

Если я заменю аргумент 2 из isOfHLevel→isOfHLevelDep дырой и спрошу Agda, какой тип 2 в этом контексте будет, он покажет:

Goal: HLevel
Have: ⦃ _ : Cubical.Data.Nat.Unit ⦄ → Cubical.Data.Nat.ℕ

Is эта проблема вызвана тем, что 2 является перегруженным литералом? Как указать, что я хочу использовать 2 с типом HLevel?

Отредактировано, чтобы добавить : если я не использую литерал, а вместо этого пишу suc (suc zero), тогда это работает; но все же я бы хотел использовать там литерал 2.

Answer 1

На самом деле разница в том, что Cubical.Data.Nat импортирует оборудование для перегрузки литералов, даже если с одним экземпляром для Nat. HLevel должно быть просто Nat, кстати. Эта разница, кажется, заставляет Agda избегать вставки некоторых приложений с неявными аргументами.

Вы можете обойти это, добавив приложения с неявными аргументами в тело r:

module _ (A : Type) (P : A → Type) (PIsProp : ∀ x → isProp (P x)) where
  r : isOfHLevelDep 2 P
  r = isOfHLevel→isOfHLevelDep 2 (λ t → isOfHLevelSuc 1 (PIsProp t)) {_} {_}

действительно это (или меньший тестовый пример) должен быть задокументирован как проблема agda.

Хотя logi c для того, когда вставлять неявные приложения, уже сложен, поскольку он должен пытаться учесть конфликтующие варианты использования.