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 with refutation pattern #7381

Closed
vicuna opened this Issue Oct 6, 2016 · 9 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Oct 6, 2016

Original bug ID: 7381
Reporter: @yallop
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-10-08T11:12:56Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.0 +dev / +beta1 / +beta2
Target version: undecided
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Related to: #7298 #7391
Monitored by: @gasche

Bug description

In 4.04.0+beta2:

type (_, _) eql = Refl : ('a, 'a) eql
let f : type t. (int, t) eql * (t, string) eql -> unit = function _ -> .

Fatal error: exception File "typing/env.ml", line 1271, characters 59-65: Assertion failed

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 7, 2016

Comment author: @yallop

Here's a similar example without a refutation pattern that causes the same assertion failure:

type (,) eql = Refl : ('a, 'a) eql
let f : type t. ((int, t) eql * (t, string) eql) option -> unit =
function None -> ()

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 8, 2016

Comment author: @garrigue

Fixed in 4.04 by commit babad14.

The problem is that the new exhaustiveness check means that we may have to type GADT constructors even when they do not appear in the patterns themselves.
The fix is to prepare for this expect in cases where this is trivially not needed, i.e. if we just match on a variable and this is not a refutation case. But this means we still do it when matching on unit for instance...

@vicuna vicuna closed this Oct 8, 2016

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 19, 2016

Comment author: @nojb

We are experiencing some regression due to commit babad14. The affected code in question uses object types and type constrains extensively and we are now seeing "Self type cannot escape its class" errors. I am trying to produce a small example, but have not had any luck yet.

I am posting this just to get the word out.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 19, 2016

Comment author: @garrigue

This may be related to #7298, making it happen more often.
I shall look into that.
An example would be welcome, whatever its size.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

Comment author: @garrigue

#7298 has been fixed in the 4.04 branch. Could you check whether it solves your problem?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

Comment author: @nojb

Unfortunately, it does not. I will be looking at this today and will try to get back with more information/an example.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

Comment author: @nojb

Small repro:

class virtual child1 parent =
object
method private parent = parent
end

class virtual child2 =
object(_ : 'self)
constraint 'parent = < previous: 'self option; .. >
method private virtual parent: 'parent
end

let _ =
object(self)
method previous = None
method child =
object
inherit child1 self
inherit child2
end
end

Error: The method parent has type < child : 'a; previous : 'b option >
but is expected to have type < previous : < .. > option; .. >
Self type cannot escape its class

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

Comment author: @garrigue

I see.
You're using a nested immediate object referring to the outer self.
This is probably not well supported at this point (independently of commit babad14).
I'm not sure I will be able to fix it for 4.04.
Also, this is a new issue, so could you file a new bug report?

A workaround for this example is to move the inner object outside, so that its parameter is generalized:

let _ =
let child self =
object
inherit child1 self
inherit child2
end
in
object(self)
method previous = None
method child = child self
end

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

Comment author: @nojb

Thanks for the quick reply.

Filed a new bug report at #7391.

We actually have quite a bit of code using this style so in the meantime it might be simpler for us to revert the last couple of commits rather than rewrite it...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.