Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generative functors are allowed to be applicative ! #7611

Closed
vicuna opened this issue Aug 23, 2017 · 4 comments
Closed

Generative functors are allowed to be applicative ! #7611

vicuna opened this issue Aug 23, 2017 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Aug 23, 2017

Original bug ID: 7611
Reporter: lavi
Assigned to: @garrigue
Status: resolved (set by @Octachron on 2017-12-13T19:52:31Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Related to: #7726
Monitored by: @gasche @yallop

Bug description

in 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 !

@vicuna
Copy link
Author

vicuna commented Aug 23, 2017

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Aug 23, 2017

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Aug 23, 2017

Comment author: @lpw25

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

  # module F () = struct
      type t = T
    end;;
      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.

@vicuna
Copy link
Author

vicuna commented Dec 13, 2017

Comment author: @Octachron

This was fixed in #1491,

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants