typing/typetexp.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                           Objective Caml                            *)
   4 (*                                                                     *)
   5 (*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
   6 (*                                                                     *)
   7 (*  Copyright 1996 Institut National de Recherche en Informatique et   *)
   8 (*  en Automatique.  All rights reserved.  This file is distributed    *)
   9 (*  under the terms of the Q Public License version 1.0.               *)
  10 (*                                                                     *)
  11 (***********************************************************************)
  12
  13 (* typetexp.ml,v 1.34.4.9 2002/01/07 08:39:16 garrigue Exp *)
  14
  15 (* Typechecking of type expressions for the core language *)
  16
  17 open Misc
  18 open Parsetree
  19 open Types
  20 open Ctype
  21
  22 exception Already_bound
  23
  24 type error =
  25     Unbound_type_variable of string
  26   | Unbound_type_constructor of Longident.t
  27   | Unbound_type_constructor_2 of Path.t
  28   | Type_arity_mismatch of Longident.t * int * int
  29   | Bound_type_variable of string
  30   | Recursive_type
  31   | Unbound_class of Longident.t
  32   | Unbound_row_variable of Longident.t
  33   | Type_mismatch of (type_expr * type_expr) list
  34   | Alias_type_mismatch of (type_expr * type_expr) list
  35   | Present_has_conjunction of string
  36   | Present_has_no_type of string
  37   | Constructor_mismatch of type_expr * type_expr
  38   | Not_a_variant of type_expr
  39   | Variant_tags of string * string
  40   | Invalid_variable_name of string
  41   | Cannot_quantify of string * type_expr
  42
  43 exception Error of Location.t * error
  44
  45 type variable_context = int * (string, type_expr) Tbl.t
  46
  47 (* Translation of type expressions *)
  48
  49 let type_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
  50 let univars        = ref ([] : (string * type_expr) list)
  51 let pre_univars    = ref ([] : type_expr list)
  52 let used_variables = ref (Tbl.empty : (string, type_expr * Location.t) Tbl.t)
  53
  54 let reset_type_variables () =
  55   reset_global_level ();
  56   type_variables := Tbl.empty
  57
  58 let narrow () =
  59   (increase_global_level (), !type_variables)
  60
  61 let widen (gl, tv) =
  62   restore_global_level gl;
  63   type_variables := tv
  64
  65 let enter_type_variable strict loc name =
  66   try
  67     if name <> "" && name.[0] = '_' then
  68       raise (Error (loc, Invalid_variable_name ("'" ^ name)));
  69     let v = Tbl.find name !type_variables in
  70     if strict then raise Already_bound;
  71     v
  72   with Not_found ->
  73     let v = new_global_var() in
  74     type_variables := Tbl.add name v !type_variables;
  75     v
  76
  77 let type_variable loc name =
  78   try
  79     Tbl.find name !type_variables
  80   with Not_found ->
  81     raise(Error(loc, Unbound_type_variable ("'" ^ name)))
  82
  83 let wrap_method ty =
  84   match (Ctype.repr ty).desc with
  85     Tpoly _ -> ty
  86   | _ -> Ctype.newty (Tpoly (ty, []))
  87
  88 let new_pre_univar () =
  89   let v = newvar () in pre_univars := v :: !pre_univars; v
  90
  91 let rec swap_list = function
  92     x :: y :: l -> y :: x :: swap_list l
  93   | l -> l
  94
  95 type policy = Fixed | Extensible | Univars
  96
  97 let rec transl_type env policy styp =
  98   match styp.ptyp_desc with
  99     Ptyp_any ->
 100       if policy = Univars then new_pre_univar () else
 101       if policy = Fixed then
 102         raise (Error (styp.ptyp_loc, Unbound_type_variable "_"))
 103       else newvar ()
 104   | Ptyp_var name ->
 105       if name <> "" && name.[0] = '_' then
 106         raise (Error (styp.ptyp_loc, Invalid_variable_name ("'" ^ name)));
 107       begin try
 108         instance (List.assoc name !univars)
 109       with Not_found -> try
 110         instance (fst(Tbl.find name !used_variables))
 111       with Not_found ->
 112         let v =
 113           if policy = Univars then new_pre_univar () else newvar () in
 114         used_variables := Tbl.add name (v, styp.ptyp_loc) !used_variables;
 115         v
 116       end
 117   | Ptyp_arrow(l, st1, st2) ->
 118       let ty1 = transl_type env policy st1 in
 119       let ty2 = transl_type env policy st2 in
 120       newty (Tarrow(l, ty1, ty2, Cok))
 121   | Ptyp_tuple stl ->
 122       newty (Ttuple(List.map (transl_type env policy) stl))
 123   | Ptyp_constr(lid, stl) ->
 124       let (path, decl) =
 125         try
 126           Env.lookup_type lid env
 127         with Not_found ->
 128           raise(Error(styp.ptyp_loc, Unbound_type_constructor lid)) in
 129       if List.length stl <> decl.type_arity then
 130         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
 131                                                            List.length stl)));
 132       let args = List.map (transl_type env policy) stl in
 133       let params = Ctype.instance_list decl.type_params in
 134       let unify_param =
 135         match decl.type_manifest with
 136           None -> unify_var
 137         | Some ty ->
 138             if (repr ty).level = Btype.generic_level then unify_var else unify
 139       in
 140       List.iter2
 141         (fun (sty, ty) ty' ->
 142            try unify_param env ty' ty with Unify trace ->
 143              raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
 144         (List.combine stl args) params;
 145       let constr = newconstr path args in
 146       begin try
 147         Ctype.enforce_constraints env constr
 148       with Unify trace ->
 149         raise (Error(styp.ptyp_loc, Type_mismatch trace))
 150       end;
 151       constr
 152   | Ptyp_object fields ->
 153       newobj (transl_fields env policy fields)
 154   | Ptyp_class(lid, stl, present) ->
 155       let (path, decl, is_variant) =
 156         try
 157           let (path, decl) = Env.lookup_type lid env in
 158           let rec check decl =
 159             match decl.type_manifest with
 160               None -> raise Not_found
 161             | Some ty ->
 162                 match (repr ty).desc with
 163                   Tvariant row when Btype.static_row row -> ()
 164                 | Tconstr (path, _, _) ->
 165                     check (Env.find_type path env)
 166                 | _ -> raise Not_found
 167           in check decl;
 168           Location.prerr_warning styp.ptyp_loc Warnings.Deprecated;
 169           (path, decl,true)
 170         with Not_found -> try
 171           if present <> [] then raise Not_found;
 172           let lid2 =
 173             match lid with
 174               Longident.Lident s     -> Longident.Lident ("#" ^ s)
 175             | Longident.Ldot(r, s)   -> Longident.Ldot (r, "#" ^ s)
 176             | Longident.Lapply(_, _) -> fatal_error "Typetexp.transl_type"
 177           in
 178           let (path, decl) = Env.lookup_type lid2 env in
 179           (path, decl, false)
 180         with Not_found ->
 181           raise(Error(styp.ptyp_loc, Unbound_class lid))
 182       in
 183       if List.length stl <> decl.type_arity then
 184         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
 185                                                        List.length stl)));
 186       let args = List.map (transl_type env policy) stl in
 187       let params = Ctype.instance_list decl.type_params in
 188       List.iter2
 189         (fun (sty, ty) ty' ->
 190            try unify_var env ty' ty with Unify trace ->
 191              raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
 192         (List.combine stl args) params;
 193       let ty =
 194         try Ctype.expand_head env (newconstr path args)
 195         with Unify trace ->
 196           raise (Error(styp.ptyp_loc, Type_mismatch trace))
 197       in
 198       begin match ty.desc with
 199         Tvariant row ->
 200           let row = Btype.row_repr row in
 201           List.iter
 202             (fun l -> if not (List.mem_assoc l row.row_fields) then
 203               raise(Error(styp.ptyp_loc, Present_has_no_type l)))
 204             present;
 205           let fields =
 206             List.map
 207               (fun (l,f) -> l,
 208                 if List.mem l present then f else
 209                 match Btype.row_field_repr f with
 210                 | Rpresent (Some ty) ->
 211                     Reither(false, [ty], false, ref None)
 212                 | Rpresent None ->
 213                     Reither (true, [], false, ref None)
 214                 | _ -> f)
 215               row.row_fields
 216           in
 217           let row = { row_closed = true; row_fields = fields;
 218                       row_bound = (); row_name = Some (path, args);
 219                       row_fixed = false; row_more = newvar () } in
 220           let static = Btype.static_row row in
 221           let row =
 222             if static || policy <> Univars then row
 223             else { row with row_more = new_pre_univar () }
 224           in
 225           newty (Tvariant row)
 226       | Tobject (fi, _) ->
 227           let _, tv = flatten_fields fi in
 228           if policy = Univars then pre_univars := tv :: !pre_univars;
 229           ty
 230       | _ ->
 231           assert false
 232       end
 233   | Ptyp_alias(st, alias) ->
 234       begin
 235         try
 236           let t =
 237             try List.assoc alias !univars
 238             with Not_found ->
 239               instance (fst(Tbl.find alias !used_variables))
 240           in
 241           let ty = transl_type env policy st in
 242           begin try unify_var env t ty with Unify trace ->
 243             let trace = swap_list trace in
 244             raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
 245           end;
 246           ty
 247         with Not_found ->
 248           if !Clflags.principal then begin_def ();
 249           let t = newvar () in
 250           used_variables := Tbl.add alias (t, styp.ptyp_loc) !used_variables;
 251           let ty = transl_type env policy st in
 252           begin try unify_var env t ty with Unify trace ->
 253             let trace = swap_list trace in
 254             raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
 255           end;
 256           if !Clflags.principal then begin
 257             end_def ();
 258             generalize_structure t;
 259           end;
 260           instance t
 261       end
 262   | Ptyp_variant(fields, closed, present) ->
 263       let name = ref None in
 264       let mkfield l f =
 265         newty (Tvariant {row_fields=[l,f]; row_more=newvar();
 266                          row_bound=(); row_closed=true;
 267                          row_fixed=false; row_name=None}) in
 268       let hfields = Hashtbl.create 17 in
 269       let add_typed_field loc l f =
 270         let h = Btype.hash_variant l in
 271         try
 272           let (l',f') = Hashtbl.find hfields h in
 273           (* Check for tag conflicts *)
 274           if l <> l' then raise(Error(styp.ptyp_loc, Variant_tags(l, l')));
 275           let ty = mkfield l f and ty' = mkfield l f' in
 276           if equal env false [ty] [ty'] then () else
 277           try unify env ty ty'
 278           with Unify trace -> raise(Error(loc, Constructor_mismatch (ty,ty')))
 279         with Not_found ->
 280           Hashtbl.add hfields h (l,f)
 281       in
 282       let rec add_field = function
 283           Rtag (l, c, stl) ->
 284             name := None;
 285             let f = match present with
 286               Some present when not (List.mem l present) ->
 287                 let tl = List.map (transl_type env policy) stl in
 288                 Reither(c, tl, false, ref None)
 289             | _ ->
 290                 if List.length stl > 1 || c && stl <> [] then
 291                   raise(Error(styp.ptyp_loc, Present_has_conjunction l));
 292                 match stl with [] -> Rpresent None
 293                 | st :: _ -> Rpresent (Some(transl_type env policy st))
 294             in
 295             add_typed_field styp.ptyp_loc l f
 296         | Rinherit sty ->
 297             let ty = transl_type env policy sty in
 298             let nm =
 299               match repr ty with
 300                 {desc=Tconstr(p, tl, _)} -> Some(p, tl)
 301               | _                        -> None
 302             in
 303             begin try
 304               (* Set name if there are no fields yet *)
 305               Hashtbl.iter (fun _ _ -> raise Exit) hfields;
 306               name := nm
 307             with Exit ->
 308               (* Unset it otherwise *)
 309               name := None
 310             end;
 311             let fl = match expand_head env ty, nm with
 312               {desc=Tvariant row}, _ when Btype.static_row row ->
 313                 let row = Btype.row_repr row in
 314                 row.row_fields
 315             | {desc=Tvar}, Some(p, _) ->
 316                 raise(Error(sty.ptyp_loc, Unbound_type_constructor_2 p))
 317             | _ ->
 318                 raise(Error(sty.ptyp_loc, Not_a_variant ty))
 319             in
 320             List.iter
 321               (fun (l, f) ->
 322                 let f = match present with
 323                   Some present when not (List.mem l present) ->
 324                     begin match f with
 325                       Rpresent(Some ty) ->
 326                         Reither(false, [ty], false, ref None)
 327                     | Rpresent None ->
 328                         Reither(true, [], false, ref None)
 329                     | _ ->
 330                         assert false
 331                     end
 332                 | _ -> f
 333                 in
 334                 add_typed_field sty.ptyp_loc l f)
 335               fl
 336       in
 337       List.iter add_field fields;
 338       let fields = Hashtbl.fold (fun _ p l -> p :: l) hfields [] in
 339       begin match present with None -> ()
 340       | Some present ->
 341           List.iter
 342             (fun l -> if not (List.mem_assoc l fields) then
 343               raise(Error(styp.ptyp_loc, Present_has_no_type l)))
 344             present
 345       end;
 346       let row =
 347         { row_fields = List.rev fields; row_more = newvar ();
 348           row_bound = (); row_closed = closed;
 349           row_fixed = false; row_name = !name } in
 350       let static = Btype.static_row row in
 351       let row =
 352         if static then row else
 353         match policy with
 354           Fixed ->
 355             raise (Error (styp.ptyp_loc, Unbound_type_variable ".."))
 356         | Extensible -> row
 357         | Univars -> { row with row_more = new_pre_univar () }
 358       in
 359       newty (Tvariant row)
 360   | Ptyp_poly(vars, st) ->
 361       begin_def();
 362       let new_univars = List.map (fun name -> name, newvar()) vars in
 363       let old_univars = !univars in
 364       univars := new_univars @ !univars;
 365       let ty = transl_type env policy st in
 366       univars := old_univars;
 367       end_def();
 368       generalize ty;
 369       let ty_list =
 370         List.fold_left
 371           (fun tyl (name, ty1) ->
 372             let v = Btype.proxy ty1 in
 373             if deep_occur v ty then begin
 374               if v.level <> Btype.generic_level || v.desc <> Tvar then
 375                 raise (Error (styp.ptyp_loc, Cannot_quantify (name, v)));
 376               v.desc <- Tunivar;
 377               v :: tyl
 378             end else tyl)
 379           [] new_univars
 380       in
 381       let ty' = Btype.newgenty (Tpoly(ty, List.rev ty_list)) in
 382       unify_var env (newvar()) ty';
 383       ty'
 384
 385 and transl_fields env policy =
 386   function
 387     [] ->
 388       newty Tnil
 389   | ({pfield_desc = Pfield_var} as pf)::_ ->
 390       begin match policy with
 391         Fixed -> raise (Error (pf.pfield_loc, Unbound_type_variable ".."))
 392       | Extensible -> newvar ()
 393       | Univars -> new_pre_univar ()
 394       end
 395   | {pfield_desc = Pfield(s, e)}::l ->
 396       let ty1 = transl_type env policy e in
 397       let ty2 = transl_fields env policy l in
 398         newty (Tfield (s, Fpresent, ty1, ty2))
 399
 400
 401 (* Make the rows "fixed" in this type, to make universal check easier *)
 402 let rec make_fixed_univars ty =
 403   let ty = repr ty in
 404   if ty.level >= Btype.lowest_level then begin
 405     Btype.mark_type_node ty;
 406     match ty.desc with
 407     | Tvariant row ->
 408         let row = Btype.row_repr row in
 409         if (Btype.row_more row).desc = Tunivar then
 410           ty.desc <- Tvariant
 411               {row with row_fixed=true;
 412                row_fields = List.map
 413                  (fun (s,f as p) -> match Btype.row_field_repr f with
 414                    Reither (c, tl, m, r) -> s, Reither (c, tl, true, r)
 415                  | _ -> p)
 416                  row.row_fields};
 417         Btype.iter_row make_fixed_univars row
 418     | _ ->
 419         Btype.iter_type_expr make_fixed_univars ty
 420   end
 421
 422 let make_fixed_univars ty =
 423   make_fixed_univars ty;
 424   Btype.unmark_type ty
 425
 426 let globalize_used_variables env fixed =
 427   let r = ref [] in
 428   Tbl.iter
 429     (fun name (ty, loc) ->
 430       let v = new_global_var () in
 431       let snap = Btype.snapshot () in
 432       if try unify env v ty; true with _ -> Btype.backtrack snap; false
 433       then try
 434         r := (loc, v,  Tbl.find name !type_variables) :: !r
 435       with Not_found ->
 436         if fixed && (repr ty).desc = Tvar then
 437           raise(Error(loc, Unbound_type_variable ("'"^name)));
 438         let v2 = new_global_var () in
 439         r := (loc, v, v2) :: !r;
 440         type_variables := Tbl.add name v2 !type_variables)
 441     !used_variables;
 442   used_variables := Tbl.empty;
 443   fun () ->
 444     List.iter
 445       (function (loc, t1, t2) ->
 446         try unify env t1 t2 with Unify trace ->
 447           raise (Error(loc, Type_mismatch trace)))
 448       !r
 449
 450 let transl_simple_type env fixed styp =
 451   univars := []; used_variables := Tbl.empty;
 452   let typ = transl_type env (if fixed then Fixed else Extensible) styp in
 453   globalize_used_variables env fixed ();
 454   make_fixed_univars typ;
 455   typ
 456
 457 let transl_simple_type_univars env styp =
 458   univars := []; used_variables := Tbl.empty; pre_univars := [];
 459   begin_def ();
 460   let typ = transl_type env Univars styp in
 461   (* Only keep already global variables in used_variables *)
 462   let new_variables = !used_variables in
 463   used_variables := Tbl.empty;
 464   Tbl.iter
 465     (fun name p ->
 466       if Tbl.mem name !type_variables then
 467         used_variables := Tbl.add name p !used_variables)
 468     new_variables;
 469   globalize_used_variables env false ();
 470   end_def ();
 471   generalize typ;
 472   let univs =
 473     List.fold_left
 474       (fun acc v ->
 475         let v = repr v in
 476         if v.level <> Btype.generic_level || v.desc <> Tvar then acc
 477         else (v.desc <- Tunivar ; v :: acc))
 478       [] !pre_univars
 479   in
 480   make_fixed_univars typ;
 481   instance (Btype.newgenty (Tpoly (typ, univs)))
 482
 483 let transl_simple_type_delayed env styp =
 484   univars := []; used_variables := Tbl.empty;
 485   let typ = transl_type env Extensible styp in
 486   (typ, globalize_used_variables env false)
 487
 488 let transl_type_scheme env styp =
 489   reset_type_variables();
 490   begin_def();
 491   let typ = transl_simple_type env false styp in
 492   end_def();
 493   generalize typ;
 494   typ
 495
 496 (* Error report *)
 497
 498 open Format
 499 open Printtyp
 500
 501 let report_error ppf = function
 502   | Unbound_type_variable name ->
 503       fprintf ppf "Unbound type parameter %s" name
 504   | Unbound_type_constructor lid ->
 505       fprintf ppf "Unbound type constructor %a" longident lid
 506   | Unbound_type_constructor_2 p ->
 507       fprintf ppf "The type constructor@ %a@ is not yet completely defined"
 508         path p
 509   | Type_arity_mismatch(lid, expected, provided) ->
 510       fprintf ppf
 511        "@[The type constructor %a@ expects %i argument(s),@ \
 512         but is here applied to %i argument(s)@]"
 513        longident lid expected provided
 514   | Bound_type_variable name ->
 515       fprintf ppf "Already bound type parameter '%s" name
 516   | Recursive_type ->
 517       fprintf ppf "This type is recursive"
 518   | Unbound_class lid ->
 519       fprintf ppf "Unbound class %a" longident lid
 520   | Unbound_row_variable lid ->
 521       fprintf ppf "Unbound row variable in #%a" longident lid
 522   | Type_mismatch trace ->
 523       Printtyp.unification_error true trace
 524         (function ppf ->
 525            fprintf ppf "This type")
 526         ppf
 527         (function ppf ->
 528            fprintf ppf "should be an instance of type")
 529   | Alias_type_mismatch trace ->
 530       Printtyp.unification_error true trace
 531         (function ppf ->
 532            fprintf ppf "This alias is bound to type")
 533         ppf
 534         (function ppf ->
 535            fprintf ppf "but is used as an instance of type")
 536   | Present_has_conjunction l ->
 537       fprintf ppf "The present constructor %s has a conjunctive type" l
 538   | Present_has_no_type l ->
 539       fprintf ppf "The present constructor %s has no type" l
 540   | Constructor_mismatch (ty, ty') ->
 541       Printtyp.reset_and_mark_loops_list [ty; ty'];
 542       fprintf ppf "@[<hov>%s %a@ %s@ %a@]"
 543         "This variant type contains a constructor"
 544         Printtyp.type_expr ty
 545         "which should be"
 546         Printtyp.type_expr ty'
 547   | Not_a_variant ty ->
 548       Printtyp.reset_and_mark_loops ty;
 549       fprintf ppf "@[The type %a@ is not a polymorphic variant type@]"
 550         Printtyp.type_expr ty
 551   | Variant_tags (lab1, lab2) ->
 552       fprintf ppf
 553         "Variant tags `%s@ and `%s have same hash value.@ Change one of them."
 554         lab1 lab2
 555   | Invalid_variable_name name ->
 556       fprintf ppf "The type variable name %s is not allowed in programs" name
 557   | Cannot_quantify (name, v) ->
 558       fprintf ppf "This type scheme cannot quantify '%s :@ %s." name
 559         (if v.desc = Tvar then "it escapes this scope" else
 560          if v.desc = Tunivar then "it is aliased to another variable"
 561          else "it is not a variable")