Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007747OCamltypingpublic2018-02-28 08:372018-03-01 08:10
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.07.0+dev 
Summary0007747: Type checker can loop infinitly and consumes all computer memory
DescriptionI allready mentioned the problem in the discussion about MPR 0007739 issue, but I think it deserves its own independant report.

Normally cycles in types defintion are disallowed by the type checker, as in this example:

module rec M : sig type t = N.t end = struct type t end
and N : sig type t = M.t end = struct type t = M.t end;;
Error: The definition of M.t contains a cycle:

But with GADT we can hide this cycle and reveal it only when inspecting an equality witness value. In some cases this can put the type checker in an infinite loop and memory consumption increases drastically (around 1 GB per 10 seconds on my computer).

The reproduction case (below) is pretty pathological and a corner case, but I don't know if such situation can appear in a more realistic code wich combines GADT and private types.
Steps To Reproducetype (_,_) eq = Refl : ('a,'a) eq

module M = struct type t end
module N : sig type t = private M.t val eq : (t, M.t) eq end =
  struct type t = M.t let eq = Refl end

  as long as we are casting between M.t and N.t
  there is no problem, this will type check.

let f x = match N.eq with Refl -> (x : N.t :> M.t)

let f x = match N.eq with Refl -> (x : M.t :> N.t)

  but as soon we're trying to cast to another type,
  the type checker will never return and memory
  consumption will increase drastically.

let f x = match N.eq with Refl -> (x : N.t :> int)
TagsNo tags attached.
Attached Files

- Relationships
related to 0007739confirmedgarrigue Abstract type and private type don't have same behavioir with type equality 

-  Notes
garrigue (manager)
2018-03-01 07:33

We should certainly expand private abbreviations when checking for recursion.
Trivial fix at: [^]
garrigue (manager)
2018-03-01 08:10

Merged GPR#1641 as commit a84c11e.

- Issue History
Date Modified Username Field Change
2018-02-28 08:37 kantian New Issue
2018-03-01 07:33 garrigue Note Added: 0018933
2018-03-01 07:34 garrigue Relationship added related to 0007739
2018-03-01 08:10 garrigue Note Added: 0018934
2018-03-01 08:10 garrigue Status new => resolved
2018-03-01 08:10 garrigue Fixed in Version => 4.07.0+dev
2018-03-01 08:10 garrigue Resolution open => fixed
2018-03-01 08:10 garrigue Assigned To => garrigue

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker