diff -urN ocaml-4.01.0-org/Makefile ocaml-4.01.0/Makefile
--- ocaml-4.01.0-org/Makefile	2013-06-17 22:15:18.000000000 +0900
+++ ocaml-4.01.0/Makefile	2014-09-30 18:46:00.000000000 +0900
@@ -57,7 +57,7 @@
   typing/typedtreeIter.cmo typing/typedtreeMap.cmo typing/cmt_format.cmo \
   typing/stypes.cmo typing/typecore.cmo \
   typing/typedecl.cmo typing/typeclass.cmo \
-  typing/typemod.cmo
+  typing/typemod.cmo typing/debug_message.cmo typing/debug_main.cmo
 
 COMP=bytecomp/lambda.cmo bytecomp/printlambda.cmo \
   bytecomp/typeopt.cmo bytecomp/switch.cmo bytecomp/matching.cmo \
diff -urN ocaml-4.01.0-org/driver/compile.ml ocaml-4.01.0/driver/compile.ml
--- ocaml-4.01.0-org/driver/compile.ml	2013-06-06 01:34:40.000000000 +0900
+++ ocaml-4.01.0/driver/compile.ml	2014-09-30 18:46:00.000000000 +0900
@@ -71,9 +71,14 @@
   Env.set_unit_name modulename;
   let inputfile = Pparse.preprocess sourcefile in
   let env = Compmisc.initial_env() in
