Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007611OCamltypingpublic2017-08-23 09:542018-06-01 15:51
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.07.0+dev/beta2/rc1/rc2 
Summary0007611: Generative functors are allowed to be applicative !
Descriptionin type expression, it is possible to use generative functors as applicative:

module F () = struct type t end
let f (x: F(List).t) (y: F(List).t) = x=y

Even if safe, I would expect the above program to be rejected !
TagsNo tags attached.
Attached Files

- Relationships
related to 0007726confirmedgarrigue Recursive modules, equi-recursive types and stack overflow 

-  Notes
lpw25 (developer)
2017-08-23 10:30

I noticed this one a while ago and tried to use it to break soundness, but it appears that this bug is not sufficient to break soundness. Of course it is still a bug.
garrigue (manager)
2017-08-23 12:15

Thanks for the report.

Indeed, there is no soundness problem here, since what this code says is just that "if there were values of type F(List).t, then we would be able to compare them". However, the code for generative functor does not allow to create values of this type.

A more correct statement would be "generative functors can be used as applicative constructors in type paths".

I agree that allowing to write this meaningless type is confusing, and this should be eventually rejected.
lpw25 (developer)
2017-08-23 14:37

Well, you can actually create values of some of these nonsense types:

  # module F () = struct
      type t = T
      module F : functor () -> sig type t = T end

  # let x : F(List).t = T;;
  Characters 20-21:
    let x : F(List).t = T;;
  Warning 40: T was selected from type F(List).t.
  It is not visible in the current scope, and will not
  be selected if the type becomes unknown.
  val x : F(List).t = F(List).T

but I think it is still not enough to break soundness.
octachron (developer)
2017-12-13 20:52

This was fixed in, [^]

module F () = struct type t end
let f (x: F(List).t) (y: F(List).t) = x=y;;

now raises an error:

Error: The functor F is generative, it cannot be applied in type expressions

- Issue History
Date Modified Username Field Change
2017-08-23 09:54 lavi New Issue
2017-08-23 10:30 lpw25 Note Added: 0018192
2017-08-23 12:15 garrigue Note Added: 0018193
2017-08-23 12:15 garrigue Assigned To => garrigue
2017-08-23 12:15 garrigue Status new => acknowledged
2017-08-23 14:37 lpw25 Note Added: 0018194
2017-12-13 20:52 octachron Note Added: 0018746
2017-12-13 20:52 octachron Status acknowledged => resolved
2017-12-13 20:52 octachron Fixed in Version => 4.07.0+dev/beta2/rc1/rc2
2017-12-13 20:52 octachron Resolution open => fixed
2018-06-01 15:51 garrigue Relationship added related to 0007726

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker