From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <avatar@hot.ee>
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 5D0CB7F89E
	for <caml-list@sympa.inria.fr>; Sat, 22 Mar 2014 21:02:39 +0100 (CET)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  avatar@hot.ee) identity=pra; client-ip=129.217.4.43;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="avatar@hot.ee"; x-sender="avatar@hot.ee";
  x-conformance=sidf_compatible
Received-SPF: SoftFail (mail2-smtp-roc.national.inria.fr: domain
  of avatar@hot.ee is inclined to not designate 129.217.4.43 as
  permitted sender) identity=mailfrom; client-ip=129.217.4.43;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="avatar@hot.ee"; x-sender="avatar@hot.ee";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@honeydew.cs.uni-dortmund.de) identity=helo;
  client-ip=129.217.4.43;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="avatar@hot.ee";
  x-sender="postmaster@honeydew.cs.uni-dortmund.de";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AoIBAFLrLVOB2QQrnGdsb2JhbABZhx/AexYOAQEBAQEGDQkJFCiCT1U2AgUTAwsCCwMCAQIBKxQZCAEBh2ABFAScTY8bmjkMh1cXgSmNboJZgUkEnxGPFw
X-IPAS-Result: AoIBAFLrLVOB2QQrnGdsb2JhbABZhx/AexYOAQEBAQEGDQkJFCiCT1U2AgUTAwsCCwMCAQIBKxQZCAEBh2ABFAScTY8bmjkMh1cXgSmNboJZgUkEnxGPFw
X-IronPort-AV: E=Sophos;i="4.97,710,1389740400"; 
   d="scan'208";a="64154473"
Received: from honeydew.cs.uni-dortmund.de ([129.217.4.43])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 22 Mar 2014 21:02:38 +0100
Received: from postamt.cs.uni-dortmund.de (postamt [129.217.4.40])
	by honeydew.cs.uni-dortmund.de with ESMTP id s2MK2bMN021269
	for <caml-list@inria.fr>; Sat, 22 Mar 2014 21:02:37 +0100 (MET)
Received: from tango.site (cpc20-cmbg14-2-0-cust7.5-4.cable.virginm.net [86.6.28.8])
	(authenticated bits=0)
	by postamt.cs.uni-dortmund.de (8.12.6/8.12.6) with ESMTP id s2MK2axu016946
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NOT)
	for <caml-list@inria.fr>; Sat, 22 Mar 2014 21:02:36 +0100 (MET)
Message-ID: <532DEC4E.6040505@hot.ee>
Date: Sat, 22 Mar 2014 20:02:22 +0000
From: Misha Aizatulin <avatar@hot.ee>
User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0
MIME-Version: 1.0
To: caml-list@inria.fr
X-Enigmail-Version: 1.6
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
X-Validation-by: avatar@hot.ee
Subject: [Caml-list] typechecking


  Using ocaml 4.00.1 the program below successfully compiles. I think
this should be rejected because the call (f t) forces t to be of type t2
whereas the annotation on input function requires it to be of type t1.

type t1 = T1
type t2 = T2

let f T2 = ()

let input (c : in_channel) : t1 =
  let t = input_value c in
  f t;
  t