boolSyntax.type

- let val ty1 = Type `:'a -> 'b -> 'a`
      val ty2 = Type `:'a -> 'b -> 'b`
  in
     type_subst (type_unify ty1 ty2) ty1 = type_subst (type_unify ty1 ty2) ty2
  end;
> val it = true : bool

- let val alpha_list = Type `:'a list`
  in
     type_unify alpha alpha_list handle e => Raise e
  end;

  Exception raised at boolSyntax.type_unify:
  occurs check
  Exception-
     HOL_ERR
       {message = "occurs check", origin_function = "type_unify",
        origin_structure = "boolSyntax"} raised

Note that attempting to use Type.match_type in the first example results in immediate error, as it can only attempt to substitute the first argument to match the second:

- let val ty1 = Type `:'a -> 'b -> 'a`
      val ty2 = Type `:'a -> 'b -> 'b`
  in
     match_type ty1 ty2 handle e => Raise e
  end;

  Exception raised at Type.raw_match_type:
  double bind on type variable 'a
  Exception-
   HOL_ERR
     {message = "double bind on type variable 'a", origin_function =
      "raw_match_type", origin_structure = "Type"} raised