+  (* Added for type debugger *)
+  let phr = Pparse.file ppf inputfile Parse.implementation ast_impl_magic_number
+  in
   if !Clflags.print_types then begin
     try ignore(
-      Pparse.file ppf inputfile Parse.implementation ast_impl_magic_number
+	    (* Changed for type debugger *)
+	    phr
+      (* Pparse.file ppf inputfile Parse.implementation ast_impl_magic_number *)
       ++ print_if ppf Clflags.dump_parsetree Printast.implementation
       ++ print_if ppf Clflags.dump_source Pprintast.structure
       ++ Typemod.type_implementation sourcefile outputprefix modulename env
@@ -90,7 +95,9 @@
     let objfile = outputprefix ^ ".cmo" in
     let oc = open_out_bin objfile in
     try
-      Pparse.file ppf inputfile Parse.implementation ast_impl_magic_number
+      (* Changed for type debugger *)
+      phr
+      (* Pparse.file ppf inputfile Parse.implementation ast_impl_magic_number *)
       ++ print_if ppf Clflags.dump_parsetree Printast.implementation
       ++ print_if ppf Clflags.dump_source Pprintast.structure
       ++ Typemod.type_implementation sourcefile outputprefix modulename env
@@ -107,7 +114,22 @@
       close_out oc;
       Pparse.remove_preprocessed inputfile;
       Stypes.dump (Some (outputprefix ^ ".annot"));
-    with x ->
+    with 
+(* Added for type debugger *)
+    |  Typecore.Error (_, _, _) as x ->
+(*
+    |  (Typecore.Error(_, Typecore.Expr_type_clash(_)) as x)
+    |  (Typecore.Error(_, Typecore.Pattern_type_clash(_)) as x) -> 
+*)
+      close_out oc;
+      remove_file objfile;
+      Pparse.remove_preprocessed_if_ast inputfile;
+      Stypes.dump (Some (outputprefix ^ ".annot"));
+      Errors.report_error ppf x; 
+      Debug_main.algo (Parsetree.Ptop_def phr) env;
+      exit 2
+(* Added up to here for type debugger *)
+    | x ->
       close_out oc;
       remove_file objfile;
       Pparse.remove_preprocessed inputfile;
diff -urN ocaml-4.01.0-org/driver/pparse.ml ocaml-4.01.0/driver/pparse.ml
--- ocaml-4.01.0-org/driver/pparse.ml	2013-06-06 01:34:40.000000000 +0900
+++ ocaml-4.01.0/driver/pparse.ml	2014-09-30 18:46:00.000000000 +0900
@@ -39,6 +39,13 @@
     None -> ()
   | Some _ -> Misc.remove_file inputfile
 
+ (* added for Type debugger from OCaml 3.12.1 *)
+let remove_preprocessed_if_ast inputfile =
+  match !Clflags.preprocessor with
+    None -> ()
+  | Some _ ->
+      if inputfile <> !Location.input_name then Misc.remove_file inputfile
+
 let write_ast magic ast =
   let fn = Filename.temp_file "camlppx" "" in
   let oc = open_out_bin fn in
diff -urN ocaml-4.01.0-org/driver/pparse.mli ocaml-4.01.0/driver/pparse.mli
--- ocaml-4.01.0-org/driver/pparse.mli	2013-03-19 05:13:53.000000000 +0900
+++ ocaml-4.01.0/driver/pparse.mli	2014-09-30 18:46:00.000000000 +0900
@@ -20,6 +20,7 @@
 
 val preprocess : string -> string
 val remove_preprocessed : string -> unit
+val remove_preprocessed_if_ast : string -> unit
 val file : formatter -> string -> (Lexing.lexbuf -> 'a) -> string -> 'a
 val apply_rewriters : string -> 'a -> 'a
 val report_error : formatter -> error -> unit
diff -urN ocaml-4.01.0-org/parsing/parser.mly ocaml-4.01.0/parsing/parser.mly
--- ocaml-4.01.0-org/parsing/parser.mly	2013-05-16 22:34:53.000000000 +0900
+++ ocaml-4.01.0/parsing/parser.mly	2014-09-30 18:46:00.000000000 +0900
@@ -18,6 +18,16 @@
 open Longident
 open Parsetree
 
+let language_level = try
+  let lang = Sys.getenv "OCAML_LANGUAGE_LEVEL" in
+  match lang with
+    "1" -> 1
+  | "2" -> 2
+  | "3" -> 3
+  | "4" -> 4
+  | _ -> 4
+  with Not_found -> 4
+
 let mktyp d =
   { ptyp_desc = d; ptyp_loc = symbol_rloc() }
 let mkpat d =
@@ -917,8 +927,26 @@
 
 seq_expr:
   | expr        %prec below_SEMI  { $1 }
-  | expr SEMI                     { reloc_exp $1 }
-  | expr SEMI seq_expr            { mkexp(Pexp_sequence($1, $3)) }
+  | expr SEMI                     
+	 { let loc = {
+	     loc_start = Parsing.symbol_start_pos ();
+	     loc_end = Parsing.symbol_end_pos ();
+	     loc_ghost = false;
+	   }
+	   in
+	   if language_level < 3 then (raise(Syntaxerr.Error(Syntaxerr.Expert_exp("sequence", language_level, loc))))
+	   else 
+	     reloc_exp $1 } 
+  | expr SEMI seq_expr
+	 { let loc = {
+	   loc_start = Parsing.symbol_start_pos ();
+	   loc_end = Parsing.symbol_end_pos ();
+	   loc_ghost = false;
+	 }
+	   in
+	 if language_level < 3 then (raise(Syntaxerr.Error(Syntaxerr.Expert_exp("sequence", language_level, loc))))
+	 else 
+	   mkexp(Pexp_sequence($1, $3)) }
 ;
 labeled_simple_pattern:
     QUESTION LPAREN label_let_pattern opt_default RPAREN
@@ -993,17 +1021,44 @@
   | IF seq_expr THEN expr ELSE expr
       { mkexp(Pexp_ifthenelse($2, $4, Some $6)) }
   | IF seq_expr THEN expr
-      { mkexp(Pexp_ifthenelse($2, $4, None)) }
+       { let loc = {
+	   loc_start = Parsing.symbol_start_pos ();
+	   loc_end = Parsing.symbol_end_pos ();
+	   loc_ghost = false;
+	 }
+	   in
+	 if language_level < 3 then (raise(Syntaxerr.Error(Syntaxerr.Expert_exp("if", language_level, loc))))
+	 else mkexp (Pexp_ifthenelse($2, $4, None)) }
   | WHILE seq_expr DO seq_expr DONE
-      { mkexp(Pexp_while($2, $4)) }
+	  { let loc = {
+	      loc_start = Parsing.symbol_start_pos ();
+	      loc_end = Parsing.symbol_end_pos ();
+	      loc_ghost = false;
+	    }
+	    in
+	    if language_level < 4 then (raise(Syntaxerr.Error(Syntaxerr.Expert_exp("while", language_level, loc))))
+	    else mkexp(Pexp_while($2, $4)) }
   | FOR val_ident EQUAL seq_expr direction_flag seq_expr DO seq_expr DONE
-      { mkexp(Pexp_for(mkrhs $2 2, $4, $6, $5, $8)) }
+	{ let loc = {
+	    loc_start = Parsing.symbol_start_pos ();
+	    loc_end = Parsing.symbol_end_pos ();
+	    loc_ghost = false;
+	  }
+	  in
+	  if language_level < 4 then (raise(Syntaxerr.Error(Syntaxerr.Expert_exp("for", language_level, loc))))
+	  else mkexp(Pexp_for(mkrhs $2 2, $4, $6, $5, $8)) }
   | expr COLONCOLON expr
       { mkexp_cons (rhs_loc 2) (ghexp(Pexp_tuple[$1;$3])) (symbol_rloc()) }
   | LPAREN COLONCOLON RPAREN LPAREN expr COMMA expr RPAREN
       { mkexp_cons (rhs_loc 2) (ghexp(Pexp_tuple[$5;$7])) (symbol_rloc()) }
   | expr INFIXOP0 expr
-      { mkinfix $1 $2 $3 }
+	 { if language_level < 4 then (match $2 with
+				      "==" ->
+				      (raise(Syntaxerr.Error(Syntaxerr.InfixOP0("=", language_level, rhs_loc 2) )))
+				    | "!=" ->
+				       (raise(Syntaxerr.Error(Syntaxerr.InfixOP0("<>", language_level, rhs_loc 2) )))
+				    | _ -> mkinfix $1 $2 $3)
+	else mkinfix $1 $2 $3 }
   | expr INFIXOP1 expr
       { mkinfix $1 $2 $3 }
   | expr INFIXOP2 expr
@@ -1029,15 +1084,24 @@
   | expr GREATER expr
       { mkinfix $1 ">" $3 }
   | expr OR expr
-      { mkinfix $1 "or" $3 }
+	 { if language_level < 4 then (raise(Syntaxerr.Error(Syntaxerr.Deprecated("||", "or", language_level, rhs_loc 2) )))
+	else mkinfix $1 "or" $3 }
   | expr BARBAR expr
       { mkinfix $1 "||" $3 }
   | expr AMPERSAND expr
-      { mkinfix $1 "&" $3 }
+	 { if language_level < 4 then (raise(Syntaxerr.Error(Syntaxerr.Deprecated("&&", "&", language_level, rhs_loc 2) )))
+	else mkinfix $1 "&" $3 }
   | expr AMPERAMPER expr
       { mkinfix $1 "&&" $3 }
   | expr COLONEQUAL expr
-      { mkinfix $1 ":=" $3 }
+	 { let loc = {
+	     loc_start = Parsing.symbol_start_pos ();
+	     loc_end = Parsing.symbol_end_pos ();
+	     loc_ghost = false;
+	   }
+	   in
+	   if language_level < 3 then (raise(Syntaxerr.Error(Syntaxerr.Expert_exp("assign", language_level, loc))))
+	   else mkinfix $1 ":=" $3 }
   | subtractive expr %prec prec_unary_minus
       { mkuminus $1 $2 }
   | additive expr %prec prec_unary_plus
diff -urN ocaml-4.01.0-org/parsing/syntaxerr.ml ocaml-4.01.0/parsing/syntaxerr.ml
--- ocaml-4.01.0-org/parsing/syntaxerr.ml	2012-10-16 23:04:33.000000000 +0900
+++ ocaml-4.01.0/parsing/syntaxerr.ml	2014-09-30 18:46:00.000000000 +0900
@@ -19,6 +19,9 @@
   | Expecting of Location.t * string
   | Applicative_path of Location.t
   | Variable_in_scope of Location.t * string
+  | Expert_exp of string * int * Location.t
+  | InfixOP0 of string * int * Location.t
+  | Deprecated of string * string * int * Location.t
   | Other of Location.t
 
 
@@ -52,6 +55,69 @@
         "%a@[In this scoped type, variable '%s@ \
          is reserved for the local type %s.@]"
         Location.print_error loc var var
+  (* language levels *)
+| Expert_exp (str, level, loc) ->
+     (match str with
+	"if" ->
+	if String.length !Location.input_name = 0
+	   && Location.highlight_locations ppf loc loc
+	then fprintf ppf "L%dError1: else 部分を忘れていませんか？@.@." level
+	else begin
+            fprintf ppf "%aelse 部分を忘れていませんか？@.@."
+		    Location.print_error loc;
+	  end
+      | "for" ->
+	if String.length !Location.input_name = 0
+	   && Location.highlight_locations ppf loc loc
+	then fprintf ppf "L%dError2: この言語レベルでは for 文を使うことはできません@.@." level
+	else begin
+            fprintf ppf "%aこの言語レベルでは for 文を使うことはできません@.@."
+		    Location.print_error loc; 
+	  end
+      | "while" ->
+	if String.length !Location.input_name = 0
+	   && Location.highlight_locations ppf loc loc
+	then fprintf ppf "L%dError3: この言語レベルでは while 文を使うことはできません@.@." level
+	else begin
+            fprintf ppf "%aこの言語レベルでは while 文を使うことはできません@.@."
+		    Location.print_error loc;
+	  end
+      | "sequence" ->
+	if String.length !Location.input_name = 0
+	   && Location.highlight_locations ppf loc loc
+	then fprintf ppf "L%dError4: この言語レベルでは逐次実行を使うことはできません@.@." level
+	else begin
+            fprintf ppf "%aこの言語レベルでは逐次実行を使うことはできません@.@."
+		    Location.print_error loc;
+	  end 
+      | "assign" ->
+	if String.length !Location.input_name = 0
+	   && Location.highlight_locations ppf loc loc
+	then fprintf ppf "L%dError5: この言語レベルでは代入を使うことはできません@.@." level
+	else begin
+            fprintf ppf "%aこの言語レベルでは代入を使うことはできません@.@."
+		    Location.print_error loc;
+	  end 
+      | _ -> fprintf ppf "no string@.@.")
+  | InfixOP0 (str, level, loc) ->
+          if String.length !Location.input_name = 0
+      && Location.highlight_locations ppf loc loc
+      then fprintf ppf "L%dError6: %s を使いましょう@.@." level
+		   str
+      else begin
+        fprintf ppf "%a%s を使いましょう@.@."
+		Location.print_error loc str;
+	end
+  | Deprecated (str1, str2, level, loc) ->          
+     if String.length !Location.input_name = 0
+      && Location.highlight_locations ppf loc loc
+      then fprintf ppf "L%dError7: %s はもう使えません。@.%s を使いましょう@.@." level
+		   str2 str1
+      else begin
+        fprintf ppf "%a%s はもう使えません。@.%s を使いましょう@.@."
+		Location.print_error loc str2 str1;
+	end
+     
   | Other loc ->
       fprintf ppf "%aSyntax error" Location.print_error loc
 
@@ -62,3 +128,6 @@
   | Variable_in_scope(l,_)
   | Other l
   | Expecting (l, _) -> l
+  | Expert_exp (_, _, l) -> l
+  | InfixOP0 (_, _, l) -> l
+  | Deprecated (_, _, _, l) -> l
diff -urN ocaml-4.01.0-org/parsing/syntaxerr.mli ocaml-4.01.0/parsing/syntaxerr.mli
--- ocaml-4.01.0-org/parsing/syntaxerr.mli	2012-10-16 23:04:33.000000000 +0900
+++ ocaml-4.01.0/parsing/syntaxerr.mli	2014-09-30 18:46:00.000000000 +0900
@@ -19,6 +19,9 @@
   | Expecting of Location.t * string
   | Applicative_path of Location.t
   | Variable_in_scope of Location.t * string
+  | Expert_exp of string * int * Location.t
+  | InfixOP0 of string * int * Location.t
+  | Deprecated of string * string * int * Location.t
   | Other of Location.t
 
 exception Error of error
diff -urN ocaml-4.01.0-org/toplevel/toploop.ml ocaml-4.01.0/toplevel/toploop.ml
--- ocaml-4.01.0-org/toplevel/toploop.ml	2013-06-06 01:34:40.000000000 +0900
+++ ocaml-4.01.0/toplevel/toploop.ml	2014-09-30 18:46:00.000000000 +0900
@@ -227,6 +227,10 @@
 
 let directive_table = (Hashtbl.create 13 : (string, directive_fun) Hashtbl.t)
 
+(* structures input so far in the reverse order *)
+(* added for Type debugger *)
+let rev_structures = ref []
+
 (* Execute a toplevel phrase *)
 
 let execute_phrase print_outcome ppf phr =
@@ -266,6 +270,7 @@
               Ophr_exception (exn, outv)
         in
         !print_out_phrase ppf out_phr;
+	rev_structures := sstr :: !rev_structures;
         begin match out_phr with
         | Ophr_eval (_, _) | Ophr_signature _ -> true
         | Ophr_exception _ -> false
@@ -328,6 +333,7 @@
       end
     in
     let lb = Lexing.from_channel ic in
+    let last_phrase = ref (Ptop_def []) in
     Location.init lb filename;
     (* Skip initial #! line if any *)
     Lexer.skip_sharp_bang lb;
@@ -337,6 +343,7 @@
           List.iter
             (fun ph ->
               let ph = phrase ppf ph in
+	      last_phrase := ph; (* here? *)
               if not (execute_phrase !use_print_results ppf ph) then raise Exit)
             (if wrap_mod then
                parse_mod_use_file name lb
@@ -346,6 +353,11 @@
         with
         | Exit -> false
         | Sys.Break -> fprintf ppf "Interrupted.@."; false
+	| Typecore.Error (_, _, _) as x ->
+           Errors.report_error ppf x; 
+           Debug_main.algo2 !last_phrase !rev_structures
+                            (Compmisc.initial_env ());
+           false
         | x -> Errors.report_error ppf x; false) in
     if must_close then close_in ic;
     success
@@ -445,6 +457,7 @@
   fprintf ppf "        OCaml version %s@.@." Config.version;
   initialize_toplevel_env ();
   let lb = Lexing.from_function refill_lexbuf in
+  let last_phrase = ref (Ptop_def []) in
   Location.init lb "//toplevel//";
   Location.input_name := "//toplevel//";
   Location.input_lexbuf := Some lb;
@@ -458,12 +471,17 @@
       first_line := true;
       let phr = try !parse_toplevel_phrase lb with Exit -> raise PPerror in
       let phr = phrase ppf phr  in
+      last_phrase := phr; (* here? *)
       Env.reset_cache_toplevel ();
       ignore(execute_phrase true ppf phr)
     with
     | End_of_file -> exit 0
     | Sys.Break -> fprintf ppf "Interrupted.@."; Btype.backtrack snap
     | PPerror -> ()
+    | Typecore.Error (_, _, _) as x ->
+       Errors.report_error ppf x; 
+       Debug_main.algo2 !last_phrase !rev_structures
+                        (Compmisc.initial_env ());
     | x -> Errors.report_error ppf x; Btype.backtrack snap
   done
 
diff -urN ocaml-4.01.0-org/typing/ctype.mli ocaml-4.01.0/typing/ctype.mli
--- ocaml-4.01.0-org/typing/ctype.mli	2013-02-09 17:42:11.000000000 +0900
+++ ocaml-4.01.0/typing/ctype.mli	2014-09-30 18:46:00.000000000 +0900
@@ -183,6 +183,9 @@
         (* Same as [moregeneral false], implemented using the two above
            functions and backtracking. Ignore levels *)
 
+(* added for Type debugger from ctype.ml *)
+val duplicate_type: type_expr -> type_expr
+
 type class_match_failure =
     CM_Virtual_class
   | CM_Parameter_arity_mismatch of int * int
diff -urN ocaml-4.01.0-org/typing/debug_main.ml ocaml-4.01.0/typing/debug_main.ml
--- ocaml-4.01.0-org/typing/debug_main.ml	1970-01-01 09:00:00.000000000 +0900
+++ ocaml-4.01.0/typing/debug_main.ml	2014-09-30 18:46:00.000000000 +0900
@@ -0,0 +1,1271 @@
+(* open Misc
+open Path
+ *)
+open Asttypes
+
+open Types
+open Typedtree
+(* open Ctype *)
+open Format
+
+open Parsetree
+
+open Debug_message
+
+module type A_t = sig
+  val algo : Parsetree.toplevel_phrase -> Env.t -> unit
+  val algo2 : Parsetree.toplevel_phrase -> Parsetree.structure list -> Env.t -> unit
+end
+
+module A : A_t = struct (* beginning of module **********************)
+let language_level = try
+  let lang = Sys.getenv "OCAML_LANGUAGE_LEVEL" in
+  match lang with
+    "1" -> 1
+  | "2" -> 2
+  | "3" -> 3
+  | "4" -> 4
+  | _ -> 4
+  with Not_found -> 4
+
+exception DebuggerQuit
+
+type expr_context =
+    Empty
+  | Lambda of pattern * expr_context
+  | Let of rec_flag * (pattern * expression) list * expr_context
+
+(* type of prefix: reversed list of structure and environment *)
+(* type str_context = (structure * Env.t) list *)
+
+(* type of contexts *)
+(* type 'a context_t = ('a * expr_context) * Env.t * str_context *)
+
+(* expression context_t 型の値 ((exp, cxt), env, lst) の意味は以下 *)
+(* env は (exp, cxt) を実行する際の環境 *)
+(* lst は (structure, env) の逆順のリストで env は structure 実行前の環境 *)
+
+(* plug_expr : expression -> expr_context -> expression *)
+let rec plug_expr expr cxt = match cxt with
+  | Empty -> expr
+  | Lambda (p, c) ->
+      plug_expr { pexp_desc = Parsetree.Pexp_function ("", None, [(p, expr)]);
+		  pexp_loc  = Location.none }
+		c
+  | Let (flag, pates, c) ->
+      plug_expr { pexp_desc = Parsetree.Pexp_let (flag, pates, expr);
+		  pexp_loc  = Location.none }
+		c
+
+(* plug_str : (expression * expr_context) -> structure 
+   : 1つの完全なプログラムにしている *)
+let plug_str (expr, cxt) =
+  [{ pstr_desc = Pstr_eval (plug_expr expr cxt);
+     pstr_loc  = Location.none }]
+
+(* collect_var : pattern -> string list *)
+let rec collect_var pat = match pat.ppat_desc with
+  | Ppat_any -> []
+  | Ppat_var(stloc) -> (match stloc with (* ok? *)
+			  {txt = st;} -> [st])
+  | Ppat_alias(pat, stloc) -> (match stloc with (* ok? *)
+				{txt = st} -> (collect_var pat) @ [st])
+  | Ppat_constant(c) -> []
+  | Ppat_tuple(pats) ->
+      List.flatten (List.map (fun pat -> collect_var pat) pats)
+  | Ppat_construct(l, None, b) -> [] 
+  | Ppat_construct(l, Some(pat), b) -> collect_var pat
+  | Ppat_variant(l, None) -> []
+  | Ppat_variant(l, Some(pat)) -> collect_var pat
+  | Ppat_record(llocpats, _) -> 
+     let lpats = List.map (fun x -> match x with ({txt = loc}, pat)-> (loc, pat)) llocpats  in
+     List.flatten (List.map (fun (l, pat) -> collect_var pat) lpats) (* ok? *)
+  | Ppat_array(pats) ->
+      List.flatten (List.map (fun pat -> collect_var pat) pats)
+  | Ppat_or(pat1, pat2) -> (collect_var pat1) @ (collect_var pat2)
+  | Ppat_constraint(pat, _) -> collect_var pat
+  | Ppat_type(_) -> [] 
+  | Ppat_lazy(pat) -> collect_var pat
+  | Ppat_unpack(stloc) -> (match stloc with {txt = st} -> [st]) (* ok? *)
+
+(* expand_lambda : pattern -> expr_context -> expr_context *)
+let expand_lambda pat cxt =
+  let sts = collect_var pat in
+  List.fold_right (fun st emp ->
+		    Lambda ({ ppat_desc = Ppat_var ({txt = st; loc = Location.none});
+			      ppat_loc = Location.none }, emp))
+		  sts cxt
+
+(* is_well_typed_structure : structure -> Env.t -> bool *)
+(* Error = Location * Env * error になったので引数に env を加えた *)
+let is_well_typed_structure structure env =
+  try
+    ignore (Typemod.type_structure env structure Location.none);
+    true
+  with Typecore.Error (_, _, Typecore.Expr_type_clash (_))
+     | Typecore.Error (_, _, Typecore.Pattern_type_clash (_))
+     | _ (* Unbound value *)
+     -> false
+
+(* is_well_typed_expr : (expression * expr_context) * Env.t * structure ->
+			bool *)
+let is_well_typed_expr ((expr, cxt), env, prefix) =
+  is_well_typed_structure (plug_str (expr, cxt)) env
+
+(* pat_appears : string -> pattern -> bool *)
+let rec pat_appears st pat = match pat.ppat_desc with
+    Ppat_any -> false
+  | Ppat_var (st') -> (match st' with {txt = st2} -> st = st2) (* ok? *)
+  | Ppat_alias (_, st') -> (match st' with {txt = st2} -> st = st2) (* ok? *)
+  | Ppat_constant (_) -> false
+  | Ppat_tuple (ps) | Ppat_array (ps) -> List.exists (pat_appears st) ps 
+  | Ppat_construct (_, None, _) -> false
+  | Ppat_construct (_, Some(p), _) -> pat_appears st p
+  | Ppat_variant (_, None) -> false
+  | Ppat_variant (_, Some(p)) -> pat_appears st p
+  | Ppat_record (llocps, _) -> 
+     let lps = List.map (fun x -> match x with ({txt = ident;}, pat) -> (ident, pat)) llocps in
+     List.exists (fun (_, p) -> pat_appears st p) lps (* ok? *)
+  | Ppat_or (p1, p2) -> pat_appears st p1 || pat_appears st p2
+  | Ppat_constraint (p, _) -> pat_appears st p
+  | Ppat_type (_) -> false
+  | Ppat_lazy (p) -> pat_appears st p
+  | Ppat_unpack (stloc) -> (match stloc with {txt = st'} -> st' = st) (* ok? *)
+
+(* pat_search : string -> pattern -> pattern *)
+let rec pat_search st pat = match pat.ppat_desc with
+    Ppat_any -> raise Not_found
+  | Ppat_var (st') -> (match st' with {txt = st2} -> if st = st2 then pat else raise Not_found) (* ok? *)
+  | Ppat_alias (_, st') -> (match st' with {txt = st2} -> if st = st2 then pat else raise Not_found) (* ok? *)
+  | Ppat_constant (_) -> raise Not_found
+  | Ppat_tuple (ps) | Ppat_array(ps) -> pat_search_list st ps
+  | Ppat_construct (_, None, _) -> raise Not_found
+  | Ppat_construct (_, Some(p), _) -> pat_search st p
+  | Ppat_variant (_, None) -> raise Not_found
+  | Ppat_variant (_, Some(p)) -> pat_search st p
+  | Ppat_record (llocps, _) -> 
+     let lps = List.map (fun x -> match x with ({txt = ident}, pat) -> (ident, pat)) llocps in
+     pat_search_list st (List.map snd lps) (* ok? *)
+  | Ppat_or (p1, p2) -> pat_search_list st [p1; p2]
+  | Ppat_constraint (p, _) -> pat_search st p
+  | Ppat_type (_) -> raise Not_found
+  | Ppat_lazy (p) -> pat_search st p
+  | Ppat_unpack (stloc) -> (match stloc with {txt = st2} -> if st = st2 then pat else raise Not_found) (* ok? *)
+and pat_search_list st pats = match pats with
+    [] -> raise Not_found
+  | pat :: rest ->
+      (try pat_search st pat
+       with Not_found -> pat_search_list st rest)
+
+(* pat_to_expr : pattern -> expression *)
+let rec pat_to_expr { ppat_desc = desc; ppat_loc = loc } = 
+  { pexp_desc = pat_to_expr' desc; pexp_loc = loc }
+and pat_to_expr' desc = match desc with
+  | Ppat_any -> assert false
+  | Ppat_var (stloc) -> (match stloc with {txt = st; loc = l} ->
+				    Pexp_ident ({txt = Longident.Lident (st); loc = l})) (* ok? *)
+  | Ppat_alias(pat, stloc) -> 
+      let {pexp_desc = pat; pexp_loc = loc} = pat_to_expr pat in
+	    pat
+  | Ppat_constant(c) -> Pexp_constant(c)
+  | Ppat_tuple(pats) -> 
+	  Pexp_tuple(List.map (fun pat -> pat_to_expr pat) pats)
+  | Ppat_construct(lloc, None, b) ->
+	  Pexp_construct(lloc, None, b)
+  | Ppat_construct(lloc, Some(e), b) ->
+	  Pexp_construct(lloc, Some(pat_to_expr e), b)
+  | Ppat_variant(l, None) ->
+	  Pexp_variant(l, None)
+  | Ppat_variant(l, Some(e)) ->
+	  Pexp_variant(l, Some(pat_to_expr e))
+  | Ppat_record(ls, _) ->
+	  Pexp_record(List.map (fun (l, p) ->(l, pat_to_expr p)) ls, None)
+	    (*  | Ppat_record of (Longident.t * pattern) list * closed_flag *)
+  | Ppat_array(pats) ->
+	  Pexp_array(List.map (fun pat -> pat_to_expr pat) pats)
+	    (* | Ppat_or of pattern * pattern *)
+  | Ppat_constraint(pat, core_type) ->
+	  Pexp_constraint(pat_to_expr pat, Some(core_type), None)
+  | Ppat_lazy(p) -> (pat_to_expr p).pexp_desc
+  | Ppat_or(_) | Ppat_type(_) -> assert false
+  | Ppat_unpack (_) -> assert false (* 対応しているものがどれか分からない *)
+
+(* is_arrow : type_expr -> bool *)
+let rec is_arrow typ = match typ.desc with
+    Tarrow (_, t1, t2, _) -> true
+  | Tlink (typ') -> is_arrow typ'
+  | _ -> false
+
+(* type of elements of yes/no list *)
+(* type yes_no_list = (string context_t * type_expr) list *)
+
+(* collect_one : (string context_t * type_expr) context_t -> pattern ->
+		 type_expr -> yes_no_list * type_expr *)
+let rec collect_one ((vartyps, cxt'), env, prefix) p t = match t.desc with
+    Tarrow (_, t1, t2, _) ->
+      (match p with
+	  { ppat_desc = Ppat_var(stloc) } -> 
+	  (match stloc with {txt = st} -> ((((st, cxt'), env, prefix), t1) :: vartyps, t2))
+	| _ -> (vartyps, t2))
+  | Tlink (t') -> collect_one ((vartyps, cxt'), env, prefix) p t'
+  | _ -> assert false
+
+(* collect : expression context_t -> type_expr -> yes_no_list * type_expr *)
+let rec collect ((expr, cxt), env, prefix) t = match cxt with
+    Empty -> ([], t)
+  | Lambda (p, cxt') ->
+      (* There and back again [Danvy&Goldberg ICFP'02] *)
+      let (vartyps, t') = collect ((expr, cxt'), env, prefix) t in
+      collect_one ((vartyps, cxt'), env, prefix) p t'
+  | Let (_, _, cxt') -> collect ((expr, cxt'), env, prefix) t
+
+(* judge : expression context_t -> yes_no_list * type_expr *)
+let judge ((expr, cxt), env, prefix) =
+  let (structure', _, _) =
+    Typemod.type_structure env (plug_str (expr, cxt)) Location.none in (* arguments...? *)
+  match structure'.str_items with
+    {str_desc = strd} :: [] -> (* ok? *)
+    (match strd with
+     | Tstr_eval ({ exp_type = typ }) ->
+	collect ((expr, cxt), env, prefix) typ
+     | _ -> assert false)
+  | _ -> assert false
+
+(* get_from_strcxt : string -> str_context -> expression context_t option *)
+let rec get_from_strcxt st prefix = match prefix with
+    [] -> (* This happens when no binding is found, such as for '+' *)
+      None
+  | ({ pstr_desc=Pstr_value (flg, patexps) }, env) :: rest ->
+      let rec loop patexps = match patexps with
+          [] -> get_from_strcxt st rest
+	| (p, e) :: rest' ->
+	    if pat_appears st p then (* pat の追加？ *)
+	      if flg = Recursive
+	      then Some ((e, Lambda (p, Empty)), env, rest)
+	      else Some ((e, Empty), env, rest)
+	    else loop rest'
+      in loop patexps
+  | _ :: rest -> get_from_strcxt st rest
+
+(* get : string context_t -> expression context_t option *)
+let rec get ((st, cxt), env, prefix) = match cxt with
+    Empty -> get_from_strcxt st prefix
+  | Lambda (p, cxt') ->
+      if pat_appears st p then None else get ((st, cxt'), env, prefix)
+  | Let (flg, patexps, cxt') ->
+      let rec loop patexps = match patexps with
+          [] -> get ((st, cxt'), env, prefix)
+	| (p, e) :: rest ->
+	    if pat_appears st p then (* pat の追加？ *)
+	      if flg = Recursive
+	      then Some ((e, Lambda (p, cxt)), env, prefix)
+	      else Some ((e, cxt'), env, prefix)
+	    else loop rest
+      in loop patexps
+
+(* dummy_int0 : expression *)
+let dummy_int0 = {
+  pexp_desc = Pexp_constant (Const_int 0);
+  pexp_loc  = Location.none;
+}
+
+(* three phases of decompose *)
+(* 名前、要変更 *)
+type decompose_phase_t =
+    Illtyped (* decompose する式には型がつかない *)
+  | Typed_fv (* 型はついていて、自由変数が意図に合っているかを確かめている *)
+  | Typed    (* 型はついていて、その型が意図に合っているかを確かめている *)
+
+(* decompose_patexps : (pattern * expression) list context_t ->
+		       expression context_t list *)
+let decompose_patexps ((patexps, cxt), env, prefix) =
+  List.map (fun (pat, exp) -> ((exp, Lambda (pat, cxt)), env, prefix))
+	   patexps
+
+(* decompose_expand_patexps : (pattern * expression) list context_t ->
+			      expression context_t list *)
+let decompose_expand_patexps ((patexps, cxt), env, prefix) =
+  List.map (fun (pat, exp) -> ((exp, expand_lambda pat cxt), env, prefix))
+	   patexps
+
+(* decompose_expr : expression context_t -> decompose_phase_t ->
+		    expression context_t list *)
+let rec decompose_expr ((exp, cxt), env, prefix) phase =
+  match exp.pexp_desc with
+     Parsetree.Pexp_ident (lloc) ->
+       (match phase with
+	   Illtyped | Typed_fv -> []
+	 | Typed -> 
+	    (match lloc with {txt = l} -> (* ok? *)
+			  (match l with
+			     Longident.Lident (st) ->
+			     (match get ((st, cxt), env, prefix) with
+				None -> []
+			      | Some ((exp', cxt'), env', prefix') ->
+				 [((exp', cxt'), env', prefix')])
+			   | Longident.Ldot (t, st) -> []
+			   | Longident.Lapply (t1, t2) -> [])))
+   | Parsetree.Pexp_constant (c) -> []
+   | Parsetree.Pexp_let (rec_flg, patexps, exp) -> (match phase with
+(* ------------------------------------------------------------------------ *)
+  Illtyped ->
+       (* let 文で定義された変数を含めたコンテキストを cxt' とする *)
+       let cxt' = List.fold_right (fun (pat, _) c -> expand_lambda pat c)
+				  patexps cxt in
+       (if rec_flg = Recursive
+	then List.map (fun (_, exp) -> ((exp, cxt'), env, prefix)) patexps
+	     (* 再帰関数なら、cxt' を使う *)
+	else List.map (fun (_, exp) -> ((exp, cxt), env, prefix)) patexps)
+    (* @ [(prefix, (cxt', exp))] *)
+	 (* exp 中からは束縛された値は見えない *)
+	 (* これでは単相になるのでだめ *)
+| Typed_fv ->
+       (* let 文で定義された変数を含めたコンテキストを cxt' とする *)
+       let cxt' = List.fold_right (fun (pat, _) c -> expand_lambda pat c)
+				  patexps cxt in
+       (if rec_flg = Recursive
+	then List.map (fun (_, exp) -> ((exp, cxt'), env, prefix)) patexps
+	     (* 再帰関数なら、cxt' を使う *)
+	else List.map (fun (_, exp) -> ((exp, cxt), env, prefix)) patexps)
+       @ [((exp, Let (rec_flg, patexps, cxt)), env, prefix)]
+	 (* exp 中から束縛された値が見える *)
+| Typed -> [((exp, Let (rec_flg, patexps, cxt)), env, prefix)]
+	 (* exp 中から束縛された値が見える *)
+   )
+(* ------------------------------------------------------------------------ *)
+   | Parsetree.Pexp_function (lbl, exp_op, patexps) ->
+       (match exp_op with
+	   None -> decompose_expand_patexps ((patexps, cxt), env, prefix)
+	 | Some (exp) ->
+	     ((exp, cxt), env, prefix) ::
+	       decompose_expand_patexps ((patexps, cxt), env, prefix))
+       (* パターンは、常に cxt に入れて構わない *)
+       (* それが問題でも、exps の中で顕在化するので *)
+       (* と、思ったが、それは exp に型がついている場合 *)
+       (* 型がついていないときは、パターンの制約が conflict しているかも *)
+       (* パターンは常に展開して、fun が原因と特定されたら、パターンを *)
+       (* 原因と特定する方針に変更 *)
+   | Parsetree.Pexp_apply (exp, lexps) ->
+       ((exp, cxt), env, prefix) ::
+	 List.map (fun (_, exp) -> ((exp, cxt), env, prefix)) lexps
+   | Parsetree.Pexp_match (exp, patexps) ->
+       ((exp, cxt), env, prefix) ::
+	 decompose_expand_patexps ((patexps, cxt), env, prefix)
+       (* とりあえず expand するようにしたが、パターンが原因だった場合の *)
+       (* 対処はまだ *)
+   | Parsetree.Pexp_try (exp, patexps) ->
+       ((exp, cxt), env, prefix) ::
+	 decompose_expand_patexps ((patexps, cxt), env, prefix)
+       (* とりあえず expand するようにしたが、パターンが原因だった場合の *)
+       (* 対処はまだ *)
+   | Parsetree.Pexp_tuple (exps) ->
+      (*(Format.fprintf (Format.std_formatter) "list@\n");*)
+       List.map (fun exp -> ((exp, cxt), env, prefix)) exps 
+   | Parsetree.Pexp_construct (lloc, None, b) -> []
+   | Parsetree.Pexp_construct (lloc, Some(exp), b) ->
+       (* (Format.fprintf (Format.std_formatter) "list@\n");*)
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_variant (l, None) -> []
+   | Parsetree.Pexp_variant (l, Some(exp)) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_record (lexps, None) ->
+       List.map (fun (l, exp) -> ((exp, cxt), env, prefix)) lexps
+   | Parsetree.Pexp_record (llocexps, Some (exp)) ->
+      (* TODO: exp ? *)
+      let lexps = List.map (fun x -> match x with ({txt = ident}, e) -> (ident, e)) llocexps in
+      List.map (fun (l, exp) -> ((exp, cxt), env, prefix)) lexps
+   | Parsetree.Pexp_field (exp, lloc) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_setfield (exp1, lloc, exp2) ->
+       [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix)]
+   | Parsetree.Pexp_array (exps) ->
+       List.map (fun exp -> ((exp, cxt), env, prefix)) exps 
+   | Parsetree.Pexp_ifthenelse (exp1, exp2, None) ->
+       [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix)]
+   | Parsetree.Pexp_ifthenelse (exp1, exp2, Some(exp3)) ->
+       [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix);
+	((exp3, cxt), env, prefix)]
+   | Parsetree.Pexp_sequence (exp1, exp2) ->
+       [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix)]
+   | Parsetree.Pexp_while (exp1, exp2) ->
+       (* [(cxt, exp1, dummy_tvar ()); (cxt, exp2, t)] *)
+       [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix)]
+   | Parsetree.Pexp_for (stloc, exp1, exp2, _, exp3) ->
+       [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix);
+	((exp3, cxt), env, prefix)]
+   | Parsetree.Pexp_constraint (exp, op1, op2) ->
+      (* TODO : other argument *)
+      (* [(prefix, (cxt, exp))] *)
+      (match (op1, op2) with
+	    (None, None) -> Format.fprintf (Format.std_formatter) "None, None@\n"
+	  | (Some (t1), None) -> Format.fprintf(Format.std_formatter) "Some None@\n";
+				 (match t1.ptyp_desc with
+				    Ptyp_any -> ()
+				  | Ptyp_var (s) -> 
+				     Format.fprintf (Format.std_formatter) "Ptyp.var %s@\n" s
+				  | Ptyp_arrow (l, c1, c2) -> ()
+				  | Ptyp_tuple (clist) -> ()
+				  | Ptyp_constr (sloc, lst) -> 
+				     (match sloc with
+					{txt = Longident.Lident(s)} -> Format.fprintf (Format.std_formatter) "Ptyp.constr %s@\n" s
+				       | _ -> Format.fprintf (Format.std_formatter) "Ptyp.constr: not Lident@\n")
+				  (* | Ptyp_constr (_, lst) -> () *)
+				  | _ -> ())
+	  (*
+		 | Ptyp_object of core_field_type list
+		 | Ptyp_class of Longident.t * core_type list * label list
+		 | Ptyp_alias of core_type * string
+		 | Ptyp_variant of row_field list * bool * label list option
+		 | Ptyp_poly of string list * core_type
+		 | Ptyp_package of package_type
+	   *)
+	  (* ); *)
+	  (*Printtyp.type_expr t1*)
+	  | (None, Some (t2)) -> Format.fprintf(Format.std_formatter) "None Some@\n"
+	  (*Printtyp.type_expr t2*)
+	  |(Some (t1), Some (t2)) -> 
+	    Format.fprintf(Format.std_formatter) "Some Some@\n"
+      (*Printtyp.type_expr t1
+	       Printtyp.type_expr t2 *) );
+      decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_when (exp1, exp2) ->
+      [((exp1, cxt), env, prefix); ((exp2, cxt), env, prefix)]
+   | Parsetree.Pexp_send (exp, st) ->
+      (* [(prefix, (cxt, exp))] *)
+      decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_new (lloc) -> []
+       (* let (str, _ ) = cxt in
+	  List.flatten (search_class (List.rev str) l cxt) *)
+   | Parsetree.Pexp_setinstvar (stloc, exp) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_override (stlocexps) ->
+      let stexps = List.map (fun x -> match x with ({txt = s}, e) -> (s, e)) stlocexps in
+       List.map (fun (st, exp) -> ((exp, cxt), env, prefix)) stexps
+   | Parsetree.Pexp_letmodule (stloc, _, exp) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_assert (exp) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_assertfalse -> []
+   | Parsetree.Pexp_lazy (exp) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_poly (exp, _)->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_object (class_structure) -> []
+       (* let cxt' = addcxt_str cxt (fun cxt -> Lambda (pat, cxt)) in
+	  decompose_class cxt' class_structure *)
+   | Parsetree.Pexp_newtype (st, exp) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+   | Parsetree.Pexp_pack (module_expr) -> []
+   | Parsetree.Pexp_open (flag, stloc, exp) ->
+       (* [(prefix, (cxt, exp))] *)
+       decompose_expr ((exp, cxt), env, prefix) phase
+
+(* trace_answer : bool *)
+(* change this variable to true to show the answer trace *)
+let trace_answer = false
+
+(* answered_yes : string context_t -> type_expr -> yes_no_list -> Env.t ->
+		  bool *)
+let answered_yes (((st, _), _, _) as key) typ yes env = try
+  let t = List.assoc key yes in
+  let b = Ctype.moregeneral env false (Ctype.duplicate_type typ)
+				      (Ctype.duplicate_type t) in
+  if trace_answer then Format.fprintf Format.std_formatter
+			 "answered_yes %s = %b@\n" st b;
+  b
+with Not_found -> false
+
+(* answered_no : string context_t -> type_expr -> yes_no_list -> Env.t ->
+		 bool *)
+let answered_no (((st, _), _, _) as key) typ no env = try
+  let t = List.assoc key no in
+  let b = Ctype.moregeneral env false (Ctype.duplicate_type t)
+				      (Ctype.duplicate_type typ) in
+  if trace_answer then Format.fprintf Format.std_formatter
+			 "answered_no %s = %b@\n" st b;
+  b
+with Not_found -> false
+
+(* ask_env : expression -> (string context_t * type_expr) list -> Env.t ->
+	     yes_no_list -> yes_no_list ->
+	     bool * yes_no_list * yes_no_list *)
+let rec ask_env expr vartyps env yes no = match vartyps with
+    [] -> (true, yes, no)
+  | (((st, _), _, _) as key, typ) :: rest ->
+      if Ctype.moregeneral env false
+			   (Ctype.duplicate_type typ) (Btype.newgenvar ())
+      || answered_yes key typ yes env
+      then ask_env expr rest env yes no
+      else if answered_no key typ no env
+      then (false, yes, no)
+      else (print_loc expr.pexp_loc;
+	    print_ask_env st typ;
+	    print_prompt ();
+	    let input = read_line () in
+	    fprintf std_formatter "@.";
+	    match input with
+		"y" | "y;;" -> ask_env expr rest env ((key, typ) :: yes) no
+	      | "n" | "n;;"  -> (false, yes, (key, typ) :: no)
+	      | _ -> raise DebuggerQuit)
+
+(* ask_expr : expression -> type_expr -> Env.t -> yes_no_list -> yes_no_list ->
+	      bool * yes_no_list * yes_no_list *)
+let ask_expr expr t env yes no =
+  (* 今は yes, no を使っていないが、expr が id だったら使えるか *)
+  if Ctype.moregeneral env false
+		       (Ctype.duplicate_type t) (Btype.newgenvar ())
+  then (true, yes, no)
+  else (print_loc expr.pexp_loc;
+	print_ask_expr t;
+	print_prompt ();
+	let input = read_line () in
+	fprintf std_formatter "@.";
+	match input with
+	    "y" | "y;;" -> (true, yes, no)
+	  | "n" | "n;;" -> (false, yes, no)
+	  | _ -> raise DebuggerQuit) (* 終わらせないようにしたい *)
+
+(* has_intended_type : expression context_t -> yes_no_list -> yes_no_list ->
+		       bool * yes_no_list * yes_no_list *)
+let has_intended_type ((expr, cxt), env, prefix) yes no =
+  let (vartyps, typ) = judge ((expr, cxt), env, prefix) in
+  let (b, yes', no') = ask_env expr vartyps env yes no in
+  if b
+  then ask_expr expr typ env yes' no'
+  else (false, yes', no')
+
+(* clean_yes_no_list : yes_no_list -> yes_no_list *)
+let rec clean_yes_no_list no = match no with
+    [] -> []
+  | (((st, cxt), env, prefix), typ) :: rest ->
+      (((st, cxt), env, prefix), typ) ::
+	clean_yes_no_list (List.filter (fun (((st', _), _, _), _) -> st <> st')
+				       rest)
+
+(* print_answers : yes_no_list -> unit *)
+let print_answers no =
+  let rec loop no = match no with
+      [] ->
+	Format.fprintf Format.std_formatter "@]@\n"
+    | (((st, cxt), env, prefix), typ) :: [] ->
+	Format.fprintf Format.std_formatter
+	  "%s : %a@]@\n" st Printtyp.type_expr typ
+    | (((st, cxt), env, prefix), typ) :: rest ->
+	Format.fprintf Format.std_formatter
+	  "%s : %a,@ " st Printtyp.type_expr typ;
+	loop rest
+  in if no <> []
+     then (Format.fprintf Format.std_formatter "no: @[";
+	   loop (clean_yes_no_list no))
+
+(* make_message_recursive : (pattern * expression) list ->
+			    expression context_t list -> unit *)
+let make_message_recursive patexps progs =
+  let rec search st vartyps = match vartyps with
+      [] -> assert false
+    | (((st', _), _, _), typ) :: rest ->
+	if st = st' then typ else search st rest in
+  let rec loop lst progs vars = match (lst, progs, vars) with
+      ([], [], []) -> ()
+    | ((vartyps, typ) :: lst, ((expr, cxt), env, prefix) :: progs, st :: vars)->
+	let typ' = search st(* List.assoc ((st, cxt), env, prefix) *) vartyps in
+	if Ctype.moregeneral env false
+			     (Ctype.duplicate_type typ)
+			     (Ctype.duplicate_type typ')
+	then loop lst progs vars
+	else (print_loc expr.pexp_loc;
+	      print_identified ();
+	      print_recursive typ st typ')
+    | _ -> assert false
+  in
+  let lst = List.map judge progs in
+  let vars = List.map (fun (p, _) -> match p.ppat_desc with
+					 Ppat_var (stloc) -> 
+					 (match stloc with {txt = st} -> st) (* ok? *)
+				       | _ -> assert false)
+		      patexps in
+  loop lst progs vars
+
+(* make_message_patexps : (pattern * expression) list context_t -> unit *)
+let make_message_patexps ((patexps, cxt), env, prefix) =
+  let rec loop patexps = match patexps with
+      [] -> assert false
+    | (pat, exp) :: rest ->
+	if is_well_typed_expr
+	     (({ pexp_desc = Parsetree.Pexp_let (Nonrecursive, [(pat, exp)],
+						 dummy_int0);
+		 pexp_loc  = Location.none }, cxt), env, prefix)
+	then loop rest
+	else
+	  (* 束縛する変数が pattern の constant 以外はダメ *)
+	  (match pat with
+	     {ppat_desc = Ppat_constant (c)} -> (* constant のとき *)
+	     print_loc pat.ppat_loc;
+	     print_identified ();
+	     print_patexps2 ();
+	   | _ -> (* それ以外のパターン *)
+	      (let (_, typ) = judge ((exp, cxt), env, prefix) in
+	       print_loc exp.pexp_loc;
+	       print_identified ();
+	       print_patexps typ))
+  in loop patexps
+
+(* search_conflict_env : (string context_t * type_expr) list -> Env.t -> yes_no_list -> yes_no_list -> yes_no_list *)
+(* ask_env とほぼ同じ *)
+let rec search_conflict_env vartyps env no conf_list = match vartyps with
+    [] -> conf_list
+  | (((st, _), _, _) as key, typ) :: rest ->
+     if answered_no key typ no env
+     then search_conflict_env rest env no ((key, typ) :: conf_list)
+     else search_conflict_env rest env no conf_list
+
+let rec make_dummy_patexps lst = 
+  let dummy = { pexp_desc = Pexp_assertfalse;
+		pexp_loc = Location.none } in
+  match lst with
+      [] -> []
+    | (pat, exp) :: rst -> 
+	  (pat, dummy) :: (make_dummy_patexps rst)
+
+(* make_pattern_match : Parsetree.match -> Parsetree.match *)
+let make_pattern_match mth = match mth with
+    { pexp_desc = Pexp_match (exp, lst) } -> 
+      let new_patexps = make_dummy_patexps lst in
+	{ pexp_desc = Pexp_match (exp, new_patexps);
+	  pexp_loc = exp.pexp_loc }
+  | _ -> raise DebuggerQuit (* とりあえず *)
+
+(* make_message_welltyped : expression context_t -> yes_no_list -> unit *)
+let make_message_welltyped ((expr, cxt), env, prefix) no =
+  let no' = clean_yes_no_list no in
+  let (vartyps, t) = judge ((expr, cxt), env, prefix) in
+  let vartyps' = List.filter (fun (key, typ) -> answered_no key typ no' env)
+			     vartyps in
+  (match expr.pexp_desc with 
+   | Parsetree.Pexp_ifthenelse (exp1, exp2, None) ->
+      (* 1. exp1 を no と言っていたら*)
+      (* exp1 に bool annotation を付ける *)
+      let lidentloc = {txt = Longident.Lident ("bool"); loc = Location.none} in
+      let exp1' = { pexp_desc = Pexp_constraint 
+				  (exp1, Some({ ptyp_desc = Ptyp_constr (lidentloc, []);
+						ptyp_loc = Location.none }), None); 
+		    pexp_loc = Location.none } in
+      let (bool_env, typ) = judge ((exp1', cxt), env, prefix) in
+      let conf_list = search_conflict_env bool_env env vartyps' [] in
+      (match conf_list with
+	 [] -> (* exp1 は bool と意図されている *)
+	 (* 2. exp2 に unit annotation を付ける *)
+	 let lidentloc2 = {txt = Longident.Lident ("unit"); loc = Location.none} in
+	 let exp2' = { pexp_desc = Pexp_constraint 
+				     (exp2, Some({ ptyp_desc = Ptyp_constr (lidentloc2, []);
+						   ptyp_loc = Location.none }), None); 
+		       pexp_loc = Location.none } in
+	 let (unit_env, typ) = judge ((exp2', cxt), env, prefix) in
+	 let conf_list = search_conflict_env unit_env env vartyps' [] in
+	 (match conf_list with
+	    [] ->   print_loc expr.pexp_loc;
+		    print_identified ();
+		    print_welltyped_expr t (* exp2 は unit と意図されている -> 部分プログラムは意図通り *)
+	  | (((st, _), _, _), typ) :: rest -> 
+	     print_loc exp2.pexp_loc;
+	     print_identified ();
+	     print_welltyped_if_unit st typ rest (* unit と意図されていない *)
+	 )
+       | (((st, _), _, _), typ) :: rest -> 
+	  print_loc exp1.pexp_loc;
+	  print_identified ();
+	  print_welltyped_if_bool st typ rest (* bool と意図されていない *)
+      )
+   | Parsetree.Pexp_ifthenelse (exp1, exp2, Some (exp3)) ->
+      (* 1. exp1 を no と言っていたら*)
+      (* exp1 に bool annotation を付ける *)
+      let lidentloc = {txt = Longident.Lident ("bool"); loc = Location.none} in
+      let exp1' = { pexp_desc = Pexp_constraint 
+				  (exp1, Some({ ptyp_desc = Ptyp_constr (lidentloc, []);
+						ptyp_loc = Location.none }), None); 
+		    pexp_loc = Location.none } in
+      let (bool_env, typ) = judge ((exp1', cxt), env, prefix) in
+      let conf_list = search_conflict_env bool_env env vartyps' [] in
+      (match conf_list with
+	 [] -> (* exp1 は bool と意図されている *)
+	 (* 2. exp2 と exp3 の型が同じかを見る *)
+       (* exp2 と exp3 を同じリストに入れる *)
+	 let mtloc = {txt = Longident.Lident ("[]"); loc = Location.none} in 
+	 let mt = { pexp_desc = Pexp_construct (mtloc,
+					       None,
+					       false);
+		   pexp_loc = Location.none } in
+	 let exploc = {txt = Longident.Lident ("::"); loc = Location.none} in 
+	 let exp3' = { pexp_desc = Pexp_construct (exploc,
+						   Some ({ pexp_desc = Pexp_tuple [exp3; mt]; 
+							   pexp_loc = Location.none }),
+						   false);
+		       pexp_loc = Location.none } in
+	 let exp' = { pexp_desc = Pexp_construct(exploc,
+						 Some ({ pexp_desc = Pexp_tuple [exp2; exp3']; 
+							 pexp_loc = Location.none }),
+						 false);
+		      pexp_loc = Location.none } in
+	let (lst_env, typ) = judge ((exp', cxt), env, prefix) in
+	let conf_list = search_conflict_env lst_env env vartyps' [] in
+	(match conf_list with
+	   [] -> 
+	   print_loc expr.pexp_loc;
+	   print_identified ();
+	   print_welltyped_expr t (* exp2, exp3 は同じ型と意図している -> 部分プログラムは意図通り *)
+	 | (((st, _), _, _), typ) ::rest -> 
+	    print_loc expr.pexp_loc;
+	    print_identified ();
+	    print_welltyped_if_then_else st typ rest (* exp2, exp3 を同じ型と意図していない *)
+	)
+       | (((st, _), _, _), typ) :: rest -> 
+	  print_loc exp1.pexp_loc;
+	  print_identified ();
+	  print_welltyped_if_bool st typ rest (* bool と意図されていない *)
+      )
+   | Parsetree.Pexp_match (exp, patexps) ->
+      (* TODO : exp と pattern が違っている場合がない *)
+      let dummy_match = make_pattern_match expr in (* expression を dummy にする *)
+   (* pattern が意図通りかを調べる *)
+      let (pat_env, typ) = judge((dummy_match, cxt), env, prefix) in
+      let conf_list = search_conflict_env pat_env env vartyps' [] in
+      (match conf_list with
+	 [] -> (* pattern は ok, expression が意図通りでない *)
+	 let (exp_env, typ) = judge((expr, cxt), env, prefix) in (* vartyps でいい気がする *)
+	 (* conf_list2 = vartyps' …? 以下の作業いらない…? *)
+	 let conf_list2 = search_conflict_env exp_env env vartyps' [] in
+	 (match conf_list2 with
+	    [] -> (* expression も意図通り -> 部分プログラムは意図通り *)
+	    print_loc expr.pexp_loc;
+	    print_identified ();
+	    print_welltyped_expr t
+	  | (((st, _), _, _), typ) :: rest -> 
+	     print_loc expr.pexp_loc;
+	     print_identified ();
+	     print_welltyped_match_expression st typ rest )
+       | (((st, _), _, _), typ) ::rest -> (* pattern が意図通りでない *)
+	  print_loc expr.pexp_loc;
+	  print_identified ();
+	  print_welltyped_match_pattern st typ rest )
+      
+   | _ ->
+  print_loc expr.pexp_loc;
+  print_identified ();
+  (match vartyps' with
+      [] -> (* 自由変数は意図通り *)
+	print_welltyped_expr t
+    | (((st, _), _, _), typ) :: [] -> (* 自由変数が意図通りでない *)
+	print_welltyped_env1 st typ
+    | (((st, _), _, _), typ) :: rest ->
+	print_welltyped_env_many st typ rest))
+
+(* upto : 'a list -> int -> 'a list *)
+let rec upto lst n = match lst with
+    [] -> []
+  | first :: rest -> if n = 0 then [] else first :: upto rest (n - 1)
+
+(* find_conflict_env : yes_no_list list -> yes_no_list -> yes_no_list *)
+(* 保留 *)
+let find_conflict_env env_lst yes = print_illtyped_if_fv ()
+  (* fprintf std_formatter "@[conflist env@]@." *)
+      
+(* find_conflict_patexp : Parsetree.match (expression * (pattern * expression) list) -> 
+   (pattern * expression) list * (pattern * expression) list *)
+let rec find_conflict_patexp mth cxt env prefix = match mth with
+    { pexp_desc = Pexp_match (exp', []) } -> ([], [])
+  | { pexp_desc = Pexp_match (exp', fst :: rst);
+      pexp_loc = loc } ->
+      let mrst =  { pexp_desc = Pexp_match (exp', rst);
+		    pexp_loc = Location.none } in
+      if is_well_typed_expr ((mrst, cxt), env, prefix) (* rst で型が付いた *)
+      then (fst :: [], rst)
+      else find_conflict_patexp mrst cxt env prefix
+  | _ ->  (fprintf std_formatter "find_conflict_exp"); 
+      raise DebuggerQuit
+
+(* lexps_to_ltyps : (label * expression) list -> (label * type) list *)
+let rec lexps_to_ltyps lexps cxt env prefix = match lexps with
+    [] -> []
+  | (l, exp) :: rst -> let (_, typ) = judge ((exp, cxt), env, prefix) in
+      (l, typ) :: (lexps_to_ltyps rst cxt env prefix)
+
+let rec elim_last_elem lst = match lst with
+    [] -> []
+  | [a] -> []
+  | fst :: rst -> fst :: (elim_last_elem rst)
+
+(* find_funtype_args : (label * typ) list -> int -> (int, typ) list *)
+(* int は 何番目の引数かを記憶 *)
+let rec find_funtype_args lst n = match lst with
+    [] -> []
+  | (_, typ') :: rst -> (match typ' with 
+			   {desc = typ} -> 
+			   (match typ with
+			      Tarrow (_, _, _, _) |
+			      Tlink ({desc = Tarrow (_, _, _, _)}) -> 
+			       (n, typ') :: (find_funtype_args rst (n + 1))
+			    | _ -> find_funtype_args rst (n + 1)))
+
+(* make_message_illtyped : expression context_t -> yes_no_list -> yes_no_list ->
+			   unit *)
+let make_message_illtyped ((expr, cxt), env, prefix) yes no =
+(*
+  print_loc expr.pexp_loc;
+  print_identified ();
+*)
+  (* print_answers no; *)
+  (match expr.pexp_desc with 
+| Parsetree.Pexp_ident (lloc) ->
+    print_loc expr.pexp_loc;
+    print_identified ();
+    print_illtyped_var_undefined ()
+| Parsetree.Pexp_ifthenelse (exp1, exp2, None) ->
+   (* TODO: try with *)
+    (* exp1 : bool annotation *)
+   let identloc = {txt = Longident.Lident("bool"); loc = Location.none} in
+   let exp1' = { pexp_desc = Pexp_constraint (exp1, Some({ ptyp_desc = Ptyp_constr (identloc, []);
+							   ptyp_loc = Location.none }), None); 
+		 pexp_loc = Location.none } in
+   (* exp2 : unit annotation *)
+   let identloc2 = {txt = Longident.Lident("unit"); loc = Location.none} in
+   let exp2' = { pexp_desc = Pexp_constraint (exp2, Some({ ptyp_desc = Ptyp_constr (identloc2, []);
+							    ptyp_loc = Location.none }), None); 
+		  pexp_loc = Location.none } in
+      (* if not is_well_typed_expr -> exp1, exp2 の型をjudgeして求めてエラーメッセージ *)
+      if not (is_well_typed_expr ((exp1', cxt), env, prefix)) then
+	let (_, typ1) = judge ((exp1, cxt), env, prefix) in
+	  (* ハイライトとメッセージ *)
+	  print_loc exp1.pexp_loc;
+	  print_identified ();
+	  print_illtyped_if_predicate typ1
+      else if not (is_well_typed_expr ((exp2', cxt), env, prefix)) then
+	(let (_, typ2) = judge ((exp2, cxt), env, prefix) in
+	  print_loc exp2.pexp_loc;
+	  print_identified ();
+	  print_illtyped_if_then typ2)
+      else (* both are well_typed *)
+	(* **** 使ってない
+	let (env1, _) = judge ((exp1', cxt), env, prefix) in
+	let (env2, _) = judge ((exp2', cxt), env, prefix) in 
+	*)
+	  (print_loc expr.pexp_loc;
+	  print_identified ();
+	  print_illtyped_if_fv ())
+	  (* find_conflict_env [env1; env2] yes *) (* coming soon *)
+	    (* cf. ask_env *)
+
+| Parsetree.Pexp_ifthenelse (exp1, exp2, Some (exp3)) ->
+   (* TODO: try with *)
+    (* exp1 に bool annotation を付ける *)
+   let identloc = {txt = Longident.Lident("bool"); loc = Location.none} in
+    let exp1' = { pexp_desc = Pexp_constraint (exp1, Some({ ptyp_desc = Ptyp_constr (identloc, []);
+							    ptyp_loc = Location.none }), None); 
+		  pexp_loc = Location.none } in
+      if not (is_well_typed_expr ((exp1', cxt), env, prefix))
+      then let (_, typ1) = judge ((exp1, cxt), env, prefix) in
+	print_loc exp1.pexp_loc;
+	print_identified ();
+	print_illtyped_if_predicate typ1
+	  (* [exp2; exp3] 同じリストに入れる *)
+      else 
+	let mtloc = {txt = Longident.Lident("[]"); loc = Location.none} in
+	let mt = { pexp_desc = Pexp_construct (mtloc,
+					       None,
+					       false);
+		   pexp_loc = Location.none } in
+	let exploc = {txt = Longident.Lident("::"); loc = Location.none} in
+	let exp3' = { pexp_desc = Pexp_construct (exploc,
+						  Some ({ pexp_desc = Pexp_tuple [exp3; mt]; 
+							  pexp_loc = Location.none }),
+						  false);
+		      pexp_loc = Location.none } in
+	let exp' = { pexp_desc = Pexp_construct(exploc,
+						Some ({ pexp_desc = Pexp_tuple [exp2; exp3']; 
+							pexp_loc = Location.none }),
+						false);
+		     pexp_loc = Location.none } in
+	  
+	  if not (is_well_typed_expr ((exp', cxt), env, prefix)) 
+	  then (let (_, typ2) = judge ((exp2, cxt), env, prefix) in
+	  let (_, typ3) = judge ((exp3, cxt), env, prefix) in
+	    print_loc expr.pexp_loc;
+	    print_identified ();
+	    print_illtyped_if_then_else typ2 typ3)
+	  else 
+	    (* let (env1, _) = judge ((exp1', cxt), env, prefix) in 
+	    let (env2, _) = judge ((exp', cxt), env, prefix) in *)
+	      (print_loc expr.pexp_loc;
+	      print_identified ();
+	      (fprintf std_formatter
+		      "@[bad else.@]@.");
+	      print_illtyped_if_fv ())
+
+| Parsetree.Pexp_apply (exp, lexps) ->
+    let rec make_message_apply n = (* TODO : occur check *)
+      (* ctype.ml の occur を使えるか *)
+      (* occur : env -> type -> type -> unit ?? *) 
+      if n > List.length lexps then
+	assert false
+      else
+	let args = upto lexps n in
+	let newexp = { pexp_desc = Parsetree.Pexp_apply (exp, args);
+		       pexp_loc = Location.none } in
+	  if is_well_typed_expr ((newexp, cxt), env, prefix) 
+	  then make_message_apply (n + 1)
+	  else (* print_illtyped_apply n *)
+	    (* exp, lexpsそれぞれ, ill type になる直前の全体の型を全て表示 *)
+	    (* exp が function ではないかもしれない *)
+	    let (_, exp_typ) = judge ((exp, cxt), env, prefix) in (* 関数の型 *)
+	    let ltyps = lexps_to_ltyps lexps cxt env prefix in (* 全ての引数の型のリスト *)
+	      (match args with
+		   [] -> (* 全ての引数が無事に渡された→ないはず *)
+		   (* 関数名を取り出す *)
+		   (match exp with
+		      {pexp_desc = Pexp_ident ({txt = Longident.Lident name})} -> (* name が関数名 *)
+		      print_loc expr.pexp_loc;
+		      print_identified ();
+		      print_illtyped_apply_funname n exp_typ ltyps exp_typ name
+		    | _ -> 
+		      print_loc expr.pexp_loc;
+		      print_identified ();
+		      print_illtyped_apply n exp_typ ltyps exp_typ )
+		 | ((_ :: _) as ill_well) -> let well = elim_last_elem ill_well in
+		     (* 一番最後の要素 : ill_typed の引数 *)
+		     let well_args = { pexp_desc = Parsetree.Pexp_apply (exp, well);
+				       pexp_loc = Location.none } in
+		       (* 型エラーになる直前までの型 *)
+		     let (_, well_typ') = judge ((well_args, cxt), env, prefix) in
+		     (* 次に要求される型を取り出す (int -> string だったら int) *)
+		     (match well_typ' with
+			{desc = typ} ->
+			(match typ with
+			   Tarrow (_, well_typ, _, _) (* 関数型は Tarrow と Tlink (Tarrow) とある *)
+			 | Tlink ({desc = Tarrow (_, well_typ, _, _)}) -> 
+			    (match exp with (* 関数名を取り出す *)
+			       {pexp_desc = Pexp_ident ({txt = Longident.Lident name})} -> (* name が関数名 *)
+			       (* language_level < 2 なら 高階関数 NG *)
+			       if language_level < 2 then (* 関数型になっている引数を探す *)
+				 let funtypes = find_funtype_args ltyps 1 in
+				 let (_, n_typ) = List.nth ltyps (n-1) in (* 型エラーの原因となっている引数の型 *)
+				 (match funtypes with
+				    [] -> (* 関数型になっている引数なし *)
+				    (print_loc expr.pexp_loc;
+				     print_identified ();
+				     print_illtyped_apply_beginning2 n name exp_typ n_typ)
+				  | _ -> 
+				     (print_loc expr.pexp_loc;
+				      print_identified ();
+				      print_illtyped_apply_beginning n name exp_typ ltyps funtypes ))
+			       else (* not beginning student *)
+				 (print_loc expr.pexp_loc;
+				  print_identified ();
+				  (* print_illtyped_apply_funname n exp_typ ltyps well_typ name) *)
+				  print_illtyped_apply n exp_typ ltyps well_typ)
+			     | _ -> (* exp が関数型でなかった -> ありえないはず *)
+		       		print_loc expr.pexp_loc;
+				print_identified ();
+				print_illtyped_apply n exp_typ ltyps well_typ)
+			 (* TODO : message を作る -> 関数と引数の型だけで大丈夫か *)
+			 | _ -> (* typ が関数型でなかった : 引数が多かった場合 *)
+			    (match exp with (* 関数名を取り出す *)
+			       {pexp_desc = Pexp_ident ({txt = Longident.Lident name})} -> 
+			       print_loc expr.pexp_loc;
+			       print_identified ();
+			       print_illtyped_too_much_args n exp_typ ltyps name
+			     | _ -> (* exp が関数型でなかった -> ありえないはず *)
+			fprintf std_formatter "no way!@."))
+		     ))
+    in
+    (* TODO : exp が関数型でなかったときの処理 *)
+    let (_, must_be_func) = judge ((exp, cxt), env, prefix) in
+    (match must_be_func.desc with
+       (* 関数型のとき *)
+       Tarrow (_, _, _, _) (* 関数型は Tarrow と Tlink (Tarrow) とある *)
+     | Tlink ({desc = Tarrow (_, _, _, _)}) -> 
+	make_message_apply 1
+     | _ -> (* 関数型でなかったとき *)
+
+	print_loc expr.pexp_loc;
+	print_identified ();
+	print_illtyped_apply_not_function must_be_func)
+
+| Parsetree.Pexp_function (lbl, exp_op, patexps) ->
+    print_illtyped_function ()
+| Parsetree.Pexp_match (exp, patexps) -> (* match *)
+   (*print_illtyped_match () *)
+
+    let mth = { pexp_desc = Pexp_match (exp, (List.rev patexps)); 
+		pexp_loc = expr.pexp_loc } in
+    let patmth = make_pattern_match mth in (* expression を dummy にする *)
+      if not (is_well_typed_expr ((patmth, cxt), env, prefix)) then (* pattern のどこかに原因がある *)
+	let (ill_patexp, well_patexps) = find_conflict_patexp patmth cxt env prefix in
+	  (match well_patexps with
+	       []  -> (* exp と pattern の型が合わないとき *)
+		 (match patmth with
+		      { pexp_desc = Pexp_match (_, (fst :: rst)) } ->
+			  let patlst = [fst] in
+			  let pat' = { pexp_desc = Pexp_function ("pat'", None, patlst); 
+				       pexp_loc = Location.none } in
+			  let (_, exp_typ) = judge ((exp, cxt), env, prefix) in
+			  let (_, pat_typ') = judge ((pat', cxt), env, prefix) in
+			    (* **** 型を取り出す *)
+			    (match pat_typ' with
+				 ({desc = Tlink ({desc = Tarrow (_, pat_typ, _, _)})}) ->
+				   (print_loc expr.pexp_loc;
+				   print_identified ();
+				   print_illtyped_match_exp exp_typ pat_typ)
+			       | _ -> fprintf std_formatter "@[pat_typ' is not Tlink@]@." )
+		      | _ -> fprintf std_formatter "patmth is not Pexp_math")
+		   
+	     | _ :: _ ->
+		 let well_mth = { pexp_desc = Pexp_function ("well_match", None, well_patexps); 
+				  pexp_loc = Location.none } in
+		 let ill_mth = { pexp_desc = Pexp_function ("ill_match", None, ill_patexp); 
+				 pexp_loc = Location.none } in 
+		 let (_, lst_typ') = judge ((well_mth, cxt), env, prefix) in
+		 let (_, exp_typ') = judge ((ill_mth, cxt), env, prefix) in 
+		   (* **** 型を取り出す *)
+		   (match (lst_typ', exp_typ') with
+			({desc = Tlink ({desc = Tarrow (_, lst_typ, _, _)})},
+			 {desc = Tlink ({desc = Tarrow (_, exp_typ, _, _)})}) ->
+			(print_loc (fst (List.hd (ill_patexp))).ppat_loc;
+			 print_identified ();
+			 print_illtyped_match_left exp_typ lst_typ)
+		      | _ -> fprintf std_formatter "@[lst_typ' is not Tlink@]@." ) )
+      else (* pattern は型が付いた *)
+	   let (ill_patexp2, well_patexps2) = 
+	     (try
+		find_conflict_patexp mth cxt env prefix
+	      with DebuggerQuit -> ([], [])) (* とりあえず *)
+	   in
+	  (match well_patexps2 with
+	       [] -> (* とりあえず env_conflict *)
+		 (print_loc expr.pexp_loc;
+		 print_identified ();
+		 print_illtyped_match_fv ())
+	     | _ :: _ -> 
+		 let well_mth2 = { pexp_desc = Pexp_match (exp, well_patexps2); 
+				   pexp_loc = Location.none } in
+		 let ill_mth2 = { pexp_desc = Pexp_match (exp, ill_patexp2); 
+				  pexp_loc = Location.none } in
+		   (try
+		      let (_, lst_typ2) = judge ((well_mth2, cxt), env, prefix) in
+		      let (_, exp_typ2) = judge ((ill_mth2, cxt), env, prefix) in
+			(print_loc (snd (List.hd (ill_patexp2))).pexp_loc;
+			print_identified ();
+			print_illtyped_match_right exp_typ2 lst_typ2 )
+		    with Assert_failure (_) -> fprintf std_formatter "judge"))
+	  
+  
+| Parsetree.Pexp_construct(l, Some (exp), b) ->
+   (* Location があるはずなのでもっと拡張できそう *)
+    print_loc expr.pexp_loc;
+    print_identified ();
+    print_illtyped_constructor ()
+| _ -> (* illtyped *)
+    print_loc expr.pexp_loc;
+    print_identified ();
+    print_illtyped_other ())
+
+(* expr_of_structure : structure_item -> expression * expr_context *)
+let expr_of_structure structure_item = match structure_item with
+  | { pstr_desc = Pstr_eval (expr) } ->
+      (expr, Empty)
+  | { pstr_desc = Pstr_value (flg, patexps); pstr_loc = loc } ->
+      (* in なしの let 文 *)
+      ({ pexp_desc = Pexp_let (flg, patexps, dummy_int0);
+         pexp_loc = loc }, Empty)
+  | _ -> assert false
+
+(* illtyped_exp : structure -> Env.t -> str_context -> expression context_t *)
+(* structure has to be ill-typed. *)
+let rec illtyped_expr structure env lst = match structure with
+    [] -> failwith "TypeDebugger: Error: structure is well typed."
+  | s :: rest -> try
+      let (_, _, env') = Typemod.type_structure env [s] Location.none in
+      illtyped_expr rest env' ((s, env) :: lst)
+    with Typecore.Error (_, _, Typecore.Expr_type_clash (_))
+       | Typecore.Error (_, _, Typecore.Pattern_type_clash (_))
+       | _ (* Unbound value *)
+       -> (expr_of_structure s, env, lst)	  
+
+(* walk_right_typed_fv :
+	expression context_t list -> yes_no_list -> yes_no_list ->
+	expression context_t option * yes_no_list * yes_no_list *)
+let rec walk_right_typed_fv progs yes no = match progs with
+    [] -> (None, yes, no) (* all the free variables are as intended *)
+  | ((expr, cxt), env, prefix) :: rest ->
+      let (vartyps, typ) = judge ((expr, cxt), env, prefix) in
+      let (intended, yes', no') = ask_env expr vartyps env yes no in
+      if intended then walk_right_typed_fv rest yes' no'
+      else (Some ((expr, cxt), env, prefix), yes', no')
+
+(* walk_right_typed :
+	expression context_t list -> yes_no_list -> yes_no_list ->
+	expression context_t option * yes_no_list * yes_no_list *)
+let rec walk_right_typed progs yes no = match progs with
+    [] -> (* All the premises are as intended. *)
+	  (* The current expr is the source of the type error. *)
+      (None, yes, no)
+  | ((expr', cxt'), env', prefix') :: rest ->
+      let (intended, yes', no') =
+	has_intended_type ((expr', cxt'), env', prefix')  yes no in
+      if intended
+      then walk_right_typed rest yes' no'
+      else (Some ((expr', cxt'), env', prefix'), yes', no')
+
+(* walk_up_typed_fv : expression context_t -> yes_no_list -> yes_no_list ->
+		      unit *)
+let rec walk_up_typed_fv ((expr, cxt), env, prefix) yes no =
+  (* ((expr, cxt), env, prefix) は well-typed *)
+  let progs = decompose_expr ((expr, cxt), env, prefix) Typed_fv in
+  let (c, yes', no') = walk_right_typed_fv progs yes no in
+  match c with
+      None ->
+	(* 部分式の fv は意図通り *)
+	(* それらを合わせたら、自由変数が衝突した *)
+	walk_up_typed ((expr, cxt), env, prefix) yes' no'
+    | Some ((expr', cxt'), env', prefix') ->
+	(* 部分式の fv が意図に合わない *)
+	walk_up_typed_fv ((expr', cxt'), env', prefix') yes' no'
+
+(* walk_up_typed : expression context_t -> yes_no_list -> yes_no_list -> unit *)
+and walk_up_typed ((expr, cxt), env, prefix) yes no =
+  (* ((expr, cxt), env, prefix) は well-typed *)
+  match expr.pexp_desc with
+     Parsetree.Pexp_let (_, _, _) -> (* let pats = exps in exp 文のみ特別扱い *)
+       let progs = decompose_expr ((expr, cxt), env, prefix) Illtyped in
+       let (c, yes', no') = walk_right_typed_fv progs yes no in
+			    (* exps の fv をチェック *)
+       (match c with
+	   None ->
+	     (* exps の fv は意図通り *)
+	     let progs' = decompose_expr ((expr, cxt), env, prefix) Typed in
+	     let (c', yes'', no'') = walk_right_typed progs' yes' no' in
+				     (* exp をチェック *)
+	     (match c' with
+		 None ->
+		   (* exp の型も意図通り *)
+		   (* この let 文がエラーの原因 *)
+		   (* もともと well-typed なので、この場合は起こらないはず *)
+		   assert false
+	       | Some ((expr'', cxt''), env'', prefix'') ->
+		   (* exp の型が意図に合わない *)
+		   walk_up_typed ((expr'', cxt''), env'', prefix'') yes'' no'')
+	 | Some ((expr', cxt'), env', prefix') ->
+	     (* exps の fv が意図に合わない *)
+	     walk_up_typed_fv ((expr', cxt'), env', prefix') yes' no')
+   | _ -> (* let 文以外の場合 *)
+       let progs = decompose_expr ((expr, cxt), env, prefix) Typed in
+       let (c, yes', no') = walk_right_typed progs yes no in
+       (match c with
+	   None ->
+	     (* 部分式の型は意図通り *)
+	     make_message_welltyped ((expr, cxt), env, prefix) no'
+	 | Some ((expr', cxt'), env', prefix') ->
+	     (* 部分式の型が意図に合わない *)
+	     walk_up_typed ((expr', cxt'), env', prefix') yes' no')
+
+(* walk_right_illtyped :
+	expression context_t list -> yes_no_list -> yes_no_list ->
+	expression context_t option * yes_no_list * yes_no_list *)
+let rec walk_right_illtyped progs yes no = match progs with
+    [] -> (* all the decomposed programs are well typed *)
+      (None, yes, no)
+  | ((expr', cxt'), env', prefix') :: rest ->
+      if is_well_typed_expr ((expr', cxt'), env', prefix')
+      then walk_right_illtyped rest yes no
+      else (Some ((expr', cxt'), env', prefix'), yes, no)
+
+(* walk_up_illtyped : expression context_t -> yes_no_list -> yes_no_list ->
+		      unit *)
+let rec walk_up_illtyped ((expr, cxt), env, prefix) yes no =
+  let progs = decompose_expr ((expr, cxt), env, prefix) Illtyped in
+  let (c, yes', no') = walk_right_illtyped progs yes no in
+  (match c with
+      None ->
+	start_typed ((expr, cxt), env, prefix) yes' no'
+    | Some ((expr', cxt'), env', prefix') ->
+	walk_up_illtyped ((expr', cxt'), env', prefix') yes' no')
+and start_typed ((expr, cxt), env, prefix) yes no =
+  match expr.pexp_desc with
+  Parsetree.Pexp_let (rec_flg, patexps, exp) ->
+    (* let pats = exps in exp を特別扱い *)
+    (* exps に型はついている（意図通りとは限らない）*)
+    let progs = decompose_expr ((expr, cxt), env, prefix) Illtyped in
+    let (c, yes', no') = walk_right_typed_fv progs yes no in
+			 (* exps の fv をチェック *)
+    (match c with
+	None ->
+	  (* exps の fv は意図通り *)
+	  if is_well_typed_expr
+		(({ pexp_desc =
+		      Parsetree.Pexp_let (rec_flg, patexps, dummy_int0);
+		    pexp_loc  = Location.none; },
+		  cxt), env, prefix)
+	  then (* pats = exps には型がつく。exp に型がつかない *)
+	       walk_up_illtyped
+		 ((exp, Let (rec_flg, patexps, cxt)), env, prefix) yes' no'
+	  else if rec_flg = Recursive then (* 再帰が原因 *)
+	    make_message_recursive patexps progs
+	  else (* パターン pats = exps が型エラーの原因 *)
+	    make_message_patexps ((patexps, cxt), env, prefix)
+      | Some ((expr', cxt'), env', prefix') ->
+	  (* exps の fv が意図に合わない *)
+	  walk_up_typed_fv ((expr', cxt'), env', prefix') yes' no')
+| _ ->
+    (* それ以外の式 *)
+    let progs = decompose_expr ((expr, cxt), env, prefix) Illtyped in
+    let (c, yes', no') = walk_right_typed progs yes no in
+    (match c with
+       None ->
+	 (* 部分式の型は意図通り *)
+	 make_message_illtyped ((expr, cxt), env, prefix) yes' no'
+     | Some ((expr', cxt'), env', prefix') ->
+	 (* 部分式の型が意図に合わない *)
+	 walk_up_typed ((expr', cxt'), env', prefix') yes' no')
+
+(* algo : toplevel_phrase -> Env.t -> unit *)
+let algo phr toplevel_env =
+  print_initial_message ();
+  match phr with
+    Ptop_dir (_, _) -> assert false
+  | Ptop_def (structure) ->
+      let ((expr, cxt), env, prefix) =
+        illtyped_expr structure toplevel_env [] in
+      try
+        walk_up_illtyped ((expr, cxt), env, prefix) [] []
+      with DebuggerQuit -> ()
+
+let rec loop structures acc = match structures with
+    [] -> acc
+  | structure :: rest -> loop rest (structure @ acc)
+
+(* algo2 : toplevel_phrase -> structure list -> unit *)
+let algo2 phr rev_structures toplevel_env =
+  print_initial_message ();
+  match phr with
+    Ptop_dir (_, _) -> assert false
+  | Ptop_def (structure) ->
+      let structure = loop (structure :: rev_structures) [] in
+      let ((expr, cxt), env, prefix) =
+        illtyped_expr structure toplevel_env [] in
+      try
+        walk_up_illtyped ((expr, cxt), env, prefix) [] []
+      with DebuggerQuit -> ()
+
+end (***** end of module *)
+
+let algo phr toplevel_env = A.algo phr toplevel_env
+
+let algo2 structure rev_structures toplevel_env =
+  A.algo2 structure rev_structures toplevel_env 
diff -urN ocaml-4.01.0-org/typing/debug_message.ml ocaml-4.01.0/typing/debug_message.ml
--- ocaml-4.01.0-org/typing/debug_message.ml	1970-01-01 09:00:00.000000000 +0900
+++ ocaml-4.01.0/typing/debug_message.ml	2014-09-30 18:46:00.000000000 +0900
@@ -0,0 +1,540 @@
+(*
+open Misc
+open Longident
+open Path
+open Asttypes
+
+open Types
+open Typedtree
+open Ctype
+
+open Parsetree
+ *)
+
+open Format
+
+type language_t = English | Japanese
+
+let language = try
+  let lang = Sys.getenv "LANG" in
+  if (String.sub lang 0 (min 5 (String.length lang)) = "ja_JP") ||  (String.sub lang 0 (min 5 (String.length lang)) = "en_US.ISO8859-1")
+  then Japanese
+  else English
+with Not_found -> English
+
+let print_loc loc = 
+  Location.print std_formatter loc;;
+
+let print_initial_message () =
+  match language with
+| English -> fprintf std_formatter
+    "The above type error was raised.  Type debugger started.@.@."
+| Japanese -> fprintf std_formatter
+    "上記の型エラーが起こりました。デバッガを起動します。@.@."
+
+let print_prompt () =
+  fprintf std_formatter "(y/n/q) > ";
+  print_flush ()
+
+let print_ask_env st typ =
+  Printtyp.reset_and_mark_loops typ;
+  match language with
+| English -> fprintf std_formatter
+    "@[In this scope, do you use '%s' as type:@ %a ?@]@."
+    st Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[ハイライトされた部分のスコープで@, %s を@ %a@ 型だと意図していますか？@]@."
+    st Printtyp.type_expr typ
+
+let print_ask_expr typ =
+  Printtyp.reset_and_mark_loops typ;
+  match language with
+| English -> fprintf std_formatter
+    "@[Do you use this expression as type:@ %a ?@]@."
+    Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[ハイライトされた部分の型を、@ %a@ だと意図していますか？@]@."
+    Printtyp.type_expr typ
+
+let print_identified () =
+  match language with
+| English -> fprintf std_formatter
+    "The source of the type error is highlighted.@."
+| Japanese -> fprintf std_formatter
+    "ハイライトされた部分に特定されました。@."
+
+let print_recursive typ st typ' =
+  Printtyp.reset_and_mark_loops typ;
+  Printtyp.reset_and_mark_loops typ';
+  match language with
+| English -> fprintf std_formatter
+    "@[Error1 : This expression has type@ %a,@ but '%s' is used at type@ %a in the recursive call.@]@."
+    Printtyp.type_expr typ st Printtyp.type_expr typ'
+| Japanese -> fprintf std_formatter
+    "@[Error1 : この式は@ %a@ 型ですが、再帰呼び出しで@ %s@ を@ %a@ 型として使っています。@]@."
+    Printtyp.type_expr typ st Printtyp.type_expr typ'
+
+let print_patexps typ =
+  Printtyp.reset_and_mark_loops typ;
+  match language with
+| English -> fprintf std_formatter
+    "@[Error2 : This expression has type:@ %a,@ but it conflicts with the type of the pattern.@]@."
+    Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[Error2 : この式は@ %a@ 型で、@,期待されるパターンの型と合いません。@]@."
+    Printtyp.type_expr typ
+
+let print_patexps2 () =
+ (* Printtyp.reset_and_mark_loops pattyp;*)
+  match language with
+| English -> fprintf std_formatter
+    "@[Error3 : This expression has constant type, but it conflicts with the type of the pattern.@]@."
+| Japanese -> fprintf std_formatter
+    "@[Error3 : この式は定数になっていますが、let 文で束縛する式は変数もしくはパターンでなければなりません。@]@."
+
+let print_welltyped_expr typ =
+  Printtyp.reset_and_mark_loops typ;
+  match language with
+| English -> fprintf std_formatter
+    "@[Error4 : This expression has type@ %a.@]@."
+    Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[Error4 : この式の型は@ %a@ 型です。@]@."
+    Printtyp.type_expr typ
+
+let print_welltyped_env1 st typ =
+  Printtyp.reset_and_mark_loops typ;
+  match language with
+| English -> fprintf std_formatter
+    "@[Error5 : The variable '%s' needs be replaced with an expression of type:@ %a.@]@."
+    st Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[Error5 : 変数 %s は@ %a@ 型になっています。@]@."
+    st Printtyp.type_expr typ
+
+let print_welltyped_env_many st typ rest =
+  Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English ->
+    fprintf std_formatter
+      "Error6 : Expressions at the following variables need the following types:@.  @["
+| Japanese ->
+    fprintf std_formatter
+      "Error6 : 次の変数は示される型になっています。@.  @[");
+  fprintf std_formatter
+    "%s : %a" st Printtyp.type_expr typ;
+  List.iter (fun (((st, _), _, _), typ) ->
+	      (* Printtyp.reset_and_mark_loops typ; *)
+	      fprintf std_formatter
+		",@ %s : %a" st Printtyp.type_expr typ)
+	    rest;
+  fprintf std_formatter "@]@."
+
+let print_welltyped_if_bool st typ rest =
+    Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English ->
+    fprintf std_formatter
+      "Error7 : Expressions at the following variables need the following types.@. The predicate of a conditional expression needs to have type bool.@.  @["
+| Japanese ->
+    fprintf std_formatter
+      "Error7 : 次の変数が示される型になっています。@. if 文の条件部は bool 型でなければなりません。@.  @[");
+  fprintf std_formatter
+    "%s : %a" st Printtyp.type_expr typ;
+  List.iter (fun (((st, _), _, _), typ) ->
+	      (* Printtyp.reset_and_mark_loops typ; *)
+	      fprintf std_formatter
+		",@ %s : %a" st Printtyp.type_expr typ)
+	    rest;
+  fprintf std_formatter "@]@."
+
+let print_welltyped_if_unit st typ rest =
+    Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English ->
+    fprintf std_formatter
+      "Error8 : Expressions at the following variables need the following types.@. Since the conditional expression does not have else branch,@, then branch needs to have type unit.@. (or you might forgot else branch)@.  @["
+| Japanese ->
+    fprintf std_formatter
+      "Error8 : 次の変数が示される型になっています。@. else 部分がないため if 文の then 部分は unit 型でなければなりません。@. （もしくは else 部分を忘れていませんか？）@.  @[");
+  fprintf std_formatter
+    "%s : %a" st Printtyp.type_expr typ;
+  List.iter (fun (((st, _), _, _), typ) ->
+	      (* Printtyp.reset_and_mark_loops typ; *)
+	      fprintf std_formatter
+		",@ %s : %a" st Printtyp.type_expr typ)
+	    rest;
+  fprintf std_formatter "@]@."
+
+let print_welltyped_if_then_else st typ rest =
+    Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English ->
+    fprintf std_formatter
+      "Error8 : Expressions at the following variables need the following types.@. Then branch and else branch of a conditional expression need to be the same type.@.  @["
+| Japanese ->
+    fprintf std_formatter
+      "Error9 : 次の変数が示される型になっています。@. if 文の then 部分と else 部分は同じ型でなければなりません。@.  @[");
+  fprintf std_formatter
+    "%s : %a" st Printtyp.type_expr typ;
+  List.iter (fun (((st, _), _, _), typ) ->
+	      (* Printtyp.reset_and_mark_loops typ; *)
+	      fprintf std_formatter
+		",@ %s : %a" st Printtyp.type_expr typ)
+	    rest;
+  fprintf std_formatter "@]@."
+
+(* TODO : English messages *)
+let print_welltyped_match_pattern st typ rest =
+    Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English ->
+    fprintf std_formatter
+      "Error10 : Expressions at the following variables need the following types:@.  @["
+| Japanese ->
+    fprintf std_formatter
+      "Error10 : 次の変数が示される型になっています。@. match 文の矢印の左側は同じ型でなければなりません。@.  @[");
+  fprintf std_formatter
+    "%s : %a" st Printtyp.type_expr typ;
+  List.iter (fun (((st, _), _, _), typ) ->
+	      (* Printtyp.reset_and_mark_loops typ; *)
+	      fprintf std_formatter
+		",@ %s : %a" st Printtyp.type_expr typ)
+	    rest;
+  fprintf std_formatter "@]@."
+
+let print_welltyped_match_expression st typ rest =
+    Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English ->
+    fprintf std_formatter
+      "Expressions at the following variables need the following types:@.  @["
+| Japanese ->
+    fprintf std_formatter
+      "Error11 : 次の変数が示される型になっています。@. match 文の矢印の右側は同じ型でなければなりません。@.  @[");
+  fprintf std_formatter
+    "%s : %a" st Printtyp.type_expr typ;
+  List.iter (fun (((st, _), _, _), typ) ->
+	      (* Printtyp.reset_and_mark_loops typ; *)
+	      fprintf std_formatter
+		",@ %s : %a" st Printtyp.type_expr typ)
+	    rest;
+  fprintf std_formatter "@]@."
+
+let print_illtyped_var_undefined () =
+  match language with
+| English -> fprintf std_formatter
+    "This variable is undefined.@."
+| Japanese -> fprintf std_formatter
+    "Error29 : この変数は未定義です。@."
+
+let print_illtyped_if_predicate typ =
+  Printtyp.reset_and_mark_loops typ;
+  match language with
+| English -> fprintf std_formatter
+    "@[The type of the predicate part is:@ %a,@ but it has to be bool.]@."
+    Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[Error12 : 条件部分の型は@ %a@ ですが bool 型でなくてはなりません。@]@."
+    Printtyp.type_expr typ
+
+let print_illtyped_if_then typ =
+  Printtyp.reset_and_mark_loops typ;
+ (match language with
+| English -> fprintf std_formatter
+    "@[The type of the then branch is:@ %a,@ but it has to be unit.]@."
+    Printtyp.type_expr typ
+| Japanese -> fprintf std_formatter
+    "@[Error13 : then 部分が @ %a @ 型になっていますが else 部分がないため unit 型でなくてはなりません。@]@."
+    Printtyp.type_expr typ);
+ (match language with
+| English -> fprintf std_formatter
+    "(Or, you forgot the else branch perhaps?)@."
+| Japanese -> fprintf std_formatter
+    "（もしくは else 部分を書き忘れていませんか？）@.")
+
+let print_illtyped_if_fv () =
+  match language with
+| English -> fprintf std_formatter
+    "Some variables are used at different types.@."
+| Japanese -> fprintf std_formatter
+    "Error14 : 同じ変数が別の場所で別の型として使われています。@."
+
+let print_illtyped_if_then_else typ2 typ3 =
+  Printtyp.reset_and_mark_loops typ2;
+  Printtyp.reset_and_mark_loops typ3;
+  match language with
+| English -> fprintf std_formatter
+    "@[The types of the then and else branches are:@ %a@ and@ %a,@ but they have to be the same.@]@."
+    Printtyp.type_expr typ2 Printtyp.type_expr typ3
+| Japanese -> fprintf std_formatter
+    "@[Error15 : then 部分が@ %a@ 型で else 部分が@ %a@ 型になっていますが、@,これらは同じ型でなくてはなりません。@]@."
+    Printtyp.type_expr typ2 Printtyp.type_expr typ3
+
+let rec print_illtyped_apply_args ltyps n = 
+  match language with
+    English ->
+    (match ltyps with
+       [] -> fprintf std_formatter ""
+     | (name, typ) :: rst -> let len = n - (List.length rst) in
+			     (match len with
+				1 -> (fprintf std_formatter
+					      "@[ 1st argument : @ %a@ @]@." Printtyp.type_expr typ);
+				     print_illtyped_apply_args rst n
+			      | 2 -> (fprintf std_formatter
+					      "@[ 2nd argument : @ %a@ @]@." Printtyp.type_expr typ);
+				     print_illtyped_apply_args rst n
+			      | 3 -> (fprintf std_formatter
+					      "@[ 3rd argument : @ %a@ @]@." Printtyp.type_expr typ);
+				     print_illtyped_apply_args rst n
+			      | n -> (fprintf std_formatter
+					      "@[ %dth argument : @ %a@ @]@." n Printtyp.type_expr typ);
+				     print_illtyped_apply_args rst n))
+
+  | Japanese ->
+     (match ltyps with
+       [] -> fprintf std_formatter ""
+     | (name, typ) :: rst -> let len = n - (List.length rst) in
+			     (fprintf std_formatter
+				      "@[ %d 番目の引数の型：@ %a@ @]@." len Printtyp.type_expr typ);
+			     print_illtyped_apply_args rst n)
+
+(* 関数名なし *)
+let print_illtyped_apply n exp_typ ltyps well_typ =
+  match language with
+| English -> (* fprintf std_formatter
+    "The type conflict occurs at the "; *)
+   (match n with
+       1 -> fprintf std_formatter "The 1st argument of this application causes a type error.@."
+     | 2 -> fprintf std_formatter "The 2nd argument of this application causes a type error.@."
+     | 3 -> fprintf std_formatter "The 3rd argument of this application causes a type error.@."
+     | n -> fprintf std_formatter "The %dth argument of this application causes a type error.@." n)
+| Japanese -> let len = List.length ltyps in
+    (fprintf std_formatter
+       "Error16 : この関数呼び出しの %d 番目の引数で型が合いません。@,関数、引数、%d 番目の引数に要求される型は以下の通りです。@."
+		 n n);
+    (fprintf std_formatter
+       "@[関数部分：@ %a@ @]@."
+       Printtyp.type_expr exp_typ);
+    (print_illtyped_apply_args ltyps len);
+    (fprintf std_formatter
+       "@[ %d 番目の引数に要求される型：@ %a@.@]"
+       n Printtyp.type_expr well_typ)
+
+(* 関数名あり *)
+let print_illtyped_apply_funname n exp_typ ltyps well_typ name =
+  match language with
+| English -> let len = List.length ltyps in
+   fprintf std_formatter
+    "The type conflict occurs at the ";
+   (match n with
+       1 -> fprintf std_formatter "1st argument.@. The types of the function, the arguments, and the type required to the 1st argument are:@."
+     | 2 -> fprintf std_formatter "2nd argument.@. The types of the function, the arguments, and the type required to the 2nd argument are:@."
+     | 3 -> fprintf std_formatter "3rd argument.@. The types of the function, the arguments, and the type required to the 3rd argument are:@."
+     | n -> fprintf std_formatter "%dth argument.@. The types of the function, the arguments, and the type required to the %dth argument are:@." n n);
+   (fprintf std_formatter
+       "@[Function(";
+     print_string name;
+     fprintf std_formatter
+	     ") : @ %a@ @]@."
+       Printtyp.type_expr exp_typ);
+    (print_illtyped_apply_args ltyps len);
+    (match n with
+       1 -> (fprintf std_formatter
+		    "@[ Required to the 1st argument : @ %a@.@]"
+		    Printtyp.type_expr well_typ)
+     | 2 -> (fprintf std_formatter
+		    "@[ Required to the 2nd argument : @ %a@.@]"
+		    Printtyp.type_expr well_typ)
+     | 3 -> (fprintf std_formatter
+		    "@[ Required to the 3rd argument : @ %a@.@]"
+		    Printtyp.type_expr well_typ)
+     | n -> (fprintf std_formatter
+		    "@[ Required to the %dth argument : @ %a@.@]"
+		    n Printtyp.type_expr well_typ))
+
+| Japanese -> let len = List.length ltyps in
+    (fprintf std_formatter
+       "Error17 : この関数呼び出しの %d 番目の引数で型が合いません。@,関数、引数、%d 番目の引数に要求される型は以下の通りです。@."
+		 n n);
+    (fprintf std_formatter
+       "@[関数(";
+     print_string name;
+     fprintf std_formatter
+	     ")部分：@ %a@ @]@."
+       Printtyp.type_expr exp_typ);
+    (print_illtyped_apply_args ltyps len);
+    (fprintf std_formatter
+       "@[ %d 番目の引数に要求される型：@ %a@.@]"
+       n Printtyp.type_expr well_typ)
+
+let rec print_funtypes n funtypes = 
+(match language with
+  English -> 
+  (match funtypes with
+     [] -> (fprintf std_formatter 
+		    "@[(some arguments might be missing.)@]@.") 
+   | (m, typ) :: rst ->
+      (match m with
+	 1 -> (fprintf std_formatter
+		       "@[1st argument : @ %a@ @]@." Printtyp.type_expr typ); print_funtypes n rst
+       | 2 -> (fprintf std_formatter
+		       "@[2nd argument : @ %a@ @]@." Printtyp.type_expr typ); print_funtypes n rst
+       | 3 -> (fprintf std_formatter
+		       "@[3rd argument : @ %a@ @]@." Printtyp.type_expr typ); print_funtypes n rst
+       | n -> (fprintf std_formatter
+		       "@[ %dth argument : @ %a@]@." m Printtyp.type_expr typ); print_funtypes n rst))
+
+| Japanese ->
+  (match funtypes with
+    [] -> (fprintf std_formatter 
+		   "@[これらに引数を渡すのを忘れていませんか？@]@.") 
+  | (m, typ) :: rst ->
+     (fprintf std_formatter
+	      "@[ %d 番目の引数の型：@ %a@ @]@."
+	      m Printtyp.type_expr typ);
+     print_funtypes n rst))
+
+let print_illtyped_apply_beginning n name exp_typ ltyps funtype_args =
+  (match language with
+  | English -> let len = List.length ltyps in
+     fprintf std_formatter
+		       "The type conflict occurs at the ";
+	       (match n with
+		  1 -> fprintf std_formatter "1st argument.@."
+		| 2 -> fprintf std_formatter "2nd argument.@."
+		| 3 -> fprintf std_formatter "3rd argument.@."
+		| n -> fprintf std_formatter "%dth argument.@." n);
+	       (fprintf std_formatter
+			"@[Function(";
+		print_string name;
+		fprintf std_formatter
+			")@ %a@ @]@."
+			Printtyp.type_expr exp_typ);
+	       (print_illtyped_apply_args ltyps len);
+	       (fprintf std_formatter "@[The following arguments have function type.@]@.";
+		print_funtypes n funtype_args)
+	       		 
+  | Japanese -> let len = List.length ltyps in
+     (fprintf std_formatter
+	      "Error18 : この関数呼び出しの %d 番目の引数で型が合いません。@."
+	      n );
+     (fprintf std_formatter
+	      "@[関数(";
+      print_string name;
+      fprintf std_formatter
+	      ")部分の型：@ %a@ @]@."
+	      Printtyp.type_expr exp_typ);
+     (print_illtyped_apply_args ltyps len);
+     (fprintf std_formatter "@[以下の引数が関数型になっています。@]@.";
+      print_funtypes n funtype_args))
+
+(* 関数型になっている引数がないとき *)
+let print_illtyped_apply_beginning2 n name exp_typ n_typ =
+  match language with
+  | English -> fprintf std_formatter
+		       "The type conflict occurs at the ";
+	       (match n with
+		  1 -> fprintf std_formatter "1st argument.@."
+		| 2 -> fprintf std_formatter "2nd argument.@."
+		| 3 -> fprintf std_formatter "3rd argument.@."
+		| n -> fprintf std_formatter "%dth argument.@." n)
+  | Japanese -> 
+     (fprintf std_formatter
+	      "Error19 : この関数呼び出しの %d 番目の引数で型が合いません。@."
+	      n );
+     (fprintf std_formatter
+	      "@[関数(";
+      print_string name;
+      fprintf std_formatter
+	      ")部分の型：@ %a@ @]@."
+	      Printtyp.type_expr exp_typ);
+     (fprintf std_formatter
+	      "@[ %d 番目の引数の型：@ %a@.@]@."
+     n Printtyp.type_expr n_typ)
+
+let print_illtyped_function () =
+  match language with
+| English -> fprintf std_formatter
+    "The pattern forces some variable an unintended type.@."
+| Japanese -> fprintf std_formatter
+    "Error20 : パターンによって変数の型が意図しないものに強制されています。@."
+
+let print_illtyped_match () =
+  match language with
+| English -> fprintf std_formatter
+    "Somewhere in this match expression is wrong.@."
+| Japanese -> fprintf std_formatter
+    "この match 文のどこかがおかしいです。@."
+
+let print_illtyped_match_exp typ1 typ2 =
+    match language with
+| English -> fprintf std_formatter
+    "Somewhere in this match expression is wrong.@." (* 英語 *)
+| Japanese -> fprintf std_formatter
+    "@[Error21 :  match する式が@ %a@ 型でパターンが@ %a@ 型になっていますが、@,これらは同じ型でなくてはなりません。@]@."
+      Printtyp.type_expr typ1 Printtyp.type_expr typ2
+
+let print_illtyped_match_left typ1 typ2 =
+  match language with
+| English -> fprintf std_formatter
+    "Somewhere in this match expression is wrong.@." (* 英語 *)
+| Japanese -> fprintf std_formatter
+    "@[Error22 : ハイライト部分が@ %a@ 型でそれ以前までの矢印の左側が@ %a@ 型になっていますが、@,これらは同じ型でなくてはなりません。@]@."
+      Printtyp.type_expr typ1 Printtyp.type_expr typ2
+
+let print_illtyped_match_right typ1 typ2 =
+  match language with
+| English -> fprintf std_formatter
+    "Somewhere in this match expression is wrong.@." (* 英語 *)
+| Japanese -> fprintf std_formatter
+    "@[Error23 : ハイライト部分が@ %a@ 型でそれ以前までの矢印の右側が@ %a@ 型になっていますが、@,これらは同じ型でなくてはなりません。@]@."
+      Printtyp.type_expr typ1 Printtyp.type_expr typ2
+
+let print_illtyped_match_fv () =
+  match language with
+| English -> fprintf std_formatter
+    "Some variables are used at different types.@."
+| Japanese -> fprintf std_formatter
+    "Error24 : 同じ変数が別の場所で別の型として使われています。@."
+   
+let print_illtyped_constructor () =
+  match language with
+| English -> fprintf std_formatter
+    "The constructor is given a wrong type of argument(s).@."
+| Japanese -> fprintf std_formatter
+    "Error25 : コンストラクタの引数の型が合っていません。@."
+
+let print_illtyped_other () =
+  match language with
+| English -> fprintf std_formatter
+    "This expression is ill-typed.@."
+| Japanese -> fprintf std_formatter
+    "Error26 : この部分に型がつきません。@."
+
+let print_illtyped_too_much_args n exp_typ ltyps name =
+  match language with
+| English -> fprintf std_formatter
+    "The type conflict occurs at the ";
+   (match n with
+       1 -> fprintf std_formatter "1st argument.@."
+     | 2 -> fprintf std_formatter "2nd argument.@."
+     | 3 -> fprintf std_formatter "3rd argument.@."
+     | n -> fprintf std_formatter "%dth argument.@." n)
+| Japanese -> let len = List.length ltyps in
+    (fprintf std_formatter
+       "Error27 : この関数呼び出しで渡されている引数が多いようです。@,関数と引数の型は以下の通りです。@.");
+    (fprintf std_formatter
+	     "@[関数(";
+     print_string name;
+     fprintf std_formatter
+	     ")部分：@ %a@ @]@."
+	     Printtyp.type_expr exp_typ);
+    (print_illtyped_apply_args ltyps len)
+
+let print_illtyped_apply_not_function exp =
+  match language with
+  | English -> fprintf std_formatter
+		       "This is not function@.";
+  | Japanese -> (fprintf std_formatter
+       "Error28 : ハイライトされた部分が関数呼び出しになっているのに、@,関数部分が @ %a@ 型になっています。@." Printtyp.type_expr exp)
