0005948: GADT with polymorphic variants bug

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005948

OCaml

OCaml typing

public

2013-03-12 18:53

2013-04-23 02:10

Reporter

lpw25

Assigned To

garrigue

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

OS Version

Product Version

4.00.1

Target Version

Fixed in Version

4.00.2+dev

Summary

0005948: GADT with polymorphic variants bug

Description

I came across a typing bug while playing around with GADTs and polymorphic variants. The following code produces a segmentation fault:

  type tag = [`TagA | `TagB | `TagC]

  type 'a poly =
      AandBTags : [< `TagA of int | `TagB ] poly
    | ATag : [< `TagA of int] poly
  constraint 'a = [< `TagA of int | `TagB]

  let intA = function `TagA i -> i
  let intB = function `TagB -> 4

  let intAorB = function
      `TagA i -> i
    | `TagB -> 4

  type _ wrapPoly =
    WrapPoly : 'a poly -> ([< `TagA of int | `TagB] as 'a) wrapPoly

  let example6 : type a. a wrapPoly -> (a -> int) =
    fun w ->
      match w with
      | WrapPoly ATag -> intA
      | WrapPoly _ -> intA (* This should not be allowed *)

  let _ = example6 (WrapPoly AandBTags) `TagB (* This causes a seg fault *)

Tags

No tags attached.

Attached Files

Relationships

child of

0005998

assigned

garrigue

GADT typing and exhaustiveness bugs

Notes
(0008964) garrigue (manager) 2013-03-13 06:07	Fixed in trunk and 4.00, revisions 13396 and 13397. Note: you cannot refine variant types whose row variable is rigid.

Issue History
Date Modified	Username	Field	Change
2013-03-12 18:53	lpw25	New Issue
2013-03-13 06:07	garrigue	Note Added: 0008964
2013-03-13 06:07	garrigue	Status	new => resolved
2013-03-13 06:07	garrigue	Fixed in Version	=> 4.00.2+dev
2013-03-13 06:07	garrigue	Resolution	open => fixed
2013-03-13 06:07	garrigue	Assigned To	=> garrigue
2013-04-23 02:10	garrigue	Relationship added	child of 0005998