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

[Andreas Abel]

On 20.07.2016 15:23, Roman wrote:
>> 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.

The simple (and maybe sobering) answer is that Agda only analyzes data 
type parameters for their variance, not the indices.  In most cases, 
since matching is performed on the indices in the target types of 
constructors, they do not have an interesting variance anyway.

The question, of course, is if positivity in A could be justified in 
your example.  This, in turn leads to the question what your definition 
means.  We could attempt to write it as parameterized datatype.

   data Coerce β {α} (A : Set α) : Set β where
     coerce : (p : α ≡ β) → subst (λ ℓ → Set ℓ) p A → Coerce β A

Agda is not very happy with this, as the predicate (λ ℓ → Set ℓ) for 
subst is too big (lives in Level -> Setomega).

But type-theoretically, this could maybe made sense of, with additional 
universe(s).  Also, subst should be strictly positive in A, presumably.

One could think of extending the positivity checker to include the 
indices which behave as parameters.  For instance, in your definition

   data Coerce β : ∀ α (A : Set α) → Set β where
     coerce : ∀{A : Set β} → A → Coerce β β A

the index A appears as variable, so it could be treated like a parameter.

However, I am not very sure about this.  A solid research paper giving a 
theoretical justification would certainly make me more confident...

Cheers,
Andreas

>
>> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/