Open lawcho opened 3 months ago
I think it's rather because HVec doesn't use its index strictly postiviely, and Exp indirectly appears through that.
We don't support annotating indices with polarities, because atm we don't even know if it makes sense.
Wrt the error message, it does tell you the occurence precisely, but I agree we could also add the given polarity of the argument for each call.
I think it's rather because HVec doesn't use its index strictly postively, and Exp indirectly appears through that.
Thanks, that makes sense.
Wrt the error message, it does tell you the occurence precisely, but I agree we could also add the given polarity of the argument for each call.
This would make it much easier to find the non-++
positions in the cycle.
In fact, the non-++
positions are the only positions the user needs to see!
So I suggest a message like:
/home/lawrence/pre-release/east/src/bsugreport2.agda:26,3-41,42
Exp is not strictly positive,
because its definition depends on the expression:
(line 43) ... HVec (synArgs ...) ...
^^^^^^^^^^^^^
this sub-expresssion depends on Exp,
but is passed into the 1st argument of HVec
which is a position with polarity *
The new polarity checker (#6385) rejects this code:
I am not satisfied with Agda's error message:
I parsed this error message as:
Exp
is an inductive data typeExp
may only appear in its own definition at++
positionsExp
appears in its own definition at a*
position, because...Exp
occurs in argument 0 of the bound variablerec
rec
uses its argument 0 with polarity*
The error message is unsatisfactory because:
I explicitly wrote
(rec : @++ Set → Set)
,The error message contracticts this by saying
uses its argument with polarity *
The error does not tell me where the
polarity *
information came fromN.B. I think this is a separate bug from #7188, because if I replace the module parameter with a postulate, I get a similar error:
This error is even less satisfying, because:
argument 0
vsfirst argument
My Agda version is the latest commit (4573e2d) of the un-merged PR #6385.
I'm reporting via a new issue to avoid blocking the merge (no existing code is broken).