Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006158OCamlOCaml typingpublic2013-09-04 14:182013-09-05 11:02
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.01.0+beta/+rc 
Target VersionFixed in Version4.01.0+dev 
Summary0006158: "Fatal error: types should not include variables"
DescriptionThe following code should be rejected but triggers an internal error:

  $ cat vars.ml
  type 'a t = T of 'a
  type 'a s = S of 'a

  type (_, _) eq = Refl : ('a, 'a) eq

  let f : (int s, int t) eq -> unit = function
    | Refl -> ()
  $ ocamlc vars.ml
  >> Fatal error: types should not include variables
  Fatal error: exception Misc.Fatal_error

A similar example with well-typed code gives the same error:

  $ cat vars2.ml
  type (_, _) eq = Refl : ('a, 'a) eq
  
  module M (S : sig
                  type 'a t = T of 'a
                  type 'a s = T of 'a
                end) =
  struct
    let f : ('a S.s, 'a S.t) eq -> unit = function
      | Refl -> ()
  end
  $ ocamlc vars2.ml
  >> Fatal error: types should not include variables
  Fatal error: exception Misc.Fatal_error
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0010314)
garrigue (manager)
2013-09-05 11:02

Fixed in trunk and 4.01, revision 14064.

Indeed, the incompatibility check is more clever than before, but as a result it may be called on type definitions containing variables. No need to fail in that case.

Keep this PR open, as there is a minor side-problem, as the non-principal typechecker may leave reified variables in exported types. They are detected and report when using -principal.
While it would be better to do that without -principal too, this has no impact on soundness.

- Issue History
Date Modified Username Field Change
2013-09-04 14:18 yallop New Issue
2013-09-05 11:02 garrigue Note Added: 0010314
2013-09-05 11:02 garrigue Status new => resolved
2013-09-05 11:02 garrigue Fixed in Version => 4.01.0+dev
2013-09-05 11:02 garrigue Resolution open => fixed
2013-09-05 11:02 garrigue Assigned To => garrigue


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker