I've just fixed some bugs that were resulting in abstract sort constructors (and their intersections) in signatures not being assigned the variances implied by what what the signature designates.
In the process I decided that it would be good to double check that the variances of pre-existing sortnames aren't being clobbered. It turns out they can't be, because you can't ever specify sorts that refine a manifest type that was previously opaquely defined.
So, this issue is that CIDRE should support some way of doing this. Perhaps there should be multiple ways, following SML:
a) sharing specs that follow sharing type t1=t2 with (*[ and sortdef s1=s2 and ... ]*)
b) where type sigexps that similarly modify signatures
c) ([* sortdef s1 = s2 ]*) transparent sort specs.
Then it would be natural to support signatures that weaken what's known about the refinements. Alternatively, we could just consider that we have sufficient modularity at the level of types, and automatically propagate sorts along with the type that they refine.
Regardless, if CIDRE does in the future support such things, it would be good to revisit the propagation of variance for abstract sort constructors. Currently this is done by imperatively improving the variance of sortnames that are subsorts of sortnames that have a variance ascribed. If such improvements were done to sortnames that were defined prior to the current signature it would be bad.
I've just fixed some bugs that were resulting in abstract sort constructors (and their intersections) in signatures not being assigned the variances implied by what what the signature designates.
In the process I decided that it would be good to double check that the variances of pre-existing sortnames aren't being clobbered. It turns out they can't be, because you can't ever specify sorts that refine a manifest type that was previously opaquely defined.
So, this issue is that CIDRE should support some way of doing this. Perhaps there should be multiple ways, following SML: a)
sharingspecs that followsharing type t1=t2with(*[ and sortdef s1=s2 and ... ]*)b)where typesigexps that similarly modify signatures c)([* sortdef s1 = s2 ]*)transparent sort specs.Then it would be natural to support signatures that weaken what's known about the refinements. Alternatively, we could just consider that we have sufficient modularity at the level of types, and automatically propagate sorts along with the type that they refine.
Regardless, if CIDRE does in the future support such things, it would be good to revisit the propagation of variance for abstract sort constructors. Currently this is done by imperatively improving the variance of sortnames that are subsorts of sortnames that have a variance ascribed. If such improvements were done to sortnames that were defined prior to the current signature it would be bad.