From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <Tiphaine.Turpin@irisa.fr>
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by yquem.inria.fr (Postfix) with ESMTP id C75E1BC37
	for <caml-list@yquem.inria.fr>; Tue, 26 Jan 2010 09:09:50 +0100 (CET)
X-IronPort-AV: E=Sophos;i="4.49,345,1262559600"; 
   d="scan'208";a="42189149"
Received: from arvin.irisa.fr (HELO [131.254.11.86]) ([131.254.11.86])
  by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 26 Jan 2010 09:09:50 +0100
Message-ID: <4B5EA286.60603@irisa.fr>
Date: Tue, 26 Jan 2010 09:06:30 +0100
From: Tiphaine Turpin <Tiphaine.Turpin@irisa.fr>
User-Agent: Thunderbird 2.0.0.19 (X11/20090216)
MIME-Version: 1.0
To: caml-list@yquem.inria.fr
Subject: obscur error message
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; irisa:01 subst:01 type-checker:01 unify:01 subst:01 unbound:01 unbound:01 prolog:01 constructor:01 expression:02 defined:02 occurrence:03 let:03 puzzled:04 complain:04 

Hi,

I'm puzzled about the type error returned with the following code (fix :
remove "fs"). Assuming value "mgu" and constructor "Var" are defined, is
it reasonable to report a type error about "subst" rather than the
unbound value "fs" ? I would expect the type-checker to first
successfully type the folded function, (with type (var_name * term) list
-> var_name * term -> (var_name * term) list) and then complain about
unbound value fs.

Tiphaine

let genereal_unify subst eqs =
  List.fold_left (fun subst (x, t) -> mgu subst (Var x) t) subst fs eqs

File "prolog.ml", line 475, characters 42-47: (* i.e., second occurrence
of subst *))
Error: This expression has type 'a -> 'b but is here used with type
         (var_name * term) list