Things like box, cap. This involves unleashing a couple power moves (already unleashed in the V types):
Checking of box should look at the dimensions and delegate to the right thing in case it is trivial (see Vin). for now, don't worry about if you are ignoring junk which appears in the term.
Checking of cap should do the same as above.
The main case for box should be implicit, as fhcom is treated as a negative type. We should "eta expand" the generic element of fhcom on the fly, and check that, if possible. This would be in harmony with the way that V-types and all other negative types are checked. This may be a little subtle to figure out.
Things like
box, cap. This involves unleashing a couple power moves (already unleashed in the V types):Checking of
boxshould look at the dimensions and delegate to the right thing in case it is trivial (seeVin). for now, don't worry about if you are ignoring junk which appears in the term.Checking of
capshould do the same as above.The main case for
boxshould be implicit, asfhcomis treated as a negative type. We should "eta expand" the generic element offhcomon the fly, and check that, if possible. This would be in harmony with the way thatV-types and all other negative types are checked. This may be a little subtle to figure out.