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

Question

The following small Agda program typechecks:

{-# 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)

However, if I also add import Cubical.Data.Nat (I don't even need to open it!), this fails:

{-# 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)

If I replace the argument 2 of isOfHLevel→isOfHLevelDep with a hole and ask Agda what the type of 2 in that context would be, it shows:

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

Is this problem caused by 2 being some kind of overloaded literal? How do I specify that I want to use 2 at type HLevel?

Edited to add: If I don't use a literal, and instead write suc (suc zero), then that works; but still, I'd like to use a literal 2 there.

Answer 1

Indeed the difference is that Cubical.Data.Nat imports the machinery for overloading of literals, even if with just the one instance for Nat. HLevel should just be Nat itself btw. This difference seems to be causing Agda to avoid inserting some implicit argument applications.

You can work around this by adding implicit arguments applications in the body of 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)) {_} {_}

indeed this (or a smaller test case) should be documented as an agda issue.

Though the logic for when to insert implicit applications is already tricky, since it has to try and accommodate conflicting use cases.