[Caml-list] Question on "more general"

[Kenichi Asai <asai@is.ocha.ac.jp>]

[-- Attachment #1: Type: text/plain, Size: 617 bytes --]

Dear OCaml type inference experts,

If I infer the type (using Typemod.type_structure) of:

let a = 1 in fun x -> 1

and see if the type of x is more general (using Ctype.moregeneral)
than the type of a type variable (Btype.newgenvar ()), I obtain yes
(since the type of x is 'a which is more general (or equal) than a
newly created type variable, I guess).  If I do the same for:

let a = assert false in fun x -> 1

I obtain no, although it still seems that the type of x is the same
'a.  (See attached file for the concrete program I executed.  I used
OCaml 4.04.0.)  Why?

Thank you in advance!

-- 
Kenichi Asai

[-- Attachment #2: main.ml --]
[-- Type: text/plain, Size: 1764 bytes --]

open Asttypes
open Ast_helper
open Types
open Typedtree
open Parsetree

(* some helper functions *)

(* extract_typ : Typedtree.structure -> type_expr *)
let extract_typ str = match str.str_items with
    [{str_desc = Tstr_eval ({ exp_type = typ }, _)}] -> typ
  | _ -> failwith "cannot happen"

(* split_arrow : type_expr -> type_expr * type_expr *)
let rec split_arrow typ = match typ.desc with
    Tarrow (_, t1, t2, _) -> (t1, t2)
  | Tlink (typ') -> split_arrow typ'
  | _ -> failwith "cannot happen"

(* various expressions *)

(* 1 *)
let one : expression = Exp.constant (Const.integer "1")

(* false *)
let ff : expression = Exp.construct (mknoloc (Longident.Lident "false")) None

(* variable pattern *)
let var x : pattern = Pat.var (mknoloc x)

(* fun x -> 1 *)
let fun_x_one : expression = Exp.fun_ Nolabel None (var "x") one

(* let a = 1 in fun x -> 1 *)
let exp1 : expression =
  Exp.let_ Nonrecursive [Vb.mk (var "a") one] fun_x_one

let env : Env.t = Env.initial_safe_string

(* infer type of exp1 *)
let (str1', _, _) =
  Typemod.type_structure env [Str.eval exp1] Location.none

(* type of x *)
let (typx1, _) = split_arrow (extract_typ str1')

let b1 = Ctype.moregeneral env false typx1 (Btype.newgenvar ())

;; print_endline (if b1 then "true" else "false")

(* assert false *)
let assert_false : expression = Exp.assert_ ff

(* let a = assert false in fun x -> 1 *)
let exp2 : expression =
  Exp.let_ Nonrecursive [Vb.mk (var "a") assert_false] fun_x_one

(* infer type of exp2 *)
let (str2', _, _) =
  Typemod.type_structure env [Str.eval exp2] Location.none

(* type of x *)
let (typx2, _) = split_arrow (extract_typ str2')

let b2 = Ctype.moregeneral env false typx2 (Btype.newgenvar ())

;; print_endline (if b2 then "true" else "false")

[-- Attachment #3: Makefile --]
[-- Type: text/plain, Size: 167 bytes --]

run : main
	./main

main : main.ml
	ocamlfind ocamlc -package compiler-libs.common,compiler-libs.bytecomp -linkpkg main.ml -o main

clean :
	rm main main.cmi main.cmo