Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007911OCamltypingpublic2019-02-04 13:412019-02-04 14:13
ReporterSkySkimmer 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusfeedbackResolutionopen 
PlatformOSOS Version
Product Version4.07.1 
Target VersionFixed in Version 
Summary0007911: Unexpected type alias used in type error with -short-paths
DescriptionIn
~~~
module M = struct
  type a
  let f (x:a) = x
end

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 [^])
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019580)
gasche (administrator)
2019-02-04 14:13

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]

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker