Open txa opened 1 month ago
Positivity checking is not integrated with termination checking, see:
So you cannot write things like
data Ty : Set where
arr : (a b : Ty) -> Ty
variable a b : Ty
data Sem : Ty -> Set where
fun : (Sem a -> Sem b) -> Sem (arr a b)
Instead, you need ugly recursive definitions:
Sem : Ty -> Set
Sem (arr a b) = Sem a -> Sem b
Your example mutually defines U
, El
and El-sigma
and El-sigma
uses El
negatively (which in turn uses El-sigma
positively). So the positivity checker rejects it. The positivity checker is a syntactic device, it does not care about whether there is a semantically equivalent definitions that would be accepted.
Really we would like to fix #4563. This would albeit have semantic implications: a data
is then no longer always a conventional inductive type.
I am running into this problem several times. When I define a universe using a record the positivity checker complains but if I replace the record with an ugly Sigma type it is ok. Is this a known issue? Any chance of fixing it?
Here is an example :
leads to an error. Actually I don't want the record to be inductive but if I leave this out I also get an error (this is wrong). But if I use a product it works:
See the discussion on Zulip.