Original bug ID: 5689
Reporter: @lpw25
Assigned to: @garrigue
Status: closed (set by @garrigue on 2012-07-18T03:37:39Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.01.0+dev
Fixed in version: 4.00.0+dev
Category: typing
Child of: #5998
Monitored by: @lpw25 @hcarty

Bug description

As I understand it the types:

type inkind = [ Link | Nonlink ]

type _ inline_t =
| Text: string -> [< inkind > Nonlink ] inline_t | Bold: 'a inline_t list -> 'a inline_t | Link: string -> [< inkind > Link ] inline_t
| Mref: string * [ Nonlink ] inline_t list -> [< inkind > Link ] inline_t

should maintain the invariant that a Mref cannot contain another Mref or a Link, because these have type [< inkind > Link] and the Mref only accepts [ Nonlink ].

However the attached file uses GADTs to break this invariant producing a value:

val broken_invariant : inkind inline_t = Mref ("foo", [Link ])

File attachments

• broken.ml