Positivity check is incorrectly implemented

[ice1000]

data Dead : Set
open data Zaoqi (A : Type)
| essentially (A -> Dead)
open data Cat : Type
  | meow : (Zaoqi Cat) → Cat

def catIsDead : Cat → Dead
  | meow (essentially f) => f (meow (essentially f))

def catIsAlive : Cat
  => meow (essentially catIsDead)

def catIsBothDeadAndAlive: Dead
  => catIsDead catIsAlive

/cc @tsao-chi

[ice1000]

https://github.com/JetBrains/Arend/blob/master/base/src/main/java/org/arend/typechecking/covariance/CovarianceChecker.java

[HoshinoTented]

😱

[mio-19]

A more mature implementation would require explicit polarity annotations

References: https://github.com/agda/agda/issues/2411 https://github.com/agda/agda/pull/6385