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

Assertion failure with existentials + inline records + rows #6716

Closed
vicuna opened this issue Dec 15, 2014 · 5 comments
Closed

Assertion failure with existentials + inline records + rows #6716

vicuna opened this issue Dec 15, 2014 · 5 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Dec 15, 2014

Original bug ID: 6716
Reporter: @yallop
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2014-12-16T01:40:33Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Related to: #6163 #7372
Monitored by: @gasche @hcarty

Bug description

$ cat bug.ml
type _ c = C : [A] c type t = T : {x:[<A] c} -> t
let f (T { x = C }) = ()
$ ocamlc bug.ml
Fatal error: exception File "typing/ctype.ml", line 1990, characters 19-25: Assertion failed

@vicuna
Copy link
Author

vicuna commented Dec 15, 2014

Comment author: @lpw25

type t = T : {x:[<`A] c} -> t

I thought we had dropped support for inline records on GADTs. Is that not the case?

@vicuna
Copy link
Author

vicuna commented Dec 15, 2014

Comment author: @alainfrisch

Probably related to #6163.

@vicuna
Copy link
Author

vicuna commented Dec 15, 2014

Comment author: @alainfrisch

Is that not the case?

Since it was decided not to expose the inline record type itself, it was decided to keep the ability to have GADT constructors with an inline record argument.

@vicuna
Copy link
Author

vicuna commented Dec 15, 2014

Comment author: @alainfrisch

Actually, the problems seems to be the definition of "free variables" in the constructor, used to define the type parameters for the inline record type. The current definition will define the row variable as the variable, while it should probably be the Tvariant itself. Concretely, the current code generates internally inline record declarations whose parameters are "row" variables, while they should be constrained types. Fixing this amounts to changing the definition of type_params in the Cstr_record case of the constructor_args function (in datarepr.ml). Instead of using free_vars defined above, one should collect a better notion of type variables. I tried with:

let free_params ty =
  let ret = ref TypeSet.empty in
  let rec loop ty =
    let ty = repr ty in
    if ty.level >= lowest_level then begin
      ty.level <- pivot_level - ty.level;
      match ty.desc with
      | Tvar _ ->
          ret := TypeSet.add ty !ret
      | Tvariant row ->
          let row = row_repr row in
          iter_row loop row;
          begin match (row_more row).desc with
          | Tvar _ -> ret := TypeSet.add ty !ret
          | _ -> ()
          end
      | _ ->
          iter_type_expr loop ty
    end
  in
  loop ty;
  unmark_type ty;
  !ret

but I'm not very confident... Here I could use some help from people who understand better than I how rows work (Jacques?).

@vicuna
Copy link
Author

vicuna commented Dec 16, 2014

Comment author: @garrigue

Fixed in trunk at revision 15675.

Thanks Alain for your good analysis.
You actually need both behaviors, because existentials must be variables (inluding row variables), while parameters must be types.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants