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

[Fredrik Nordvall Forsberg]

Hi Roman and Frédéric,

On 20/07/16 11:08, Frédéric Blanqui wrote:
>> This implies that Coerce β A is equivalent to (A -> Coerce β A)...
> Could you please give more explanation about that?

I'm sorry, this is of course rubbish. I misread the type, and was then
tricked into the false verification that D was empty, as Roman pointed out.

To get back to the original mystery, 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. (Would it be
feasible for Agda to find this out in general? There already seems to be
some kind of magic going on with arguments of constructors that are used
as indices as in Coerce -- The argument A would normally be too big to
fit...)

Towards a "solution", note that the type signature of Coerce looks
deceptively general; if we write out all implicit arguments and types,
it really is

data Coerce β : ∀ {α} -> Set α -> Set β where
  coerce : ∀ {A : Set β} -> A -> Coerce β {β} A

Indeed, Coerce β {α} is empty if α is not equal to β, as can be seen by
the following function (keeping the original definition of Coerce just
in case):

open import Data.Empty
open import Relation.Binary.PropositionalEquality

data Coerce β : ∀ {α} -> Set α -> Set β where
  coerce : ∀ {A} -> A -> Coerce β A

f : ∀ {α β}{A : Set α} -> (α ≡ β -> ⊥) -> Coerce β {α} A -> ⊥
f p (coerce x) = p refl

(we also only have Coerce β A isomorphic to A if A : Set β).

On 20/07/16 09:57, Roman originally wrote:
> Is there something I can do to make positivity check pass?

Hence, a disappointing way to pass the positivity checker is to use the
more direct definition

data Coerce' β (B : Set β) : Set β where
  coerce : B -> Coerce' β B

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.)

Best wishes,
Fredrik

-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.