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
Comments
Comment author: @lpw25
I thought we had dropped support for inline records on GADTs. Is that not the case? |
Comment author: @alainfrisch Probably related to #6163. |
Comment author: @alainfrisch
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. |
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?). |
Comment author: @garrigue Fixed in trunk at revision 15675. Thanks Alain for your good analysis. |
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} -> tlet f (T { x = C }) = ()
$ ocamlc bug.ml
Fatal error: exception File "typing/ctype.ml", line 1990, characters 19-25: Assertion failed
The text was updated successfully, but these errors were encountered: