Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006716OCamltypingpublic2014-12-15 11:512016-09-26 15:13
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0+dev / +beta1 
Target VersionFixed in Version4.03.0+dev / +beta1 
Summary0006716: Assertion failure with existentials + inline records + rows
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
TagsNo tags attached.
Attached Files

- Relationships
related to 0006163closedgarrigue Fatal error: exception Assert_failure("typing/ctype.ml", 1891, 19) 
related to 0007372resolvedfrisch Bug in type-checker with GADTs and inline records 

-  Notes
(0012821)
lpw25 (developer)
2014-12-15 12:04

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

I thought we had dropped support for inline records on GADTs. Is that not the case?
(0012824)
frisch (developer)
2014-12-15 13:09

Probably related to 0006163.
(0012825)
frisch (developer)
2014-12-15 13:10

> 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.
(0012826)
frisch (developer)
2014-12-15 15:05
edited on: 2014-12-15 18:30

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?).

(0012828)
garrigue (manager)
2014-12-16 02:40

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.

- Issue History
Date Modified Username Field Change
2014-12-15 11:51 yallop New Issue
2014-12-15 12:04 lpw25 Note Added: 0012821
2014-12-15 13:09 frisch Note Added: 0012824
2014-12-15 13:09 frisch Relationship added related to 0006163
2014-12-15 13:10 frisch Note Added: 0012825
2014-12-15 15:05 frisch Note Added: 0012826
2014-12-15 18:30 frisch Note Edited: 0012826 View Revisions
2014-12-16 02:40 garrigue Note Added: 0012828
2014-12-16 02:40 garrigue Status new => resolved
2014-12-16 02:40 garrigue Fixed in Version => 4.03.0+dev / +beta1
2014-12-16 02:40 garrigue Resolution open => fixed
2014-12-16 02:40 garrigue Assigned To => garrigue
2016-09-26 15:13 frisch Relationship added related to 0007372
2017-02-23 16:45 doligez Category OCaml typing => typing


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker