From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <arthur@chargueraud.org>
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 394CC7FB0A
	for <caml-list@sympa.inria.fr>; Tue, 25 Nov 2014 18:33:39 +0100 (CET)
X-IronPort-AV: E=Sophos;i="5.07,456,1413237600"; 
   d="scan'208";a="109531577"
Received: from dhcp-rocq-82.inria.fr (HELO [128.93.62.82]) ([128.93.62.82])
  by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 25 Nov 2014 18:33:39 +0100
Message-ID: <5474BD72.5050909@chargueraud.org>
Date: Tue, 25 Nov 2014 18:33:38 +0100
From: =?UTF-8?B?QXJ0aHVyIENoYXJndcOpcmF1ZA==?= <arthur@chargueraud.org>
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.2
MIME-Version: 1.0
To: caml-list@inria.fr
References: <5474B195.3040108@chargueraud.org> <5474BBE8.6020004@frisch.fr>
In-Reply-To: <5474BBE8.6020004@frisch.fr>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Validation-by: arthur@chargueraud.org
Subject: Re: [Caml-list] teaching OCaml


Ah, sorry for the typo, I meant to say: "the patch is not guaranteed to 
report appropriate error messages for code that would not type-check 
with the -principal flag activated".

In other words, "the patch works as long as the the type-checking of the 
code does not depend on the order in which unifications are performed".

The reason is that the patch performs unification in a different order 
than the standard algorithm (precisely to avoid left-right bias).

Then, the question of whether "-new-type-error" should systematically 
compile all the code (including the one that does not contain type 
errors) using "-principal" is another question, I'm not sure what is the 
best choice.

+
Arthur


>
>> - Document the fact it does not support GADTs, and does not
>>     typecheck with "-principal", in particular code that uses 
>> overloading
>>     of record fields.
>
> Is it really what you mean?  I thought that your alternative 
> type-checking rules would be coherent with the existing ones 
> *provided* that -principal is enabled, so I'd expect this option to be 
> forced when using your mode.
>
>
> -- Alain