Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007298OCamltypingpublic2016-07-20 19:132016-10-20 04:27
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.04.0 +dev / +beta1 / +beta2 
Target Version4.05.0 +dev/beta1/beta2/beta3/rc1Fixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0007298: GADT matching allows dummy method to escape
DescriptionThe following code fails to type-check:

  type t = T : t

  module M : sig
    type free = < bar : t -> unit; foo : free -> unit >
  end = struct

    class free = object (self : 'self)

      method foo self = ()

      method bar T =
        self#foo self

      end

  end

with the error:

  Error: Signature mismatch:
       ...
       Type declarations do not match:
         type free =
             < bar : t -> unit;
               foo : (< bar : t -> unit; foo : 'a -> unit > as 'a) -> unit >
       is not included in
         type free = < bar : t -> unit; foo : free -> unit >

but if we use non-GADT syntax for the definition of [T] then there is no error.

I'm not sure how exactly it is happening, but the issue is that one of the dummy_method fields is being duplicated and allowed to escape from the class definition.

(This is similar to 0007293 but different as this bug is still present on trunk)
TagsNo tags attached.
Attached Files

- Relationships
related to 0007381resolvedgarrigue Assertion failure with refutation pattern 

-  Notes
(0016174)
garrigue (manager)
2016-08-03 02:14

This one is a but different.
The dummy method does not escape, it is only believed to escape: i.e. the logic in update_level used to check that the type of self does not escape is wrongly activated.
Would probably need to find a different way to check that.
Bu this is not high priority as the number of features required to cause this (completeness) problem is large (GADTs + binary methods).
(0016178)
lpw25 (developer)
2016-08-03 09:45

> The dummy method does not escape, it is only believed to escape: i.e. the logic in update_level used to check that the type of self does not escape is wrongly activated.

I'm slightly confused by this. When the module inclusion check is done -- so after the escape logic has been run -- the internal `free` type still contains a dummy method, and that is what causes the inclusion check to fail. Am I misunderstanding something, or did it behave differently when you ran it?

> Bu this is not high priority as the number of features required to cause this (completeness) problem is large (GADTs + binary methods).

The reason I came across this bug is that I am trying to evaluate turning on GADT-style matching for all matches that contain a variant constructor, rather than just those matches that obviously contain a GADT. This would allow disambiguation of GADTs in pattern matching (of course it may have too much of a compile-time performance cost, but that is what I was trying to evaluate). In that context, this bug becomes a bit of a show stopper as it basically happens for any binary method.
(0016179)
garrigue (manager)
2016-08-03 11:24

OK, merging GADT matching with normal case is indeed a goal.
But I think that a first step would be to get rid of all the hackery in type_cases.
This mechanism of synchronization between ids and levels is weird.
Same thing for the dummy method: the current approach is too brittle.
Have to understand better how it works.
(0016432)
garrigue (manager)
2016-10-20 04:27

Fixed in 4.04 by commit 911b874.

In subst.ml, do not copy the type of self when it is not generalized.

- Issue History
Date Modified Username Field Change
2016-07-20 19:13 lpw25 New Issue
2016-07-20 19:13 lpw25 Description Updated View Revisions
2016-08-03 02:14 garrigue Note Added: 0016174
2016-08-03 02:14 garrigue Assigned To => garrigue
2016-08-03 02:14 garrigue Status new => confirmed
2016-08-03 09:45 lpw25 Note Added: 0016178
2016-08-03 11:24 garrigue Note Added: 0016179
2016-09-07 16:57 shinwell Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2016-10-19 17:42 garrigue Relationship added related to 0007381
2016-10-20 04:27 garrigue Note Added: 0016432
2016-10-20 04:27 garrigue Status confirmed => resolved
2016-10-20 04:27 garrigue Fixed in Version => 4.04.0 +dev / +beta1 / +beta2
2016-10-20 04:27 garrigue Resolution open => fixed
2017-02-23 16:45 doligez Category OCaml typing => typing


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker