Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007214OCamltypingpublic2016-04-06 02:052017-09-24 17:32
Reporterstedolan 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target Version4.03.0+dev / +beta1Fixed in Version4.03.0+dev / +beta1 
Summary0007214: Assertion failure in Env.add_gadt_instances
DescriptionThe following program causes an assertion in Env.add_gadt_instance to fail:

type _ t = I : int t

let f (type a) (x : a t) =
  let module M = struct
    let (I : a t) = x
    let x = (I : a t)
  end in
  ()

Tested on recent trunk and 4.03+beta1.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0015690)
garrigue (manager)
2016-04-08 09:22

Fixed in 4.03 and trunk, commits 24cb12f and 8667b66.

Do not allow refining local abstract types in toplevel lets, as they have a different scope.

Note that we should still think about whether we should allow this eventually, and how.
(0015691)
stedolan (developer)
2016-04-08 10:11

Great!

If you do allow this eventually, you'll have to be very careful to avoid the same sort of issues as 0007215 arising via "module rec" instead of "let rec".

Here's an erroneous program which used to trigger the assert, and is now correctly rejected. Any patch that allows toplevel refinement will have to ensure this program is still rejected:


type (_,_) eq = Refl : ('a, 'a) eq

let bad (type a) =
  let module N = struct
    module rec M : sig
      val e : (int, a) eq
    end = struct
      let (Refl : (int, a) eq) = M.e
      let e : (int, a) eq = Refl
    end
  end in N.M.e

I do not think that the current check for "recursive module cannot be safely evaluated" will catch this case, for the same reasons as 0007215.
(0015692)
garrigue (manager)
2016-04-08 10:18

Thanks. I added this to the test suite, which is the best way to be safe for the future.

- Issue History
Date Modified Username Field Change
2016-04-06 02:05 stedolan New Issue
2016-04-06 13:21 doligez Status new => confirmed
2016-04-06 13:21 doligez Target Version => 4.03.0+dev / +beta1
2016-04-08 09:22 garrigue Note Added: 0015690
2016-04-08 09:22 garrigue Status confirmed => resolved
2016-04-08 09:22 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-04-08 09:22 garrigue Resolution open => fixed
2016-04-08 09:22 garrigue Assigned To => garrigue
2016-04-08 10:11 stedolan Note Added: 0015691
2016-04-08 10:18 garrigue Note Added: 0015692
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:32 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker