|Anonymous | Login | Signup for a new account||2017-09-23 02:18 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0005848||OCaml||typing||public||2012-12-06 12:13||2015-12-11 19:18|
|Target Version||Fixed in Version||4.01.0+dev|
|Summary||0005848: Assertion failure in type checker|
module B : sig
type (_, _) t = Eq: ('a, 'a) t
val f: 'a -> 'b -> ('a, 'b) t
type (_, _) t = Eq: ('a, 'a) t
let f t1 t2 = Obj.magic Eq
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)
|Tags||No tags attached.|
|Note: this seems to be related to the record_disambiguation branch.|
|The problem is that the contains_gadt function in typecore.ml is not correct in the presence of record disambiguation.|
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.
|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).|
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?
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.
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.
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?
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.
> 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!
|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|
|2015-12-11 19:18||xleroy||Status||resolved => closed|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|Copyright © 2000 - 2011 MantisBT Group|