MantisBT - Core Inform
View Issue Details
0000753Core InformKinds and type checkingpublic2011-09-20 17:102014-05-07 07:33
Ron Newcomb 
graham 
normalmildalways
closedfixed 
PPCMac OS X10.4
6G60 
6L02 
(mild) Compiler accepts invalid code
0000753: I6 substitution returning a value can be used for any kind
In the attached source, foo is invoked with bar as a parameter, even though a value is not necessarily a device.
There is a room.
To decide what value is bar: (- 0 -).
To foo (X - a device):
foo bar.
No tags attached.
related to 0000648closed graham Property names typecast to a number and back again can not be typed 
Issue History
2011-09-20 17:10Ron NewcombNew Issue
2011-09-20 17:13Ron NewcombNote Added: 0001280
2011-09-20 22:05EmacsUserNote Added: 0001282
2011-09-20 22:13EmacsUserRelationship addedrelated to 0000648
2011-09-21 12:25Ron NewcombNote Added: 0001284
2011-09-21 15:22Ron NewcombNote Added: 0001286
2011-09-21 17:07EmacsUserEffect(serious) Compiler rejects valid code => (mild) Compiler accepts invalid code
2011-09-21 17:07EmacsUserNote Added: 0001290
2011-09-21 17:07EmacsUserSeverityserious => mild
2011-09-21 17:07EmacsUserStatusnew => confirmed
2011-09-21 17:07EmacsUserSummarythe type "relation of X to Y" cannot take "an arithmetic/enumerated value" or a kind variable K as subtype => I6 substitution returning a value can be used for any kind
2011-09-21 17:07EmacsUserDescription Updatedbug_revision_view_page.php?rev_id=545#r545
2011-09-21 17:07EmacsUserSteps to Reproduce Updatedbug_revision_view_page.php?rev_id=547#r547
2014-02-01 08:06grahamNote Added: 0002422
2014-02-01 08:06grahamStatusconfirmed => resolved
2014-02-01 08:06grahamResolutionopen => fixed
2014-02-01 08:06grahamAssigned To => graham
2014-05-07 07:32jmcgrewFixed in Version => 6L02
2014-05-07 07:33jmcgrewStatusresolved => closed

Notes
(0001280)
Ron Newcomb   
2011-09-20 17:13   
Test me with "examine me".
(0001282)
EmacsUser   
2011-09-20 22:05   
The source code is in fact invalid when those bits are uncommented.

If ``[arithmetic]'' is uncommented, the parsed player's command will have kind ``relation of 1-based indices to (relations of arithmetic values to word values),'' but the argument arr to the #-of substitution will expect type ``relation of 1-based indices to (relations of numbers to word values).'' Number is more specific than arithmetic value, but Inform relations are covariant, not contravariant, in their keys. So the code should read ``... (arr - a relation of 1-based indices to relations of arithmetic values to word values) ...'' instead.

If ``[K]'' is uncommented and ``word value'' is commented, K becomes the kind ``understood word'' according to the definition of ``the word.'' But then the parsed player's command has kind ``relation of 1-based indices to (relations of numbers [arithmetic values] to word values),'' instead of the expected ``relation of 1-based indices to (relations of numbers [arithmetic values] to understood words).'' Again, understood word is more specific than a word value, and Inform relations are covariant in their values too.

Hidden behind all of this is the issue that ``arithmetic value'' and ``word value'' aren't really kinds, but kinds of kinds, and therefore ``number'' and ``understood word'' aren't more specific in the same way that, say, ``person'' is more specific than ``thing.'' Also, something like ``relation of 1-based indices to (relations of arithmetic values to word values)'' is a kind of kind, meaning that its dangerous (and arguably invalid) to declare a phrase with such a return value (cf. 0000648:0001158).

Now Inform is still failing to give a helpful error message, but I traced that back, and it looks like the underlying cause is the same as for 0000739. I will leave a note with a reduced test case there, just in case the issues turn out to be separate.

The last question then, is why Inform accepts the source with no commenting changes. The same problem seems to come up whenever ``value'' is used in a return kind:

- - - -
There is a room.
To decide what value is bar: (- 0 -).
To foo (X - a device):
    foo bar.
- - - -

This case probably constitutes a distinct, accepts-invalid bug, albeit a non-issue if 0000648 is resolved by forbidding ambiguous return kinds. But I'll ask for other opinions before I reduce the report.
(0001284)
Ron Newcomb   
2011-09-21 12:25   
Doh, I did forget about the covariant / contravariant "direction".

Normally I'd just expose an array to I7 multiple times under different, specific types. "Pattern", for instance, has 4 different I7 names according to its return type. But I can't do that with Parse because the type depends on the VM, which means the I7 source code using it would need to use different names depending upon VM... ugh. I'm trying to hide these small differences so my readers can concentrate on how the algorithm works, hence the partially-vague return type.

I'll see if I can re-work things somehow.
(0001286)
Ron Newcomb   
2011-09-21 15:22   
Oh, and to answer the question about why Inform accepts the source with no commenting changes, I believe it's because I didn't actually try to use "the parsed player's command" in an I7 phrase, only in I6 phrases. I do get a Problem message when trying to do so:

>> I can't allow 'MoveWord' , because the phrase it gives a name to is generic, that is, it has a kind which is too vague. That means there isn't any single phrase which 'MoveWord' could refer to - there would have to be different versions for every setting where it might be needed, and we can't predict in advance which one 'MoveWord' might need to be.<<

So I believe your foo bar example is a separate issue.
(0001290)
EmacsUser   
2011-09-21 17:07   
Hmm. But that looks like the error one gets when naming a generic phrase, whether or not the phrase or the name is used.

Regardless, the foo bar bug isn't already on Mantis, so I've reduced and confirmed the report.
(0002422)
graham   
2014-02-01 08:06   
Inform now rejects "To decide what value is bar:" as being too vague about the return kind. Return kinds have to involve either definite kinds, or kind variables decided by the usage, or else be decided by the rules of arithmetic/dimensions.