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

Allow GADT constructors to introduce equations and existential types under or-patterns #2110

Merged
merged 3 commits into from Nov 12, 2018

Conversation

@trefis
Copy link
Contributor

commented Oct 18, 2018

(This PR is the last part to be extracted from #1675.)

It adds limited support for GADTs under or-patterns (and nothing else): equations and existential types can be introduced in an or-pattern branch, but they are not accessible outside of that branch.

The implementation is straightforward, and it should be easier to reason about soundness than with the previous PR (which included many orthogonal changes).

Note: once again the calls to check_scope_escape are here only to get better error messages. They could be removed and you'd still get an error on escapes (thanks to the call to unify_var that was inserted in enter_orpat_variables, which pulls things out of the or-pattern scope), but the message would be worse.

@garrigue would you mind giving it a new look?

@trefis trefis force-pushed the trefis:gadt-under-or-pattern branch from e6d888e to 8125ef5 Nov 5, 2018

@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Nov 5, 2018

@garrigue: ping :)

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Nov 5, 2018

Not forgetting. I try to look at that this week.

@garrigue
Copy link
Contributor

left a comment

Sorry for the long delay.
The actual code is very short, and since levels are only used here to ensure that no existential or ambiguous type escapes, this looks fine to me. There should be no interaction with levels coming from outside the pattern-matching, which are either lower (and as a result untouchable), or generic lowered to the current level to be re-generalized later.

I have added some comments in the test file. I think it would be useful to document what looks strange there, as things to potentially straighten up in the future. I don't believe anything is directly related with this patch, but you have exerted some dark corners, like the way expand_head just expands everything, sometimes creating spurious ambivalence. This was known, but I'm not sure I had explicit examples for that.

but a pattern was expected which matches values of type a t
Type bool is not compatible with type a = int
|}]

This comment has been minimized.

Copy link
@garrigue

garrigue Nov 12, 2018

Contributor

Actually the above could be just an unused case warning: the BoolLit branch cannot be reached.
But since this is wrong code anyway, failing is still fine for now.

This comment has been minimized.

Copy link
@trefis

trefis Nov 12, 2018

Author Contributor

Well, if we expand the or-pattern like so:

let f (type a) (tt : a t * a t) =
  match tt with
  | IntLit, IntLit -> ()
  | IntLit, BoolLit -> ()
  | _ -> ()

one still gets an error.
So at least, the behavior is consistent, and I think that should remain true whether we want an error or a warning. (Though I think we do want an error)

Error: The variable x on the left-hand side of this or-pattern has type
a but on the right-hand side it has type bool
|}]

This comment has been minimized.

Copy link
@garrigue

garrigue Nov 12, 2018

Contributor

This failure is a bit mysterious: not only does it work without that as x, but it also works with no literal and (x : a).

let f (type a) (x : a t * a) = match x with                            
  (IntLit, (y : a)) | (BoolLit, (y : a)) -> y

I don't think this is a consequence of this patch, but eager expansion sometimes gives incoherent results.

This comment has been minimized.

Copy link
@trefis

trefis Nov 12, 2018

Author Contributor

I agree that this is not a consequence of this patch, however, I'm not sure this is related to expansion, but rather to the implementation of build_as_type.
In the first branch, build_as_type sees that the input pattern p is a constant, so it returns p.pat_type which is the type we assign to x.
In the second branch build_as_pat is given a Tpat_construct, and it just retypes that (ignoring the pat_extra field), which results in it returning bool, which we assign to x in the second branch.
Finally (and this is why I think expansion really doesn't come in to play here) we try to unify the type of both x in the outer environment, where no equation is available. Which explains the failure.

This comment has been minimized.

Copy link
@garrigue

garrigue Nov 12, 2018

Contributor

Right. This goes back to what should be the semantics of build_as_type when there is a type annotation.

This comment has been minimized.

Copy link
@trefis

trefis Nov 12, 2018

Author Contributor

Yes. I haven't had time to think about it since the last time I mentioned the issue. But hopefully we can find some time to do something about it for 4.09.

@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Nov 12, 2018

Thank you for the review @garrigue!

@trefis trefis merged commit e233882 into ocaml:trunk Nov 12, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

@trefis trefis deleted the trefis:gadt-under-or-pattern branch Nov 12, 2018

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