Importing `Cubical.Data.Nat` breaks `isOfHLevel→isOfHLevelDe

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)

如果我用一个洞替换isOfHLevel→isOfHLevelDep的自变量2，并询问Agda在这种情况下2的类型是什么，它显示：

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

这个问题是由2是某种重载的文字引起的吗？如何指定要使用类型为HLevel的2？

编辑以添加：如果我不使用文字，而是编写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问题记录下来。

尽管何时插入隐式应用程序的逻辑已经很棘手，因为它必须尝试并适应冲突的用例。