@andreasabel wrote the following:
The OP could probably be fixed by declaring
MyList : ++Set -> Setafter merging:
This does not quite work.
The following code is accepted (note that one has to manually specify that the first data type is strictly positive in its parameter, the inferred polarity is not used):
{-# OPTIONS --polarity #-}
data Box (@++ A : Set) : Set where
[_] : A → Box A
Box′ : @++ Set → Set
Box′ A = Box A
data D : Set where
c : Box′ D → D
However, the positivity checker rejects the final definition in the following piece of code, where Box′ has been made opaque:
{-# OPTIONS --polarity #-}
data Box (@++ A : Set) : Set where
[_] : A → Box A
opaque
Box′ : @++ Set → Set
Box′ A = Box A
data D : Set where
c : Box′ D → D
D is not strictly positive, because it occurs
in the first argument of Box′
in the type of the constructor c
in the definition of D.
I think this code should be accepted.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4