Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type unsoundness bug with polymorphic variants #8134

Closed
vicuna opened this issue May 5, 2003 · 3 comments
Closed

Type unsoundness bug with polymorphic variants #8134

vicuna opened this issue May 5, 2003 · 3 comments
Labels

Comments

@vicuna
Copy link

vicuna commented May 5, 2003

Original bug ID: 1673
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Hi,
I've attached a gzipped tarball which causes the problem on 3.06 and above,
including the latest CVS snapshots. See the file test.ml. At the very end I
call a function on a type I shouldn't be able to and get a segfault. The code
essentially follows the code in Jacques Garrigue's "Code reuse through
Polymorphic Variants", but the application is modeling an evaluator for
abutting rectangular geometric structures on a plane. Run

touch depend
make depend
make
pvtst

and you'll get the segfault.

All attempts to create a cell.mli file for cell.ml failed. ocamlc -i 

generated a "signature" which didn't match. So I guess this is two bug reports,
one for the unsoundness, and one for this behavior, but I guess they are
related.

-- Brian


�‹���ض>��bug.tar�í�ksÛ62_?¿�u’‰è‘eÉÏ«zÌŒã8­oòðØÎ4?ÔU
²?ð¡’”-M“ûí·»�H?¢d·‰?ÉĘÄ�?ž°Ø]@K_�Áú½›míöV{w{�>ÛíÝ?ò§n÷°�ÚV»
ý?vg{ç�Û¾a¾¨MÒŒ'ŒÝë?“¥pW?�£ÍÇõÇ?­0¸)�°ží?­ö¢õß�ëÐ뿱½³¹ ð?­Í?{¬}S Ùí;_ÿx,"ö³ˆC‘%3‡žNE�ʈ�Ž�ˆŒ%Âg>��–ŠÈ<õÑ�N"6ek?­¡©ûÓOŽ“ÍÆ‚¡=õd”!ü_�ƒF=���ë²½,�[ÙOE¿\4ðAFƒº~1ÍD”¥0d8o?c g?d ��à'�dj?Å“,?‘˜›Îx’ð��~Ò‚4�ñ&{ÔwYŸ§ÒïÑì4K&~6I�ó�å[öî¹àC��Ù#�=�Ù»ãø’�û £êÜ?�»ó¬J�‘ƒ¾�yGAˆ§Ô±Z(Öá ™�H�ñûq�=�%‚'äòíc�œÏ?�Q/ÕY�5�jAÿ¢���Õ•ñÍñŠPJåLM��Ü�!,�ÌÍ¿— ´��*�?ã� ù…��‘�"Z  PäÊæÉSD«ä<‹œEÈSHr2´†SèV«95ý¸–~�¤„|¨p �Î����I˜ãa�™¬Ñ˜§�È�ZñrÔóJñ,z’}‚'M4�æ<¶‡öÔ’‘Ì�§%V�” �?LhŠðxm™?Ì­É„\—d"NK¬?L(�À*™Î…bIy?neW¡Ÿ*\�LF÷Õè5‹^·�SÁY�w âš-P?Èûš¬G$ò�E¢Œ�åC9kôlaê¹U�÷z–a{=P&2P!•ŽâË�y�–ò|…�ð÷FÙðý<�áha_0˜À�­¬¨¾aœ !°6Ëb6NÄ€� bâXâB>Ʊ‘ˆôz'¬ë±��ö�[i²�øh(ZçÈ��r N�©˜›P�9ˆ#?–ôCbÉ„�Š�?¥1¯�Å�a¯¯1Àr«èqÎ/Õ@“Ž•ë úÊ Bžù#†DÙ¥ÌF4]9�2’•�¾v•�Ô¤À-BE� šà‚5I”ú „r‘i��ò± Éä­ÑÌP�ô ¨¹6†£�5ÒJÇôÉVK½}88ëþçaúx…¨7lcQ´Ü"ˆùW²ë��»®? Ê-lùëp›ç.8¨pSö’[LÑ?iË×NþZ£ü?ä�D�²¢�¢¡òÿ­…ç¿­NÇäÿ?m<'t:;?Í»üÿ6Úú�2àu�n½/£õØça0�c¶
ÇAI�Á£· GD�§��|?dk>Ó'Hç™ �ìQõ�.ŸòìN{�\ñˆ'܇t<e›;k›»]çt$S&¦�FÒTÆ��Aêˆ)1l|H‚û˜]ŸG¼>OÕ©)¦›�¡òìþ�r–”?��áI
Ñ }1á�àÌA3ï²ÕÕUö–8ôÃøŒ�$ �µ?ïÕ�Ðþ×�|S4®Úÿ››Ûæþg“úñüß¾Ûÿ·Ñ2}Ø‡Í »ŒãI�¾Aî«�Æøà˜Ý²�ÀF’CO¯�?‰4S¸
•k@Osèé2语Üo Ñþ��Žq�žû†h,ßÿ?ÍN{ÓÄÿÝ?­�Šÿ�[wûÿ6ÚýÕ/Ñî;÷ë�L�»-Çóªÿ^ø™¼�l�R?�Žç�ós$E�©Å¯B¦M8þÆïጱŸH°  É�_��î±ãØÿs""?ž$Ù
ñ³�?g‰<�e¬óã?ÿfx?&3È|^ò Ò(�08„���² øÏà€t�Á¹�N¨�8c"3xdo��Z ´�{*ñø�I�dNq�ÌX�ÆÆèP)?k]­ŸÏ‘ë�Ùa-C?‹H$ÒgÆÏÑ=FÅšŽ’ø<áa �–4ö4ö'xC@ºfõ@�ªå4Æ�”e˜ä�º]è_[c¿Å��Nðè)§xYÂ.x�+��õC"y�˜<yõúxÿà„õE�_¶jã´n�ðã4¼ãF�3°<%Q
ß|?��§-·BÚO�Ï�ã4l2ü&° Çg�}?Å��”gþD���ð¥ ðæ
t #"­€xäK‘�·Ù¥�Óø�ãÁ�XhâÒpmpø³Á ?„c²60´’¢€]€~?òs­–Š�A¹2��h%���é��r‡ ¥³4�aS?&”Aî¯&*P [Ï·á¶:™åª �a|¡h‰©ð'�­�^œãÏ!Ø­Ù�(õÏcó�Á#…ÌpNº§É�'»ôñ:I?&öäxœ¡?}vs–�û5‘ µï .@? î�×LÙy©áz�’u²K�ex�h¬Ÿ.Ó´ñ�Úl²�\•½!�ÃÁ›ƒý¦º…�¯‡�›xíhc?ûd—�ý3nhB?ᬇ�]?„y¦Çb,��˜Ž…/Á‰�²Ÿ�a° €º?ƒü49Ò�C��î
 3�I�–™'}™Á¼�ÞŽú’εÑ$ìñ· Vs> ٰμðO_Y5Y«Õr�ÝÌìѪ�ØóÃ''(#v�Wà› �t—sÛbÏb´•B?™qD‚�>5øŒf�¤��¿�žþòóñÞÑ/‡û'.j
‡¼J?ꋼ�Ÿ�^�ÍÌâ
ã�<��1^
Ãf?@iÖêÙxðW ¥×´–5
þúåá›èë� �Îó"�r_T&œœ�WákÔ®�c
y$Ç0F¾¼Œçåë�s<Ö-.H—?àü�ÑeÌý�ü�Áé/Ç�{Oçpôg™X£???À��ª�?}ò¢:å)Ï8{ÂA×/x��’bÊR/À�À�ÁÒ\�²œ¥Ž�ü°H�¥ùJ¦õaOE½|wPðIY�üt0� ¶ñ¾hÆ}Ÿü$>�bZ R[&¨yê숗Pùù��òó�>èk&F‡Â0p4}Ë#S¼ÊðD �Ä;ÇÑ›�|‘¥Ùr©-—ö÷Å7^;mYÛ���ÝMÑþåèLb�
�£,ÜŠ™‰®?bhÈý�ì$���Ò˜?ø�‰Æ�j?Å“”­�bh€U�²¯ö÷^<?}u�–îíœû8°?±Äƒ=oÀÜâ>ϱ�ŠNšöêè´v�P5�5ˆÝMSŸ��ÕN…°êXãy�Mz~ð¦v�XŽc?ç}4é·½ýýºIh{Ž�Ptê•3)�­Cáÿ1,˜�E˜°�SžYah‘·Ô^�ݘù��Ê|E'c¾k�áþŽÙWC»�ò¶‹¼ðÉ(ž�À—P?"fk>D?84�±â?�?x�’�@€ü� d_å�Ʀú��}0!?Ì°?»!á��ˆ� ¸�ŠÍR�Sû¯ON_½ð4#ÈäS1ä“€bY†N@3ƒÂ¬�[ªe ã?xt�¤•��Ë� /�‡-�ÅH|�åëböMË)…�Ï�––�rÐ?�hØZ?‡�Óó|}’&ëo:?ã?uê0?Ðå8y(ò&�|ʨ°GAìñ ´”Ç¡C
SHñ �¨ð‚=
ÂÄ Odž2œîT �'¼A?,ƒÀÖé‡�fxš÷q&.\Ó¯}nŽ8OŸŽ�cžÐÏ}zÕÏÕ�m�øe Ù?æÅ1™ùdŒfk<éç²æ@ºÞÕ™=ì: �Å趺汅ɶsß8B½Å€)tÑÊÙ²’?©! hKì?ì*Ǫ–v�vÛ�j‘�ÃXΤ1ÌZ�h¤Ë§çv[;Ÿlx9‚|çÔ" ]´�?±öÚùµ–¯³‰�E�ýÐ…LaæÁ�× oØÃ���Ôø«'ÿ=±Ç6pÌÃ+j�;:]8<��ÒÖƒf„p®ó¯� Š«èï•›tÙZl¬ >ÑÍ»9¸c™�!Qôr<ð\3¿‹ "�¸kOrZ'¯Ÿ=;|�â[_�&O”Iѵ;ݙӕ:ª�ÿÌb¨nþ-þ×|öà?4"éWƒÚ!º¤/3›?•1B wq¤Œe•�:
<]�œ#ÎÁg%Ü�é� —‹�ÎJ�«�J�år>äõøPR†Áœ?
?5?£qèú�ú�°ù![�boe<=c«ÿc-ø��õ¾�3^­ü¨¼šr|]Ë„sû‚tÌ­ÿ�ØQ�}~it÷+Ë·Üè÷�}€º)�Wüþ»½³»iýþKõ�Ûí?»ß�n£-«ÿ¦§}0�UM5˜„ᬨ¡üË
êöØ
?®ÌUu×�Q]w툩ìöX£Ýl»s�Ý�{{VSÉ
Ý�?ž©Âí‚U
çÃ�tH�幌˜§?âc�âµq’ºõe/x–@jy”O�)U
+³^¨†�2¤?36ÔE±ºZR�5nú
?@‘·¢ 
?LÓR
¥Â�ç5‡
Ã$JùPôR?xj
"©&–¨7°èÞÕÓLm$¶F�Q6 ÊÅ{G¼Z1\†�´”ª�Ø”6§ªV7ÍËrÓ’l¦þVâêHö>�¬«�&�»†²¾.¸�¬R�¬¨}*W�ê…ðJËRÈSfÖL|§åVà–B蹇U‰Ãªê8äQ^‰ð�AuÕv•²žYÔ«rŽãnAº‚µ¼?Ó�«µJT¨¨�«ÌN«LU«t?•É¥V�¨ÂZ#„ª³å0)Ç¡°¼¯b™ÙX¬²ß?��¶Rÿ«Ú�UÀï]�Úª�®N^8�m¿f�™pIŸy©pã�Ô ×�òU�ÃÅ�»j˜§úõ‹¢|�[] 1¶ûµïž¬=&ÏÜ*ËUÔÐêé�s«o4pk4i—?a#�¡[ÔòæšÊ«u­?qEuqh�Í|Í®Bô�I{��MÚ¤ðå h<LWÊ«?o↽�Šº^Ãæõj{�ü™{À�««¬ìâWu‰pÏ*…ç�"íuvÊo�À3 �¡äª¤»AåÜ+�4�WÚÓ°Èu]ë5�ôƒ6¶\?ôÞ�nç<žº�qûÝ�œM�Ók(ZO?�ãTr¶Š}‘S?Ü9(+(Î�® ¾T}zU¨ K=õJ?y3§A?eiìð»RLZ±ßñ°dâò¯(�1S•Š:—HULB©œ<’tv¦¹dÊÔZyÀ…?²˜�Ùê�•n Ü"Qõð"a¥‹Ž·W3òÞVƒa¾g½òe´aÆ–(¤4ÝÒ‰�0ô%iA(íiÓ.<˜mY0Á�Õ–b?ZËU�-´o4Oðe¹Ì”†öQCí£Òl ’„­¨� S¼²–)x§ß#íŸ�Ëpª?q$’�ðÕ°‘[Ã’Ž4R5¦È�?H�
Ã3¯PžÓEy™f!õ�E÷Ëœ»õù¯øUí‹`-·+ëÿ76‹÷�ñ]€ÎÆÖnçîüw�?Šãqý{©�ÐAŠ½{�'Ù�S‡�8_Ñ—��F�Ÿ¿
õyˆ¿¾ƒÁ˜—Xé-[ó~ a«y¥—YtºÅ÷Ò z�·þ½^
�ð™HêQ_Ê�ðÛeÕ)�1®í��NäE�Õ§ïë>‹ö¿ù­ý†h\µÿÛ�ùû?Û?MõþOû®þ÷VšÚ¾� )3øŽß„û>�í�»Äæ�h\µÿ;VüßØÅú�ð�Ûwûÿ6šŠß
ìâuZÆVé]9ÕmÝØå—¨Ý�ª|“ª�¾³øy×îÚ]»kwí®}‹íÿ?ߨ �P��----------------

@vicuna
Copy link
Author

vicuna commented May 7, 2003

Comment author: administrator

On Thu, 8 May 2003, Jacques Garrigue wrote:

Indeed, the behaviour of type definitions seems to differ in .ml and
.mli, the .mli being probably the right one. I'll look into this.

The problem is your use of 'b = ('a,'b) structure in place of the real
constraint: in order to allow polymorphic type definitions, each
individual definition in the mutual recursion should be
self-contained, with exact constraints.

So the right formulation would be
type ('a, 'b) cell = 'b * cell_intf
constraint 'b = [> ('a, ('a, 'b) inst) basic_cell_structure ]
and ('a, 'b) structure = 'b
constraint 'b = [> ('a, ('a, 'b) inst) basic_cell_structure ]
and ('a, 'b) inst = {
inst_cell : ('a, 'b) cell;
inst_placement : Geometry.placement;
inst_name : string;
} constraint 'b = [> ('a, ('a, 'b) inst) basic_cell_structure ]

This allows you to write a .mli.
But then you have an error line 91 of test.ml, so I expect there is
something else wrong in your program.

I rewrote the type as you suggested, and split the Matrix module out of
test.ml so that I could see what the Matrix types look like.

Somehow, I'm not getting the open polymorphism that I want, as the Matrix
module's Matrix tag isn't reflected in the types and the pattern match in the Matrix module's show_rec function warns that the Matrix case is
unused.

I was expecting to be able to extend the the type cell, much as you extended
the evaluator in your paper. The type variable 'b was to be for the open
recursion, with 'a an orthogonal addition to parameterize over leaf types,
but is unnecessary for the understanding of this problem. Since it's really a
direct map of the simplest (non OO, non-lazy, ...) version of the evaluator
form your paper, I'm a bit puzzled as to why your evaluator works and is
extensible and myine isn't.

-- Brian

@vicuna
Copy link
Author

vicuna commented May 8, 2003

Comment author: administrator

From: brogoff@speakeasy.net

I've attached a gzipped tarball which causes the problem on 3.06 and above, 

including the latest CVS snapshots. See the file test.ml. At the very end I
call a function on a type I shouldn't be able to and get a segfault.
[..]
All attempts to create a cell.mli file for cell.ml failed. ocamlc -i
generated a "signature" which didn't match. So I guess this is two
bug reports, one for the unsoundness, and one for this behavior, but
I guess they are related.

Indeed, the behaviour of type definitions seems to differ in .ml and
.mli, the .mli being probably the right one. I'll look into this.

The problem is your use of 'b = ('a,'b) structure in place of the real
constraint: in order to allow polymorphic type definitions, each
individual definition in the mutual recursion should be
self-contained, with exact constraints.

So the right formulation would be
type ('a, 'b) cell = 'b * cell_intf
constraint 'b = [> ('a, ('a, 'b) inst) basic_cell_structure ]
and ('a, 'b) structure = 'b
constraint 'b = [> ('a, ('a, 'b) inst) basic_cell_structure ]
and ('a, 'b) inst = {
inst_cell : ('a, 'b) cell;
inst_placement : Geometry.placement;
inst_name : string;
} constraint 'b = [> ('a, ('a, 'b) inst) basic_cell_structure ]

This allows you to write a .mli.
But then you have an error line 91 of test.ml, so I expect there is
something else wrong in your program.

Jacques

@vicuna
Copy link
Author

vicuna commented May 13, 2003

Comment author: administrator

two bugs fixed by JG (2003-05-13)
subst.ml, ctype.ml, typedecl.ml

@vicuna vicuna closed this as completed May 13, 2003
@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant