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

Segfault from conjunctive constraints #7269

Closed
vicuna opened this issue May 31, 2016 · 4 comments · Fixed by #9547
Closed

Segfault from conjunctive constraints #7269

vicuna opened this issue May 31, 2016 · 4 comments · Fixed by #9547
Assignees
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented May 31, 2016

Original bug ID: 7269
Reporter: @stedolan
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:56Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 4.03.0
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: @gasche @yallop @hcarty

Bug description

The following program segfaults in 4.03.0 (but not previous versions):

type s = [`A | `B] and sub = [`B]
type +'a t = T : [< `Conj of 'a & sub | `Other of string] -> 'a t
let f (T (`Other msg) : s t) = print_string msg
let _ = f (T (`Conj `B) :> s t)

The issue is that (Conj of [A|B] & [B]) is judged impossible, since [A|B] and [B] do not unify, and therefore the pattern matching that f does is considered exhaustive. However, I can in fact construct a (Conj of [A|B] & [B]), because covariance yields one from a Conj [`B].

I am unsure exactly what & represents. On one hand, it seems like an intersection or subtyping meet (which should be covariant in both arguments), and on the other it seems like a delayed unification (which should not).

The example uses GADTs, but I don't think they're essential. GADTs are the easiest way to keep a row variable around (the row is existentially quantified), which is necessary to exhibit the bug. I suspect it would also come up with modules and private row types.

@vicuna
Copy link
Author

vicuna commented Jun 2, 2016

Comment author: @garrigue

Fixed in trunk by commit c7ea9e8.

Indeed, this is a delayed unification, so it should be handled the same way as GADT parameters.
Changed the computation of variance so that variables appearing in conjunctive constraints be considered as invariant (i.e. only if there is a &).

Note that this is related to GADTs, because otherwise there is no way to export a conjunctive constraint without exporting the enclosing row variable, and such subtyping is not allowed under a row variable.

@vicuna
Copy link
Author

vicuna commented Jun 2, 2016

Comment author: @stedolan

Nice, this fixes the subtyping issue. Now that you point it out, I see that conjunctive constraints are very much like GADT parameters.

However, the exhaustivity checker is still too eager to reject conjunctive constraints as unsatisfiable. This program doesn't use subtyping, but still segfaults (on 4.03):

module M : sig
  type s
  type t = T : [< `Conj of int & s | `Other of string] -> t
  val x : t
end = struct
  type s = int
  type t = T : [< `Conj of int | `Other of string] -> t
  let x = T (`Conj 42)
end

let _ = M.(match x with T (`Other msg) -> print_string msg)

For this example, GADTs aren't strictly necessary. Here's the same program, with the existential row encoded using a polymorphic record field instead:

module M : sig
  type s
  type elim = { ex : 'a . ([<`Conj of int & s | `Other of string] as 'a) -> unit }
  val e : elim -> unit
end = struct
  type s = int
  type elim = { ex : 'a . (([<`Conj of int | `Other of string] as 'a) -> unit) }
  let e { ex } = ex (`Conj 42 : [`Conj of int])
end

let _ = M.(e { ex = fun (`Other msg) -> print_string msg })

@vicuna
Copy link
Author

vicuna commented Jun 2, 2016

Comment author: @garrigue

You're right.
Subtyping is only one way to trigger it.
The true problem is the possibility to trigger a seemingly impossible unification during pattern-matching. The system assumes that it can only happen is a GADT parameter, but this is another way.

@vicuna
Copy link
Author

vicuna commented Jun 3, 2016

Comment author: @garrigue

Really? fixed in trunk by commit 240fde1.

While handling conjunctive types as GADT constraints could be interesting, this would require more work. So for now just make the redundancy check less complete, by having it ignore conflicts in conjunctive types. Hacky but reasonable.

Technical note: the common part between gadts and universal record fields is that they use so-called "fixed variant types", which have the property of forcing conjunctive fields appearing in types they are unified to.

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

Successfully merging a pull request may close this issue.

3 participants