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 equality a in polymorphic field #5673

Closed
vicuna opened this issue Jul 7, 2012 · 3 comments
Closed

type equality a in polymorphic field #5673

vicuna opened this issue Jul 7, 2012 · 3 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Jul 7, 2012

Original bug ID: 5673
Reporter: giavitto
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:08:32Z)
Resolution: fixed
Priority: normal
Severity: minor
Platform: Mac
OS: MacOS X
OS Version: 10.7.4
Version: 4.00.0+beta2/+rc1
Target version: 4.00.2+dev
Fixed in version: 4.01.0+dev
Category: typing
Monitored by: @hcarty

Bug description

A parameterized class signature in classdef.mli cause a type equality problem in the definition of a record with a polymorphic field 'poly' in anotherModule.ml.

The problem appear or disappear with the presence or the suppression of an additional method ('cause_trouble' in classedef.mli).

Steps to reproduce

Untar the attached file. Just do "make". The program is 20 line in total on 3 files.

Additional information

The 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.

File attachments

@vicuna
Copy link
Author

vicuna commented Dec 27, 2012

Comment author: @garrigue

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.

@vicuna vicuna closed this as completed Dec 11, 2015
@vicuna
Copy link
Author

vicuna commented Oct 17, 2018

Comment author: @trefis

To do things properly, one would need to introduction a notion of scope
on unification variables, which would be an extensive change.

Could the new scope field which appeared recently on type_expr be used for this?
That is: could you give some details regarding what change you had in mind? Was it an "extensive change" mostly because of the plumbing (which has now hopefully been done)?

@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.00.2 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
@garrigue
Copy link
Contributor

By scope, I mean a list of universal type variables that are allowed to occur in an expression. I have not thought of whether this could be done with levels, but this is a good question. This would probably involve some copying.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants