1

以下小型 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询问 Agda2在该上下文中的类型是什么，它会显示：

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

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

编辑添加：如果我不使用文字，而是使用 write suc (suc zero)，那么它可以工作；但是，我还是想在2那里使用文字。

4

1 回答 1

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 问题。

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

于 2020-08-06T08:57:08.073 回答