[Agda] Why does Agda think this is not strictly positive?

[Roman]

> the problem seems to be that Agda
> cannot see that all constructors that target Coerce β A use A in a
> strictly positive way, since A is not a fixed parameter.

Ah, it didn't come to my mind that Agda treats parameters and indices
differently wrt positivity checking.

> Now, since B is fixed, it is easy for Agda to see that B is always used
> strictly positively, but this is probably not what you intended... (Of
> course, being able to coerce from Set α to Set β for arbitrary α and β
> would be too good to be true.)

I'm not trying to coerce from `Set α` to `Set β` for arbitrary `α` and
`β`, of course. The idea is the same as with propositional equality:
in `p : x ≡ y` `x` and `y` can be syntactically distinct terms, but
once you pattern match on `p` they will be unified. `Coerce` allows to
kinda postpone universes check: you can write `Coerce β A` as an
argument to a constructor and no matter where `A` lies, `Coerce β A`
will lie in `Set β`. The actual universes check will be performed when
constructing an element of `Coerce β A`.

Using `Coerce` we can define a type of universe polymorphic descriptions ([1]):

    {-# NO_POSITIVITY_CHECK #-}
    data Desc {ι} (I : Set ι) β : Set (ι ⊔ lsuc β) where
      var : I -> Desc I β
      π   : ∀ {α}
          -> Coerce (ι ⊔ lsuc β) (∃ λ (A : Set α) -> A -> Desc I β)
          -> Desc I β
      _⊛_ : Desc I β -> Desc I β -> Desc I β

The type signature of `π` encodes the fact that `lsuc α` is less or
equal than `ι ⊔ lsuc β`.

As you noted `Coerce β A` implies `α ≡ β`, which in the case of `π` means that

    lsuc α ⊔ ι ⊔ lsuc β ≡ ι ⊔ lsuc β

which is the same as `lsuc α ≤ ι ⊔ lsuc β` (if there would be `_≤_`
defined on levels). So we have a first-class encoding of cumulativity
as witnessed by the following example:

    pattern pi A D = π (coerce (A , D))

    open import Data.Nat.Base

    Vec : ∀ {α} -> Set α -> Desc ℕ α
    Vec A = pi Bool λ b -> if b
              then var 0
              else (pi ℕ λ n -> pi A λ _ -> var n ⊛ var (suc n))

In the second constructor of `Vec` one `pi` receives `ℕ` from `Set`
and another `pi` receives `A` from `Set α`, nevertheless the
definition is type checked, because both `lzero` and `α` are less or
equal than `α`.

`Coerce` can be defined as a function

    Coerce : ∀ {α β} -> α ≡ β -> Set α -> Set β
    Coerce refl = id

and then used like this

    data Desc {ι} (I : Set ι) β : Set (ι ⊔ lsuc β) where
      var     : I -> Desc I β
      π       : ∀ {α} {{q : α ⊔ β ≡ β}}
             -> Coerce (cong (λ αβ -> ι ⊔ lsuc αβ) q) (∃ λ (A : Set α)
-> A -> Desc I β)
             -> Desc I β
      _⊛_ : Desc I β -> Desc I β -> Desc I β

I'm using a similar definition in some actual code ([1]), but a
function confuses the termination checker, so I would like to switch
to `Coerce` defined as a data type.

[1] https://github.com/effectfully/Generic