0005673: type equality a in polymorphic field

Notes
(0008654) garrigue (manager) 2012-12-27 08:16	Fixed in trunk, at revision 13164. This is a quick hack: I just replaced expand_head_unif by the safe version expand_head in moregeneral and eqtype. Unification will still fail for structural types. type refer1 = < poly : 'a 'b 'c . (('b, 'c) #Classdef.cl2 as 'a) > type refer2 = < poly : 'a 'b 'c . (('b, 'c) #Classdef.cl2 as 'a) > let f (x : refer1) = (x : refer2) The definition of f still fails for the same reason. In more detail, there is a bad interaction between universal type variables and constrained arguments. Expanding a type abbreviation is done by taking a copy of its body, and the unifying its formal parameters with actual arguments. In the absence of constraints, this unification always succeeds, even if the arguments contain universal type variables. But when there are constraints, the occur check for universal variables is activated, and this unification fails. To do things properly, one would need to introduction a notion of scope on unification variables, which would be an extensive change.

Issue History
Date Modified	Username	Field	Change
2012-07-07 10:24	giavitto	New Issue
2012-07-07 10:24	giavitto	File Added: PbWithPolymorphicField.tgz
2012-07-08 07:59	garrigue	Assigned To	=> garrigue
2012-07-08 07:59	garrigue	Status	new => assigned
2012-07-09 14:50	doligez	Target Version	=> 4.01.0+dev
2012-07-31 13:36	doligez	Target Version	4.01.0+dev => 4.00.1+dev
2012-09-21 14:46	doligez	Target Version	4.00.1+dev => 4.00.2+dev
2012-12-27 08:16	garrigue	Note Added: 0008654
2012-12-27 08:16	garrigue	Status	assigned => resolved
2012-12-27 08:16	garrigue	Fixed in Version	=> 4.01.0+dev
2012-12-27 08:16	garrigue	Resolution	open => fixed

Relationships