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.