Opaque definition no longer strictly-positive

[flupe]

Opaque definition no longer strictly-positive

[jespercockx]

@plt-amy is this intentional? Could you please take a look?

[plt-amy]

This also happens if MyList is marked abstract. I think it's perfectly sensible: Agda doesn't track polarities in types (yet), so as far as the positivity checker is concerned, MyList is Just Some Set → Set. But I suppose I could be talked down from this position, and the fix is simple..

[andreasabel]

Maybe it makes sense for abstract, which is kind of trying to prevent any information about the abstract thing to leak (but no one uses it for that purpose).
If opaque is an explicit mechanism mainly to prevent unwanted unfoldings, it could allow positivity information to get out...

[plt-amy]

Like I said, my view could be swayed! I don't think it makes much sense for the positivity checker to see through opaque definitions like this, but since we don't support opaque data types (hence there would be no way to unfold MyList in the definition of B), it would be a sensible stop-gap.

[flupe]

I agree that the positivity checker should probably not know this by default, and positivity information should ideally be expressed intentionally in the type of opaque definitions with polarity annotations. Since they are not available (yet), an alternative could be to repurpose the POLARITY pragma for opaque definitions to explicitly decide whether to expose this information to the positivity checker.

opaque
  MyList : Set → Set
  MyList = List

  {-# POLARITY MyList ++ #-}

Could be coupled with a check that enforces that the given polarities do hold, in order to still allow this with --safe.