Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005848OCamlOCaml typingpublic2012-12-06 12:132013-04-26 00:34
Reporterwaern 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.01.0+dev 
Summary0005848: Assertion failure in type checker
DescriptionExample:

module B : sig
  type (_, _) t = Eq: ('a, 'a) t
  val f: 'a -> 'b -> ('a, 'b) t
end
 =
struct
  type (_, _) t = Eq: ('a, 'a) t
  let f t1 t2 = Obj.magic Eq
end

let of_type: type a. a -> a = fun x ->
  match B.f x 4 with
  | Eq -> 5

This produces the following error message when I try to compile:

File "test.mf", line 13, characters 4-6:
Warning 40: Eq is used out of scope.
Fatal error: exception Assert_failure("typing/env.ml", 811, 59)
TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 
child of 0005759resolvedgarrigue Using well-disciplined type-propagation to disambiguate label and constructor names 

-  Notes
(0008577)
frisch (developer)
2012-12-06 12:29

 Note: this seems to be related to the record_disambiguation branch.
(0008578)
lpw25 (developer)
2012-12-06 14:13

 The problem is that the contains_gadt function in typecore.ml is not correct in the presence of record disambiguation.
(0008585)
garrigue (manager)
2012-12-07 03:34

 Indeed, we need to know in advance whether a constructor is GADT or not in patterns (mostly for performance reasons).
As a simple fix, I just disabled any disambiguation for GADT constructor lookup in patterns.
(If the inferred constructor is not the default one, you get an explicit error).

In theory it is possible to remove all the calls to contains_gadt, but I'm afraid of the performance cost / possible bugs.
GADTs are a language extension, so it is not shocking that they are not supported as well as the core language.
(0008586)
garrigue (manager)
2012-12-07 04:31

 Actually, it would be easy to do better than that: still allow type-based disambiguation, but only for indentifiers in scope. contains_gadt would lose in precision (become true as soon as one of the candidate constructors is a GADT), but this should not be a problem. The only question is wether it is worth the extra code (in particular we need a different behavior for expressions and patterns).
(0008587)
lpw25 (developer)
2012-12-07 12:43

 For those of us who only intend to use identifiers in scope (i.e. turn warning 40 into an error) I think that having disambiguation work the same for GADTs as other constructors would be appreciated.

What do you mean by different behaviour for expressions and patterns?
(0008588)
garrigue (manager)
2012-12-07 15:28

 It's just that the problem does not exist for expressions: there is no need to know in advance whether this is a GADT constructor or not. So disambiguation should work normally there.

Concerning patterns, I actually started implementing that scheme, and then decided to think a bit more about it. It is not too complicated, but as mentioned above this means that contains_gadt is no longer exact. So you might have an extra cost whereas your constructor is not GADT (but you have a GADT constructor with the same name in scope). However, this is probably fine. Then part of the cost (like copying some types in the environment) could probably be avoided by defining another contains_gadt, that works on the typed tree. However, this means bigger changes, and I'm not sure it's worth it, if this is only a question of (probably small) cost.
(0008591)
garrigue (manager)
2012-12-08 03:43

 Improved fix in revision 13119, as indicated above.
Disambiguation is enable for GADTs in patterns, only scope is restricted.
Didn't try to refine the cases where environment duplication is needed.
(0008593)
frisch (developer)
2012-12-10 13:17
edited on: 2012-12-10 13:18

 Should we really mark this as resolved? The current situation seems a bit unsatisfactory (and at least, it should be documented).

What would be the impact on performance of doing the safe thing always? If the slowdown is too big, would it be an option to try first in non-GADT mode, fail if a GADT is encountered, and then try again in GADT mode?
(0008595)
garrigue (manager)
2012-12-11 08:24

 This is why it is not closed, just resolved :-)
At least we now have a reasonable behavior.

My concern with handling everything as GADT is not only the slowdown but also the risk of introducing bugs. Currently if you don't use GADTs at all, you still mostly get the original behavior.
You may be right that backtracking is another solution.
But note that we have to be careful there: backtracking can undo a unification, but it does not handle all the state, so we need to check the typing of patterns in detail.
(0008596)
frisch (developer)
2012-12-11 11:15

 > My concern with handling everything as GADT is not only the slowdown but also the risk of introducing bugs.

I rather see it as an opportunity to find bugs introduced by GADTs earlier!

- Issue History
Date Modified Username Field Change
2012-12-06 12:13 waern New Issue
2012-12-06 12:29 frisch Note Added: 0008577
2012-12-06 14:13 lpw25 Note Added: 0008578
2012-12-07 03:34 garrigue Note Added: 0008585
2012-12-07 03:34 garrigue Status new => resolved
2012-12-07 03:34 garrigue Fixed in Version => 4.01.0+dev
2012-12-07 03:34 garrigue Resolution open => fixed
2012-12-07 03:34 garrigue Assigned To => garrigue
2012-12-07 04:31 garrigue Note Added: 0008586
2012-12-07 12:43 lpw25 Note Added: 0008587
2012-12-07 15:28 garrigue Note Added: 0008588
2012-12-08 03:43 garrigue Note Added: 0008591
2012-12-10 13:17 frisch Note Added: 0008593
2012-12-10 13:18 frisch Note Edited: 0008593 View Revisions
2012-12-11 08:24 garrigue Note Added: 0008595
2012-12-11 11:15 frisch Note Added: 0008596
2013-04-26 00:34 garrigue Relationship added child of 0005998
2013-04-26 00:34 garrigue Relationship added child of 0005759

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker