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

Polymorphic references lose an argument #3834

Closed
vicuna opened this issue Sep 26, 2002 · 5 comments
Closed

Polymorphic references lose an argument #3834

vicuna opened this issue Sep 26, 2002 · 5 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Sep 26, 2002

Original bug ID: 1411
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Full_Name: Tim Freeman
Version: CVS
OS: linux
Submission from: adsl-64-161-114-6.dsl.snfc21.pacbell.net (64.161.114.6)

If I attempt to compile this file:

module type S = sig
type foo =
[Trouble of int | Other]

 class type ['a] bozzo = object ('self)
   constraint 'a = [<foo]
   method bar: string
 end
           
 class ['a] baz: 'a option -> ['a] bozzo

end

module S: S = struct
type foo =
[Trouble of int | Other]

class type ['a] bozzo =
object ('self)
constraint 'a = [<foo]
method bar: string
end

class ['a] baz (sf: 'a option): ['a] bozzo =
object (self: 'self)
constraint 'a = [<foo]
method bar: string =
match sf with
None -> failwith "ouch"
| Some sf ->
match sf with
`Trouble r -> failwith "ouch"
| _ -> failwith "ouch"
end
end

I get this message:

Signature mismatch:
Modules do not match:
sig
type foo = [ Other | Trouble of int]
class type ['a] bozzo =
object constraint 'a = [< foo] method bar : string end
class ['a] baz :
'a option ->
object constraint 'a = [< foo > Trouble] method bar : string end end is not included in S Class declarations do not match: class ['a] baz : 'a option -> object constraint 'a = [< foo > Trouble] method bar : string end
does not match
class ['a] baz :
'a option -> object constraint 'a = [< foo] method bar : string end
One type parameter has type
[< foo > Trouble] = [< Other | Trouble of int > Trouble]
but is expected to have type [< foo] = [< Other | Trouble of int]

The problem is that the pattern match "Trouble r" toward the end somehow lost the "r", thus leading to the incorrect conclusion that the type parameter for "baz" has to include "Trouble" instead of
"`Trouble of int".

@vicuna
Copy link
Author

vicuna commented Sep 30, 2002

Comment author: administrator

From: tim@fungible.com

Simple answer: the bug is in your code.
The trouble is in the use of an open match on sf:

class ['a] baz (sf: 'a option): ['a] bozzo =
object (self: 'self)
constraint 'a = [<foo]
method bar: string =
match sf with
None -> failwith "ouch"
| Some sf ->
match sf with
`Trouble r -> failwith "ouch"
| _ -> failwith "ouch"
end

Compare these two idioms:

function Trouble x -> x | Other -> 0;;

  • : [< Other | Trouble of int] -> int =

function `Trouble x -> x | _ -> 0;;

  • : [> `Trouble of int] -> int =

If you use an open match, you get a >-type rather than a <-type.
If you unify later, your type ends-up with both < and >.
In this case, you definitely should write `Other rather than _; it may
help you detect errors.
If for some specific reason you still want to use a wild card, you can
write

function `Trouble x -> x | #foo -> 0;;

  • : [< foo] -> int =

For variants open and closed matches are really different constructs,
so much so that at some point we thought of having "_" mean "all
variant tags" rather than "all variant tags allowed by the type". This
proved not to be practical for other reasons, but you should keep this
distinction in mind.

One type parameter has type
[< foo > Trouble] = [< Other | Trouble of int > Trouble]
but is expected to have type [< foo] = [< Other | Trouble of int]

You see now how this crops up from your use of an open match.
By the way, there is no argument to the second occurence of `Trouble
just because it was already given in the first occurence: no need to
repeat. This syntax is described in the reference manual.

    Jacques

@vicuna
Copy link
Author

vicuna commented Oct 7, 2002

Comment author: administrator

Compare these two idioms:

function Trouble x -> x | Other -> 0;;

  • : [< Other | Trouble of int] -> int =

function `Trouble x -> x | _ -> 0;;

  • : [> `Trouble of int] -> int =

If you use an open match, you get a >-type rather than a <-type.
If you unify later, your type ends-up with both < and >.
...
If for some specific reason you still want to use a wild card, you can
write

function `Trouble x -> x | #foo -> 0;;

  • : [< foo] -> int =

I agree, and thank you for saying things that are interesting and true
and new to me. Unfortunately there is more to say, and we get to
continue in the unfortunate internet tradition of ignoring large areas
of agreement and focusing on small areas of disagreement:

In this case, you definitely should write `Other rather than _; it may
help you detect errors.

If I change the only "_" in my example to "`Other", it fails with this
error:

File "foo.ml", line 13, characters 17-532:
Signature mismatch:
Modules do not match:
sig
type foo = [ Other | Trouble of int]
class type ['a] bozzo =
object constraint 'a = [< foo] method bar : string end
class ['a] baz :
'a option ->
object
constraint 'a = [< Other | Trouble of int & 'b]
method bar : string
end
end
is not included in
S
Class declarations do not match:
class ['a] baz :
'a option ->
object
constraint 'a = [< Other | Trouble of int & 'b]
method bar : string
end
does not match
class ['a] baz :
'a option -> object constraint 'a = [< foo] method bar : string end
One type parameter has type
[< Other | Trouble of int & 'a] = [< Other | Trouble of int & 'a]
but is expected to have type [< foo] = [< Other | Trouble of int]

I think it should have unified int with 'a instead of complaining that
Trouble of int & 'a is different from Trouble of int. If I change

             `Trouble r -> failwith "ouch"

to

             `Trouble (r: int) -> failwith "ouch"

it does compile, but I thought the type system was supposed to be able
to figure out what's an int and what isn't without being told.

--
Tim Freeman
tim@fungible.com
GPG public key fingerprint ECDF 46F8 3B80 BB9E 575D 7180 76DF FE00 34B1 5C78

@vicuna
Copy link
Author

vicuna commented Oct 8, 2002

Comment author: administrator

followup problem fixed by JG (2002-10-08)
see ctype.ml, typeclass.ml

@vicuna vicuna closed this as completed Oct 8, 2002
@vicuna
Copy link
Author

vicuna commented Oct 8, 2002

Comment author: administrator

However I followed your advice: unification is now enforced inside
type parameters of a class definition (at definition time). This is
not principal either, but this shall work better in most cases. In
particular your exemple now works correctly.

Thanks.

Tim Freeman
tim@fungible.com
GPG public key fingerprint ECDF 46F8 3B80 BB9E 575D 7180 76DF FE00 34B1 5C78

@vicuna
Copy link
Author

vicuna commented Oct 8, 2002

Comment author: administrator

From: tim@fungible.com (Tim Freeman)

If I change the only "_" in my example to "`Other", it fails with this
error:

File "foo.ml", line 13, characters 17-532:
Signature mismatch:
Class declarations do not match:
class ['a] baz :
'a option ->
object
constraint 'a = [< Other | Trouble of int & 'b]
method bar : string
end
does not match
class ['a] baz :
'a option -> object constraint 'a = [< foo] method bar : string end
One type parameter has type
[< Other | Trouble of int & 'a] = [< Other | Trouble of int & 'a]
but is expected to have type [< foo] = [< Other | Trouble of int]

This is not actually a bug, but just a side-effect of the fact class
are defining types: constraints on parameters are fixed by the
definition, and you cannot refine them in the interface. There are
examples using functors showing that this would be unsound.

I personally think that infering type definitions is not a good idea
(I already removed inference from type declarations), but with classes
there is a subtle balance between clean-ness and usability.

I think it should have unified int with 'a instead of complaining that
Trouble of int & 'a is different from Trouble of int. If I change

             `Trouble r -> failwith "ouch"

to

             `Trouble (r: int) -> failwith "ouch"

it does compile, but I thought the type system was supposed to be able
to figure out what's an int and what isn't without being told.

Well, not with classes: they are known not to be principal.

However I followed your advice: unification is now enforced inside
type parameters of a class definition (at definition time). This is
not principal either, but this shall work better in most cases. In
particular your exemple now works correctly.

Jacques

@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant