From: Sebastien Furic <programming.languages@furic.org>
To: caml-list@inria.fr
Subject: Re: [Caml-list] Clarification needed: use of "as" in patterns (with GADTs)
Date: Mon, 29 Oct 2012 12:19:17 +0100 [thread overview]
Message-ID: <508E6635.1060205@furic.org> (raw)
In-Reply-To: <565CA144-D2B0-45D5-8C2C-845610AE860A@math.nagoya-u.ac.jp>
On 10/20/2012 09:27 AM, Jacques Garrigue wrote:
> Actually, this is not the same issue: the problem here is related to ambiguity inference, which in the case of OCaml is required for soundness in presence of GADTs.
> What happens here is that you Cons constructor introduces an existential variable, which is immediately forced to nonempty by matching against the nested Cons. However is inferred as using this existential variable.
> When typing the recursive call the existential variable is forced to expand to nonempty, but as a result of this expansion it is marked as ambiguous.
>
> When you get such an error message, there is an easy solution: add a type annotation on the faulty expression, using exactly the printed type:
>
> max (xs : ('a, nonempty) my_list)
>
> This is enough to make this program accepted.
>
> It could be argued that in this case there is no ambiguity, since the existential cannot be exported anyway.
> I'll look into that, but you must keep in mind that we must be very careful, as soundness is at stake.
Thank you Jacques, for the explanation and for the hint.
Cheers,
Sébastien.
prev parent reply other threads:[~2012-10-29 11:23 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-10-19 14:05 Sebastien Furic
2012-10-20 7:27 ` Jacques Garrigue
2012-10-29 11:19 ` Sebastien Furic [this message]
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=508E6635.1060205@furic.org \
--to=programming.languages@furic.org \
--cc=caml-list@inria.fr \
/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;
as well as URLs for NNTP newsgroup(s).