i.e. we should be able to infer that the constructor has sort S because of the signature. I don't think this is too hard to implement. We should add an additional case for parsing constructors that omits the surface::PathExpr and change the surface + fhir structures to an Option.
This should leave us with two places where we need to handle not having a path for the constructor:
mod/conv (conv from fhir to rty): For this, I think we can do the same thing we do for records.
wf/sortck (sort checking): For this, I'm not exactly sure what we'd want to do - I think that we would omit the path checking entirely but this may not be the right thing.
Right now, the constructor syntax is a bit redundant. e.g. this annotation:
Could be a bit simpler:
i.e. we should be able to infer that the constructor has sort
Sbecause of the signature. I don't think this is too hard to implement. We should add an additional case for parsing constructors that omits thesurface::PathExprand change thesurface+fhirstructures to anOption.This should leave us with two places where we need to handle not having a path for the constructor:
mod/conv(conv fromfhirtorty): For this, I think we can do the same thing we do for records.wf/sortck(sort checking): For this, I'm not exactly sure what we'd want to do - I think that we would omit the path checking entirely but this may not be the right thing.