Skip to content
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

Closed
vicuna opened this issue Dec 6, 2012 · 10 comments
Closed

Assertion failure in type checker #5848

vicuna opened this issue Dec 6, 2012 · 10 comments
Assignees
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Dec 6, 2012

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)

@vicuna
Copy link
Author

vicuna commented Dec 6, 2012

Comment author: @alainfrisch

Note: this seems to be related to the record_disambiguation branch.

@vicuna
Copy link
Author

vicuna commented Dec 6, 2012

Comment author: @lpw25

The problem is that the contains_gadt function in typecore.ml is not correct in the presence of record disambiguation.

@vicuna
Copy link
Author

vicuna commented Dec 7, 2012

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Dec 7, 2012

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).

@vicuna
Copy link
Author

vicuna commented Dec 7, 2012

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?

@vicuna
Copy link
Author

vicuna commented Dec 7, 2012

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.

@vicuna
Copy link
Author

vicuna commented Dec 8, 2012

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Dec 10, 2012

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?

@vicuna
Copy link
Author

vicuna commented Dec 11, 2012

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Dec 11, 2012

Comment author: @alainfrisch

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants