Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006223OCamltypingpublic2013-11-04 13:462015-12-11 19:24
Assigned Tolpw25 
StatusclosedResolutionno change required 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version 
Summary0006223: GADT patterns allow type mismatches in some type parameters
DescriptionIt seems that GADT patterns do not give unification errors for the parameters of types which may be non-injective. For example, in the following code, `t` is known to be injective and we get an error on the definition of `f`, but `N.s` is not known to be injective and we are allowed to use the `Bar` pattern with the wrong type.

  # type 'a t = T;;
  type 'a t = T
  # type 'a foo = Foo : int t foo;;
  type 'a foo = Foo : int t foo
  # let f (Foo: string t foo) = ();;
  Characters 7-10:
    let f (Foo: string t foo) = ();;
  Error: This pattern matches values of type int t foo
         but a pattern was expected which matches values of type string t foo
         Type int is not compatible with type string

  # module N : sig type 'a s end = struct type 'a s = S end;;
  module N : sig type 'a s end
  # type 'a bar = Bar : int N.s bar;;
  type 'a bar = Bar : int N.s bar
  # let g (Bar: string N.s bar) = ();;
  val g : string N.s bar -> unit = <fun>
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
lpw25 (developer)
2013-11-04 13:53

I'm actually not sure if this is a bug or not. It seems wrong to allow you to use a pattern with a different type than it was declared. On the other hand if I was to try to pattern match on a `string N.s bar` I need to include a case for `Bar` in case `string N.s` equals `int N.s`.

Either way I thought it was better to have a Mantis issue than to not have one.
lpw25 (developer)
2013-11-04 13:59

I have now convinced myself that this is in fact the correct behavior, so I will mark the issue resolved.
yallop (developer)
2013-11-04 14:11

This might be viewed as a design question rather than a bug. If N.s turns out to be non-injective then it's possible to construct a value of type string N.s bar that matches the pattern in g. For example, N may also export a coercion function

  module M (S : sig type 'a t end) : sig
    val coerce : 'a s S.t -> 'b s S.t

- Issue History
Date Modified Username Field Change
2013-11-04 13:46 lpw25 New Issue
2013-11-04 13:53 lpw25 Note Added: 0010575
2013-11-04 13:54 lpw25 Description Updated View Revisions
2013-11-04 13:59 lpw25 Note Added: 0010577
2013-11-04 14:00 lpw25 Status new => resolved
2013-11-04 14:00 lpw25 Resolution open => no change required
2013-11-04 14:00 lpw25 Assigned To => lpw25
2013-11-04 14:11 yallop Note Added: 0010579
2015-12-11 19:24 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker