Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005673OCamltypingpublic2012-07-07 10:242015-12-11 19:08
Assigned Togarrigue 
PlatformMacOSMacOS XOS Version10.7.4
Product Version4.00.0+beta2/+rc1 
Target Version4.00.2+devFixed in Version4.01.0+dev 
Summary0005673: type equality a in polymorphic field
DescriptionA parameterized class signature in classdef.mli cause a type equality problem in the definition of a record with a polymorphic field 'poly' in

The problem appear or disappear with the presence or the suppression of an additional method ('cause_trouble' in classedef.mli).
Steps To ReproduceUntar the attached file. Just do "make". The program is 20 line in total on 3 files.
Additional InformationThe problem disappear if the method "cause_troubel" is removed or if its type does not involve the parameter of the class.

If the file anotherModule.mli is removed, the problem disappear in 4.00.0+beta2 but persist in 3.11 and 3.12.

I didn't try the trunk version.
TagsNo tags attached.
Attached Filestgz file icon PbWithPolymorphicField.tgz [^] (489 bytes) 2012-07-07 10:24

- Relationships

-  Notes
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
2015-12-11 19:08 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker