Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007269OCamltypingpublic2016-05-31 12:552017-09-24 17:32
Reporterstedolan 
Assigned Togarrigue 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0 
Target VersionFixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0007269: Segfault from conjunctive constraints
DescriptionThe 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.
TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0015958)
garrigue (manager)
2016-06-02 09:58

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.
(0015962)
stedolan (developer)
2016-06-02 11:53

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 })
(0015963)
garrigue (manager)
2016-06-02 13:06

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.
(0015968)
garrigue (manager)
2016-06-03 09:57

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.

- Issue History
Date Modified Username Field Change
2016-05-31 12:55 stedolan New Issue
2016-06-02 09:58 garrigue Note Added: 0015958
2016-06-02 09:58 garrigue Status new => resolved
2016-06-02 09:58 garrigue Fixed in Version => 4.04.0 +dev / +beta1 / +beta2
2016-06-02 09:58 garrigue Resolution open => fixed
2016-06-02 09:58 garrigue Assigned To => garrigue
2016-06-02 11:53 stedolan Note Added: 0015962
2016-06-02 13:06 garrigue Note Added: 0015963
2016-06-02 13:06 garrigue Status resolved => confirmed
2016-06-03 09:57 garrigue Note Added: 0015968
2016-06-03 09:57 garrigue Status confirmed => resolved
2016-06-03 09:58 garrigue Relationship added child of 0005998
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:32 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker