New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Assertion failure in type checker #5848
Comments
Comment author: @alainfrisch Note: this seems to be related to the record_disambiguation branch. |
Comment author: @lpw25 The problem is that the contains_gadt function in typecore.ml is not correct in the presence of record disambiguation. |
Comment author: @garrigue Indeed, we need to know in advance whether a constructor is GADT or not in patterns (mostly for performance reasons). In theory it is possible to remove all the calls to contains_gadt, but I'm afraid of the performance cost / possible bugs. |
Comment author: @garrigue 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). |
Comment author: @lpw25 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? |
Comment author: @garrigue 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. |
Comment author: @garrigue Improved fix in revision 13119, as indicated above. |
Comment author: @alainfrisch 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? |
Comment author: @garrigue This is why it is not closed, just resolved :-) 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. |
Comment author: @alainfrisch
I rather see it as an opportunity to find bugs introduced by GADTs earlier! |
Original bug ID: 5848
Reporter: waern
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:46Z)
Resolution: fixed
Priority: normal
Severity: major
Fixed in version: 4.01.0+dev
Category: typing
Child of: #5759 #5998
Bug description
Example:
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)
The text was updated successfully, but these errors were encountered: