From: Jonathan Protzenko <jonathan.protzenko@gmail.com>
To: Julien Signoles <julien.signoles@gmail.com>
Cc: caml-list@inria.fr, Roberto Di Cosmo <roberto@dicosmo.org>
Subject: Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS?
Date: Thu, 22 Mar 2012 14:39:15 +0100 [thread overview]
Message-ID: <4F6B2B83.3070003@gmail.com> (raw)
In-Reply-To: <CAPczgCBmVN-qiRv2f-UfnG3gQnCgwmxXO0k=t5+E-N=v7sUa-w@mail.gmail.com>
Jacques Garrigue recently implemented a patch that tries to keep
user-provided type names when printing out types, and also when giving
error messages. In your example, there probably is an internal variable
that's called "a" because of the type name you provided. Some wizardry
happens with GADTs, so another type variable is generated. The other
one ends up being printed, and because it's called "a" too, the
type-checker has to find another suitable name.
Or something like that. Maybe change type a b. to type foo bar. will
give different results :).
Cheers,
jonathan
On Thu 22 Mar 2012 01:05:08 PM CET, Julien Signoles wrote:
> Hello,
>
> Le 22 mars 2012 10:51, Roberto Di Cosmo <roberto@dicosmo.org
> <mailto:roberto@dicosmo.org>> a écrit :
>
> val length : ('a1, 'b) l -> int = <fun>
>
> Why do we get 'a1, and not 'a, in the type?
>
> Well, probably, since 'a is instantiated to int during
> type checking, it may be the case that 'a, as type name, is
> still marked as taken during the type output, so we get ('a1,'b)
>
> The type is perfectly sound... it is just 'surprising' for
> a regular user... do you think this should be considered a bug?
>
>
> IMHO it is not a bug (as you said, the type is sound), but you could
> write a feature request like "generate variable name as best as
> possible"...
>
> --
> Julien
next prev parent reply other threads:[~2012-03-22 13:39 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-03-22 9:51 Roberto Di Cosmo
2012-03-22 12:05 ` Julien Signoles
2012-03-22 13:39 ` Jonathan Protzenko [this message]
2012-03-22 14:40 ` Didier Remy
2012-03-22 22:12 ` Jacques Garrigue
2012-03-22 23:35 ` Roberto Di Cosmo
2012-03-23 5:52 ` Gabriel Scherer
2012-03-23 6:45 ` Jacques Garrigue
2012-03-23 8:13 ` Roberto Di Cosmo
2012-03-23 10:25 ` Gabriel Scherer
2012-03-24 0:24 ` Jacques Garrigue
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=4F6B2B83.3070003@gmail.com \
--to=jonathan.protzenko@gmail.com \
--cc=caml-list@inria.fr \
--cc=julien.signoles@gmail.com \
--cc=roberto@dicosmo.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox