0005448: Fancy named type variables are not used in typing error

Notes
(0006528) garrigue (manager) 2011-12-24 02:26	Same comment as PR#5447. I'm not sure inheriting variable names from type definitions makes sense.

(0006535) garrigue (manager) 2011-12-24 04:23	Might consider some future action, but this is not a bug.

(0006538) pilki (reporter) 2011-12-26 17:13	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 = <fun> >>> <<< 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!

(0006539) garrigue (manager) 2011-12-27 07:26	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.

Issue History
Date Modified	Username	Field	Change
2011-12-23 17:10	pilki	New Issue
2011-12-23 17:16	protz	Relationship added	child of 0005444
2011-12-24 02:25	garrigue	Relationship added	related to 0005447
2011-12-24 02:25	garrigue	Assigned To	=> garrigue
2011-12-24 02:25	garrigue	Status	new => assigned
2011-12-24 02:26	garrigue	Note Added: 0006528
2011-12-24 04:23	garrigue	Note Added: 0006535
2011-12-24 04:23	garrigue	Status	assigned => closed
2011-12-24 04:23	garrigue	Resolution	open => no change required
2011-12-26 17:13	pilki	Note Added: 0006538
2011-12-26 17:13	pilki	Status	closed => feedback
2011-12-26 17:13	pilki	Resolution	no change required => reopened
2011-12-27 07:26	garrigue	Note Added: 0006539
2011-12-27 07:26	garrigue	Status	feedback => resolved
2011-12-27 07:26	garrigue	Resolution	reopened => no change required