Bug in type-checker with GADTs and inline records

[vicuna]

Original bug ID: 7372
Reporter: @alainfrisch
Assigned to: @alainfrisch
Status: resolved (set by @alainfrisch on 2017-03-24T14:37:24Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Tags: github
Related to: #6716
Monitored by: @gasche @yallop

Bug description

bug1.mli:
  type _ t =  C: { f: ('a -> [<`X]) t } -> [<`X] t

bug2.ml:
  open Bug1
  let f (C {f}) = ()

ocamlc -c bug1.mlo bug2.ml

gives:

File "bug2.ml", line 3, characters 9-12:
Error: This pattern matches values of type ([< `X ] as 'a, 'b) Bug1.t.C
       but a pattern was expected which matches values of type
         ($C_'a, [< `X ]) Bug1.t.C
       Type [< `X ] as 'a is not compatible with type $C_'a

The problem probably comes from the internal encoding of inline records as regular records (whose parameters are derived from free variables of the inline record).

Note: explicitly qualifying Bug1.C in bug2.ml removes the error message; so does inlining the type definition in bug2.ml.

[vicuna]

Comment author: @alainfrisch

Tentative fix proposed in #824

[vicuna]

Comment author: @alainfrisch

Another fix in #828

[vicuna]

Comment author: @alainfrisch

I'm setting Target Version = 4.04, but I don't think this is necessarily a blocking issue.

[vicuna]

Comment author: @alainfrisch

#834