|Anonymous | Login | Signup for a new account||2019-02-22 21:06 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007911||OCaml||typing||public||2019-02-04 13:41||2019-02-04 14:13|
|Target Version||Fixed in Version|
|Summary||0007911: Unexpected type alias used in type error with -short-paths|
module M = struct
let f (x:a) = x
type b = M.a
let _ = M.f 2
compiling wit -short-paths says "Error: This expression has type int but an expression was expected of type b"
Using the "b" alias for "M.a" seems to come out of nowhere.
For instance in Coq we define "type module_ident = Id.t" then use the alias as a form of documentation about what some Id.t means in eg a constructor "Foo of module_ident", but then this means we get errors using the alias when it was never involved.
(alias definition https://github.com/coq/coq/blob/506136d60c0dcc4fc2a2ca83ef3b586fbede55a2/kernel/names.mli#L118 [^])
|Tags||No tags attached.|
I don't think this is a bug; -short-paths tries to find one of the shortest paths within the set of equivalent paths, and this is the behavior you observe here.
You seem to have a different specification in mind, where equalities are directed from the new name to its definition, and only expansions in this direction are tried to find a short path. However, I believe that we rely on the other direction (from the definition to the name) to be able to robustly re-fold type definitions in the way the user expects.
(I would expect introducing a Notation in Coq to have the same effect: it may affect the printing of terms that have been written without the notation at all.)
Having the "right" type show up among type-aliases is an ill-defined problem and it is likely that you will never be completely satisfied by the result. If you really care about which types get printed, you have to use incompatible types, for example through aliases:
type foo = Foo of bar [@@unboxed]
|2019-02-04 13:41||SkySkimmer||New Issue|
|2019-02-04 14:13||gasche||Note Added: 0019580|
|2019-02-04 14:13||gasche||Status||new => feedback|
|Copyright © 2000 - 2011 MantisBT Group|