Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006275OCamlOCaml typingpublic2013-12-16 23:282013-12-18 02:48
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version4.01.1+dev 
Summary0006275: Soundness bug related to type constraints
DescriptionSoundness bug related to type constraints reported by art-w on reddit:

            OCaml version 4.02.0+dev2-2013-09-12
     
    # type 'x t = A of 'a constraint 'x = [< `X of 'a ] ;;
    type 'b t = A of 'a constraint 'b = [< `X of 'a ]
    # let magic (x : 'a) =
        let A x = A x in
          x;;
        val magic : 'a -> 'b = <fun>
    # (magic 0: string);;
     
    Process ocaml-toplevel segmentation fault

TagsNo tags attached.
Attached Files

- Relationships
related to 0005985confirmedgarrigue Unexpected interaction between variance and GADTs 

-  Notes
(0010731)
lpw25 (developer)
2013-12-16 23:44

This appears to be related to the injectivity bug. A type which unifies with:

    [< `X of 'a | `Y]

may not be injective in 'a since it might be [`Y]. I think something similar is happening in this bug.
(0010732)
lpw25 (developer)
2013-12-16 23:53

Same bug using GADTs instead of constraints:

            OCaml version 4.02.0+dev2-2013-09-12
     
    # type 'a t = A : 'a -> [< `X of 'a ] t;;
    type 'a t = A : 'a -> [< `X of 'a ] t
    # let magic (x : 'a) =
            let A x = A x in
              x;;
        val magic : 'a -> 'b = <fun>
    # (magic 0: string);;
     
    Process ocaml-toplevel segmentation fault
(0010733)
garrigue (manager)
2013-12-17 02:46

Fixed in trunk and 4.01, at revisions 14363 and 14364.

It is indeed very similar to PR#5985 as the problem is non-injectivity,
and this is related to the need of having both upper and lower bounds
for variance.
You could say it's worse, as you don't even need abstraction to trigger it.
(0010738)
doligez (administrator)
2013-12-17 12:49

Reopened because on 4.01 the fix breaks the regression test for 0005985.
(0010739)
lpw25 (developer)
2013-12-17 15:03

It looks like revision 14364 doesn't actually include the fix, only the tests for the bug.
(0010744)
garrigue (manager)
2013-12-18 02:48

Indeed, I committed in testsuite for 4.01...
Now really fixed at 14373.

- Issue History
Date Modified Username Field Change
2013-12-16 23:28 lpw25 New Issue
2013-12-16 23:44 lpw25 Note Added: 0010731
2013-12-16 23:53 lpw25 Note Added: 0010732
2013-12-17 02:43 garrigue Relationship added related to 0005984
2013-12-17 02:46 garrigue Note Added: 0010733
2013-12-17 02:46 garrigue Status new => resolved
2013-12-17 02:46 garrigue Fixed in Version => 4.01.1+dev
2013-12-17 02:46 garrigue Resolution open => fixed
2013-12-17 02:46 garrigue Assigned To => garrigue
2013-12-17 02:47 garrigue Relationship deleted related to 0005984
2013-12-17 02:47 garrigue Relationship added related to 0005985
2013-12-17 12:49 doligez Note Added: 0010738
2013-12-17 12:49 doligez Status resolved => confirmed
2013-12-17 12:49 doligez Resolution fixed => reopened
2013-12-17 15:03 lpw25 Note Added: 0010739
2013-12-18 02:48 garrigue Note Added: 0010744
2013-12-18 02:48 garrigue Status confirmed => resolved
2013-12-18 02:48 garrigue Resolution reopened => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker