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

Fancy named type variables are not used in typing error #5448

Closed
vicuna opened this issue Dec 23, 2011 · 4 comments
Closed

Fancy named type variables are not used in typing error #5448

vicuna opened this issue Dec 23, 2011 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Dec 23, 2011

Original bug ID: 5448
Reporter: pilki
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2013-08-31T10:44:05Z)
Resolution: not a bug
Severity: feature
Category: ~DO NOT USE (was: OCaml general)
Related to: #5447
Child of: #5444
Monitored by: @protz

Bug description

Say you have
<<<
type ('fst, 'snd) mypair = MkMyPair of 'fst * 'snd
let myfst (MkMyPair (x, _): ('fst, 'snd) mypair) = x

with type inferred:
<<<
type ('fst, 'snd) mypair = MkMyPair of 'fst * 'snd
val myfst : ('fst, 'snd) mypair -> 'fst

then
<<<
let () = myfst

leads to error message:
<<<
Error: This expression has type ('a, 'b) mypair -> 'a
but an expression was expected of type unit

where 'fst and 'snd don't appear

@vicuna
Copy link
Author

vicuna commented Dec 24, 2011

Comment author: @garrigue

Same comment as #5447.
I'm not sure inheriting variable names from type definitions makes sense.

@vicuna
Copy link
Author

vicuna commented Dec 24, 2011

Comment author: @garrigue

Might consider some future action, but this is not a bug.

@vicuna
Copy link
Author

vicuna commented Dec 26, 2011

Comment author: pilki

I guess my example was badly chosen, but here I'm not suggesting to take the name of type variables from type definition. Another (better) example:

<<<
let myfst ((x, _): 'fst * 'snd) = x;;
val myfst : 'fst * 'snd -> 'fst =

<<<
let () = myfst;;
Error: This expression has type 'a * 'b -> 'a
but an expression was expected of type unit

Type variable names are only used in error messages when they are defined locally:
<<<
let f x =
let myfst ((x, y):'fst*'snd) = x in
let () = myfst in ();;
Error: This expression has type 'fst * 'snd -> 'fst
but an expression was expected of type unit

Since you (Jacques) told me the main purpose of this modification on type variables is error reporting, I would almost call that a bug and not a feature request!

@vicuna
Copy link
Author

vicuna commented Dec 27, 2011

Comment author: @garrigue

Sorry, my first answer was a bit ambiguous, as I answered simultaneously several bug.
Here this is about inheriting type variables from a polymorphic value definition.

Actually, your second example precisely demonstrates the advantage of not inheriting:

let f x =
let myfst ((x, y):'fst*'snd) = x in
let () = myfst in ();;
Error: This expression has type 'fst * 'snd -> 'fst
but an expression was expected of type unit

This is different from the first example because named type variables in local
let definitions cannot be generalized. I.e. the type of the second myfst is
precisely 'fst * 'snd -> 'fst, with the same type variables, not an instance of it.
So the property we have is even stronger: if a type variable has the same name
as in a type annotation, it denotes the same variable, and vice-versa.

If we were to keep names upon instantiation, we would need a way to distinguish
instances of a variable from the original, i.e. something like 'fst1 * 'snd1 -> 'fst1,
which in my opinion is not very elegant.

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