hphp/hack/src/typing/typing_generic_constraint.ml

   1 (*
   2  * Copyright (c) 2015, Facebook, Inc.
   3  * All rights reserved.
   4  *
   5  * This source code is licensed under the MIT license found in the
   6  * LICENSE file in the "hack" directory of this source tree.
   7  *
   8  *)
   9
  10 open Core_kernel
  11 module TUtils = Typing_utils
  12 module Reason = Typing_reason
  13 module Env = Typing_env
  14 open Typing_defs
  15 open Typing_env_types
  16
  17 let check_constraint env ck ty ~cstr_ty =
  18   Typing_log.(log_with_level env "sub" 1 (fun () ->
  19     log_types (Reason.to_pos (fst ty)) env
  20     [Log_head ("Typing_generic_constraint.check_constraint",
  21      [Log_type ("ty", ty);
  22       Log_type ("cstr_ty", cstr_ty)])]));
  23   let env, ety = Env.expand_type env ty in
  24   let env, ecstr_ty = Env.expand_type env cstr_ty in
  25   (* using unify error here since the error itself is (almost) always superseded
  26    * by an Errors.try_ fallback using explain_constraint *)
  27   match ck with
  28   | Ast_defs.Constraint_as ->
  29       (* If ty is a Tvar, we don't want to unify that Tvar with
  30        * cstr_ty; we merely want the type itself to be added to
  31        * cstr_ty's list of unresolved types. Thus we pass the
  32        * expanded type. *)
  33       TUtils.sub_type env ety cstr_ty Errors.unify_error
  34   | Ast_defs.Constraint_eq ->
  35       (* An equality constraint is the same as two commuting `as`
  36        * constraints, i.e. X=Y is { X as Y, Y as X }. Thus, add
  37        * add both expansions to the environment. We don't expand
  38        * both sides of the equation simultaniously, to preserve an
  39        * easier convergence indication. *)
  40        let env = TUtils.sub_type env ecstr_ty ty Errors.unify_error in
  41        TUtils.sub_type env ety cstr_ty Errors.unify_error
  42   | Ast_defs.Constraint_super ->
  43       (* If cstr_ty is a Tvar, we don't want to unify that Tvar with
  44        * ty; we merely want the constraint itself to be added to the
  45        * ty's list of unresolved types. Thus we pass the expanded
  46        * constraint type. *)
  47       TUtils.sub_type env ecstr_ty ty Errors.unify_error
  48
  49 let add_check_constraint_todo (env:env) ~use_pos (pos,name) ck cstr_ty ty =
  50     Errors.try_
  51       (fun () ->
  52         check_constraint env ck ty ~cstr_ty)
  53       (fun l ->
  54        Errors.explain_constraint ~use_pos ~definition_pos:pos ~param_name:name l;
  55        env
  56       )
  57
  58 let add_check_where_constraint_todo ~in_class (env:env) ~use_pos ~definition_pos ck cstr_ty ty =
  59     Errors.try_
  60       (fun () ->
  61         check_constraint env ck ty ~cstr_ty)
  62       (fun l ->
  63         Errors.explain_where_constraint ~in_class ~use_pos ~definition_pos l;
  64         env
  65       )
  66
  67 (*
  68   For where clauses containing type accesses, we can't just handle equality
  69   constraints the normal way. Given two unresolved types(which are exactly the
  70   type returned by generics when checking where constraints), unifying them will
  71   only cause the types to grow. Thus (int) will unify with (string). But this is
  72   unsound when it comes to generic type accesses, since type constants do not
  73   follow variance rules. Thus, the reasonable thing to do is to check whether
  74   all types within the unresolved types unify with each other.
  75
  76   For example, for the constraint:
  77   function foo<T1 as Box, T2>(T1 $x) : T2 where T1::T = T2::T {
  78     $x->set($y->get());
  79   }
  80   We should expect the where clause to actually check if T1 and T2
  81   are equal, not unify them into the same type.
  82 *)
  83 let handle_eq_tconst_constraint env ck ty cstr_ty =
  84   (* First check that the bigger types work *)
  85   let env = check_constraint env ck ty ~cstr_ty in
  86   let env, ty = Env.expand_type env ty in
  87   let env, cstr_ty = Env.expand_type env cstr_ty in
  88   let rec flatten_unresolved_tys ty =
  89     match ty with
  90     | _, Tunion tyl ->
  91       List.fold tyl ~init: []
  92       ~f: (fun acc ty -> (flatten_unresolved_tys ty) @ acc)
  93     | _ ->
  94       [ty] in
  95   let tyl =
  96     (flatten_unresolved_tys) ty @ (flatten_unresolved_tys cstr_ty) in
  97   match tyl with
  98   (* If they are both unresolved and empty for some reason, it's fine *)
  99   | [] -> env
 100   | ty::tys ->
 101   List.fold tys ~init: env
 102   ~f: begin fun env ty_ ->
 103     check_constraint env ck ty_ ~cstr_ty:ty
 104   end
 105
 106 let add_check_tconst_where_constraint_todo
 107   (env:env) ~use_pos ~definition_pos ck ty_from_env cstr_ty ty =
 108     Errors.try_
 109       (fun () ->
 110         let env, ty = ty_from_env env ty in
 111         let env, cstr_ty = ty_from_env env cstr_ty in
 112         match ck with
 113         | Ast_defs.Constraint_eq ->
 114           handle_eq_tconst_constraint env ck ty cstr_ty
 115         | _ ->
 116           check_constraint env ck ty ~cstr_ty
 117       )
 118       (fun l ->
 119         Errors.explain_tconst_where_constraint ~use_pos ~definition_pos l;
 120        env
 121       )