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

Unexpected type alias used in type error with -short-paths #7911

Closed
vicuna opened this Issue Feb 4, 2019 · 4 comments

Comments

Projects
None yet
3 participants
@vicuna
Copy link
Collaborator

vicuna commented Feb 4, 2019

Original bug ID: 7911
Reporter: SkySkimmer
Status: feedback (set by @gasche on 2019-02-04T13:13:55Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.07.1
Category: typing
Monitored by: @nojb

Bug description

In

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)

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 4, 2019

Comment author: @gasche

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]

@vicuna vicuna added typing bug labels Mar 14, 2019

@trefis trefis removed the bug label Mar 20, 2019

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Mar 20, 2019

I agree with @gasche: this is not a bug.

For the use case of type aliases that you describe in Coq, I personally would use inline records: Foo of { module_ident: Id.t }.

@trefis trefis closed this Mar 20, 2019

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Mar 20, 2019

@trefis out of curiosity, why are you recommending an inline record rather than (just a record with one field) or (just a variant constructor)? Personally I like the fact that (just a variant constructor) gives more flexibility in naming, but maybe that is what you are against?

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Mar 21, 2019

I guess it's just a personal preference for labels, for examples, if we were talking about functions, I assume you'd suggest:

val sub : string -> pos:int -> len:int -> string

over

type pos = Pos of int [@@unboxed]
type len = Len of int [@@unboxed]

val sub : string -> pos -> len -> string

I agree it's not exactly the same situation, in particular using inline records will allow you to be less robust to changes of the type (because while your constructor might have 5 args, your pattern might look like Foo { one_arg; _ } -> ...). Still, ...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.