Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006817OCamltypingpublic2015-03-23 15:502016-12-07 11:47
Reporterchambart 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0+dev / +beta1 
Target VersionFixed in Version4.02.2+dev / +rc1 
Summary0006817: GADT exhaustiveness breakage with modules
DescriptionThis code is correctly checked for exhaustiveness if defined like this. But
if nil is declared in another module, it breaks

  type nil

  type _ s =
    | Nil : nil s
    | Cons : 't s -> ('h -> 't) s

  type ('stack, 'typ) var =
    | Head : (('typ -> _) s, 'typ) var
    | Tail : ('tail s, 'typ) var -> ((_ -> 'tail) s, 'typ) var

  type _ lst =
    | CNil : nil lst
    | CCons : 'h * ('t lst) -> ('h -> 't) lst

  let rec get_var : type stk ret. (stk s, ret) var -> stk lst -> ret = fun n s ->
    match n, s with
    | Head, CCons (h, _) -> h
    | Tail n', CCons (_, t) -> get_var n' t

For instance if we replace `type nil` with

  module A = struct
    type nil
  end
  open A

Or even

  module A = struct
    type nil = Cstr
  end
  open A

Notice that `type nil = unit` works.
TagsNo tags attached.
Attached Filespatch file icon fix-6817.patch [^] (520 bytes) 2015-03-24 22:22 [Show Content]

- Relationships

-  Notes
(0013526)
lpw25 (developer)
2015-03-23 16:18
edited on: 2015-03-23 16:19

The first case is the correct behaviour, because an abstract type from another module could be equal to a function type. The second case could probably be improved, since a type with a `Cstr` constructor could not be equal to a function type.

(0013536)
lpw25 (developer)
2015-03-24 22:22

The attached patch fixes the second case. It seems sound to me, since a structural type cannot be equal to a datatype.
(0013543)
garrigue (manager)
2015-03-25 02:52

Fixed as suggested in trunk and 4.02, at revisions 15959 and 15960.
(0013559)
chambart (developer)
2015-03-26 11:24

Thanks you !

- Issue History
Date Modified Username Field Change
2015-03-23 15:50 chambart New Issue
2015-03-23 16:18 lpw25 Note Added: 0013526
2015-03-23 16:19 lpw25 Note Edited: 0013526 View Revisions
2015-03-24 22:22 lpw25 File Added: fix-6817.patch
2015-03-24 22:22 lpw25 Note Added: 0013536
2015-03-25 02:52 garrigue Note Added: 0013543
2015-03-25 02:52 garrigue Status new => resolved
2015-03-25 02:52 garrigue Fixed in Version => 4.02.2+dev / +rc1
2015-03-25 02:52 garrigue Resolution open => fixed
2015-03-25 02:52 garrigue Assigned To => garrigue
2015-03-26 11:24 chambart Note Added: 0013559
2016-12-07 11:47 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker