deal with type constants

Summary:
When we localize a function type with where constraints, we might localize type const access like T1::T. Whenever we localize type consts like T1::T, create a tvar v2 representing T1::T, and add it in the node for v1, representing T1:
```
v1 -> {
  upper_bound: [ StringBox; ... ]
  lower_bounds: ...
  appears_covariantly: ...
  appears_contravariantly: ...
  type_consts: varid SidMap.t = [
    "T" -> v2
  ]
}
```
Note: if we localize T1::T::T, then we would need v1 for T1, v2 for v1::T and v3 for v2::T.

For all present and future upper bounds U of #1, localize U::T as a type variable #3 with the same constraints as T in U, then make #2 equivalent to #3.

For all present and future lower bounds L of #1, simply make #2 equivalent to L::T.

For upper bounds, we're just checking that the constraints on U::T are satisfied. For lower bounds L however, we make #1::T equal to the type constant in L, possibly making it an expression dependent type if T is abstract in L.

Reviewed By: andrewjkennedy

Differential Revision: D13958402

fbshipit-source-id: 23b8d157fd78ae27d777904bbea53a166f6a939b

hphp/hack/src/typing/dune

@@ -56,6 +56,7 @@
     typing_reactivity
     typing_set
     typing_subtype
+    typing_subtype_tconst
     typing_taccess
     typing_tdef
     typing_unify

hphp/hack/src/typing/typing_dependent_type.ml

@@ -113,6 +113,7 @@ module ExprDepTy = struct
         let env, ty = apply_single env dep_tys ty in
         env, ty::acc) ~init:(env, []) in
       env, (r, Tunresolved tyl)
+    | _, Tvar _ -> env, ty
     | _ -> apply_single env dep_tys ety
 
 

hphp/hack/src/typing/typing_env.ml

@@ -78,6 +78,7 @@ let empty_tvar_info =
     upper_bounds = empty_bounds;
     appears_covariantly = false;
     appears_contravariantly = false;
+    type_constants = SMap.empty;
     }
 
 let add_current_tyvar env p v =
@@ -439,15 +440,14 @@ let get_tpenv_size env =
  *****************************************************************************)
 
 let get_tyvar_lower_bounds env var =
-match IMap.get var env.tvenv with
-| None -> empty_bounds
-| Some {lower_bounds; _} -> lower_bounds
+  match IMap.get var env.tvenv with
+  | None -> empty_bounds
+  | Some {lower_bounds; _} -> lower_bounds
 
 let get_tyvar_upper_bounds env var =
-match IMap.get var env.tvenv with
-| None -> empty_bounds
-| Some {upper_bounds; _} -> upper_bounds
-
+  match IMap.get var env.tvenv with
+  | None -> empty_bounds
+  | Some {upper_bounds; _} -> upper_bounds
 
 let rec is_tvar ~elide_nullable ty var =
   match ty with
@@ -461,11 +461,19 @@ let merge_tvar_info tvinfo1 tvinfo2 =
     upper_bounds = TySet.union tvinfo1.upper_bounds tvinfo2.upper_bounds;
     appears_covariantly = tvinfo1.appears_covariantly || tvinfo2.appears_covariantly;
     appears_contravariantly = tvinfo1.appears_contravariantly || tvinfo2.appears_contravariantly;
+    type_constants =
+      (* At this point, type constants of equivalent type variables must
+      have been made equivalent too. *)
+      SMap.union tvinfo1.type_constants tvinfo2.type_constants
+        ~combine:(fun _tconstid ty1 _ty2 -> Some ty1);
   }
 
 let get_tyvar_info env var =
   Option.value (IMap.get var env.tvenv) ~default:empty_tvar_info
 
+let set_tyvar_info env var tvinfo =
+  env_with_tvenv env (IMap.add var tvinfo env.tvenv)
+
 let remove_tyvar env var =
   env_with_tvenv env (IMap.remove var env.tvenv)
 
@@ -514,7 +522,7 @@ let remove_equivalent_tyvars env var =
       upper_bounds = TySet.diff tvinfo.upper_bounds redundant_bounds;
       lower_bounds = TySet.diff tvinfo.lower_bounds redundant_bounds;
     } in
-  env_with_tvenv env (IMap.add var tvinfo env.tvenv)
+  set_tyvar_info env var tvinfo
 
 let get_tyvar_appears_covariantly env var =
   let tvinfo = get_tyvar_info env var in
@@ -524,6 +532,18 @@ let get_tyvar_appears_contravariantly env var =
   let tvinfo = get_tyvar_info env var in
   tvinfo.appears_contravariantly
 
+let get_tyvar_type_consts env var =
+  let tvinfo = get_tyvar_info env var in
+  tvinfo.type_constants
+
+let get_tyvar_type_const env var (_, tyconstid) =
+  SMap.get tyconstid (get_tyvar_type_consts env var)
+
+let set_tyvar_type_const env var (_, tyconstid_ as tyconstid) ty =
+  let tvinfo = get_tyvar_info env var in
+  let type_constants = SMap.add tyconstid_ (tyconstid, ty) tvinfo.type_constants in
+  set_tyvar_info env var { tvinfo with type_constants }
+
 (* Conjoin a subtype proposition onto the subtype_prop in the environment *)
 let add_subtype_prop env prop =
   {env with subtype_prop = TL.conj env.subtype_prop prop}
@@ -1450,6 +1470,13 @@ let set_tyvar_variance ~tyvars env ty =
     let env = if ISet.mem var negative then set_tyvar_appears_contravariantly env var else env in
     env)
 
+let fresh_invariant_type_var env p =
+  let v = Ident.tmp () in
+  let env = add_current_tyvar env p v in
+  let env = set_tyvar_appears_covariantly env v in
+  let env = set_tyvar_appears_contravariantly env v in
+  env, (Reason.Rtype_variable p, Tvar v)
+
  (* Add a single new upper bound [ty] to type variable [var] in [env.tvenv].
   * If the optional [intersect] operation is supplied, then use this to avoid
   * adding redundant bounds by merging the type with existing bounds. This makes

hphp/hack/src/typing/typing_env.mli

@@ -18,6 +18,7 @@ val get_tcopt : env -> TypecheckerOptions.t
 val fresh : unit -> int
 val fresh_type : env -> Pos.t -> env *  locl ty
 val fresh_unresolved_type : env -> Pos.t -> env * locl ty
+val fresh_invariant_type_var : env -> Pos.t -> env * locl ty
 val open_tyvars : env -> env
 val get_current_tyvars : env -> Ident.t list
 val add_current_tyvar : env -> Pos.t -> Ident.t -> env
@@ -168,6 +169,12 @@ val get_tyvar_appears_contravariantly :
   env -> Ident.t -> bool
 val get_tyvar_info :
   env -> Ident.t -> tyvar_info
+val get_tyvar_type_const :
+  env -> int -> Nast.sid -> (Nast.sid * locl ty) option
+val set_tyvar_type_const :
+  env -> int -> Nast.sid -> locl ty -> env
+val get_tyvar_type_consts :
+  env -> int -> (Nast.sid * locl ty) SMap.t
 val remove_tyvar :
   env -> Ident.t -> env
 val remove_equivalent_tyvars :

hphp/hack/src/typing/typing_env_types.ml

@@ -105,6 +105,13 @@ type tyvar_info = {
   appears_contravariantly: bool;
   lower_bounds : TySet.t;
   upper_bounds : TySet.t;
+  (* Map associating a type to each type constant id of this variable.
+  Whenever we localize "T1::T" in a constraint, we add a fresh type variable
+  indexed by "T" in the type_constants of the type variable representing T1.
+  This allows to properly check constraints on "T1::T". *)
+  type_constants :
+    (Nast.sid (* id of the type constant "T", containing its position. *)
+    * locl_ty) SMap.t;
 }
 type tvenv = tyvar_info IMap.t
 

hphp/hack/src/typing/typing_env_types_sig.mli

@@ -52,6 +52,7 @@
    appears_contravariantly: bool;
    lower_bounds : TySet.t;
    upper_bounds : TySet.t;
+   type_constants : (Nast.sid * locl ty) SMap.t;
  }
  type tvenv = tyvar_info IMap.t
 

hphp/hack/src/typing/typing_subtype.ml

@@ -1656,6 +1656,8 @@ and add_tyvar_upper_bound env r var ty =
   let lower_bounds = Env.get_tyvar_lower_bounds env var in
   let env =
     Typing_set.fold (fun upper_bound env ->
+      let env = Typing_subtype_tconst.make_all_type_consts_equal env var
+        upper_bound ~as_tyvar_with_cnstr:true in
       Typing_set.fold (fun lower_bound env ->
         sub_type env lower_bound upper_bound)
         lower_bounds env)
@@ -1679,6 +1681,8 @@ and add_tyvar_lower_bound env r var ty =
   let upper_bounds = Env.get_tyvar_upper_bounds env var in
   let env =
     Typing_set.fold (fun lower_bound env ->
+      let env = Typing_subtype_tconst.make_all_type_consts_equal env var
+        lower_bound ~as_tyvar_with_cnstr:false in
       Typing_set.fold (fun upper_bound env ->
         sub_type env lower_bound upper_bound)
         upper_bounds env)

hphp/hack/src/typing/typing_subtype_tconst.ml

@@ -0,0 +1,51 @@
+module Env = Typing_env
+module Phase = Typing_phase
+module TySet = Typing_set
+module Utils = Typing_utils
+
+(** Make tconstty (usually a type variable representing the type constant of
+another type variable v) equal to ty::tconstid (where ty is usually a bound
+of v) *)
+let make_type_const_equal env tconstty ty tconstid ~as_tyvar_with_cnstr =
+  let ety_env = Phase.env_with_self env in
+  let (env, (_ety_env, tytconst)) =
+    Utils.expand_typeconst ety_env env ~as_tyvar_with_cnstr (fst ty) ty
+      [tconstid] in
+  let env = Utils.sub_type env tytconst tconstty in
+  let env = Utils.sub_type env tconstty tytconst in
+  env
+
+(** Add a type constant with id `tyconstid` and type `ty` to a type variable,
+and propagate constraints to all type constants `tyconstid` of upper bounds and
+lower bounds. *)
+let add_tyvar_type_const env var tconstid ty =
+  let env = Env.set_tyvar_type_const env var tconstid ty in
+  let upper_bounds = Env.get_tyvar_upper_bounds env var in
+  let env = TySet.fold
+    (fun bound env -> make_type_const_equal env ty bound tconstid
+      ~as_tyvar_with_cnstr:true)
+    upper_bounds env in
+  let lower_bounds = Env.get_tyvar_lower_bounds env var in
+  TySet.fold
+    (fun bound env -> make_type_const_equal env ty bound tconstid
+      ~as_tyvar_with_cnstr:false)
+    lower_bounds env
+
+
+(** For all type constants T of var, make its type equal to ty::T *)
+let make_all_type_consts_equal env var ty ~as_tyvar_with_cnstr =
+  SMap.fold
+    (fun _ (tconstid, tconstty) env ->
+      make_type_const_equal env tconstty ty tconstid ~as_tyvar_with_cnstr)
+    (Env.get_tyvar_type_consts env var)
+    env
+
+
+(** `p` is the position where var::tconstid was encountered. *)
+let get_tyvar_type_const env var (pos, _ as tconstid) =
+  match Env.get_tyvar_type_const env var tconstid with
+  | Some (_pos, ty) -> env, ty
+  | None ->
+    let env, tvar = Env.fresh_invariant_type_var env pos in
+    let env = add_tyvar_type_const env var tconstid tvar in
+    env, tvar

hphp/hack/src/typing/typing_subtype_tconst.mli

@@ -0,0 +1,22 @@
+open Typing_defs
+
+module Env = Typing_env
+
+(** For all type constant T of type variable, make its type equal to `ty`::T *)
+val make_all_type_consts_equal:
+  Env.env ->
+  Ident.t ->
+  locl ty ->
+  as_tyvar_with_cnstr:bool ->
+  Env.env
+
+(** Get the type of a type constant of a type variable by looking it up in the
+environment.
+If that type constant is not present, make a fresh invariant
+type variable and add it as the type of the type constant in the environment.
+*)
+val get_tyvar_type_const:
+  Env.env ->
+  Ident.t ->
+  Nast.sid ->
+  Env.env * locl ty

hphp/hack/src/typing/typing_taccess.ml

@@ -57,13 +57,18 @@ let empty_env env ety_env ids = {
   typeconsts_seen = [];
 }
 
-let rec expand_with_env ety_env env reason root ids =
-  let tenv, env, ty = expand_with_env_ ety_env env reason root ids in
+(** Expand a type constant access like A::T
+If as_tyvar_with_cnstr is set, then return a fresh type variable which has
+the same constraints as type constant T in A. Otherwise, return an
+AKGeneric("A::T"). *)
+let rec expand_with_env ety_env env ?(as_tyvar_with_cnstr = false) reason root ids =
+  let tenv, env, ty =
+    expand_with_env_ ety_env env ~as_tyvar_with_cnstr reason root ids in
   tenv, (env.ety_env, ty)
 
-and expand_with_env_ ety_env env reason root ids =
+and expand_with_env_ ety_env env ~as_tyvar_with_cnstr reason root ids =
   let env = empty_env env ety_env ids in
-  let env, (root_r, root_ty) = expand env root in
+  let env, (root_r, root_ty) = expand env ~as_tyvar_with_cnstr root in
   let trail = List.rev_map env.trail (compose strip_ns ExprDepTy.to_string) in
   let reason_func r =
     let r = match r with
@@ -96,7 +101,7 @@ and expand_with_env_ ety_env env reason root ids =
 
 and referenced_typeconsts tenv ety_env r (root, ids) =
   let tenv, (ety_env, root) = Phase.localize_with_env ~ety_env tenv root in
-  let _, env, _ = expand_with_env_ ety_env tenv r root ids in
+  let _, env, _ = expand_with_env_ ety_env ~as_tyvar_with_cnstr:false tenv r root ids in
   List.rev env.typeconsts_seen
 
 (* The root of a type access is a type. When expanding a type access this type
@@ -106,7 +111,10 @@ and referenced_typeconsts tenv ety_env r (root, ids) =
  * We also need to track what expansions have already taken place to make sure
  * we do not recurse infinitely.
  *)
-and expand env (root_reason, root_ty as root) =
+and expand env ~as_tyvar_with_cnstr root =
+  let expand = expand ~as_tyvar_with_cnstr in
+  let tenv, (root_reason, root_ty as root) = Env.expand_type env.tenv root in
+  let env = { env with tenv = tenv } in
   match env.ids with
   | [] ->
       env, root
@@ -120,7 +128,8 @@ and expand env (root_reason, root_ty as root) =
           let env, ty =
             create_root_from_type_constant
               env class_pos class_name
-               (root_reason, Tclass ((class_pos, class_name), Nonexact, tyl)) head in
+              (root_reason, Tclass ((class_pos, class_name), Nonexact, tyl))
+              head ~as_tyvar_with_cnstr in
           expand { env with ids = tail } ty
       | Tabstract (AKgeneric s, _) ->
         let dep_ty = generic_to_dep_ty s in
@@ -171,13 +180,9 @@ and expand env (root_reason, root_ty as root) =
             { prev_env with tenv }, ty
           end in
           { env with dep_tys = [] } , (root_reason, Tunresolved tyl)
-      | Tvar _ ->
-          if TypecheckerOptions.new_inference env.tenv.Env.genv.Env.tcopt
-          then env, root (* TODO: T36856670 *)
-          else
-            let tenv, ty = Env.expand_type env.tenv root in
-            let env = { env with tenv = tenv } in
-            expand env ty
+      | Tvar n ->
+          let tenv, ty = Typing_subtype_tconst.get_tyvar_type_const env.tenv n head in
+          expand { env with ids = tail; tenv } ty
       | Tanon _ | Tobject | Tnonnull | Tprim _ | Tshape _ | Ttuple _
       | Tarraykind _ | Tfun _ | Tabstract (_, _)  | Tdynamic ->
           let pos, tconst = head in
@@ -199,8 +204,9 @@ and expand env (root_reason, root_ty as root) =
  * otherwise we choose the constraint type. If there is no constraint type then
  * we choose the assigned type.
  *)
-and create_root_from_type_constant env class_pos class_name root_ty (pos, tconst) =
-  match get_typeconst env class_pos class_name pos tconst with
+and create_root_from_type_constant env class_pos class_name root_ty
+  (pos, tconst) ~as_tyvar_with_cnstr =
+  match get_typeconst env class_pos class_name pos tconst ~as_tyvar_with_cnstr with
   | None -> env, (fst root_ty, Typing_utils.tany env.tenv)
   | Some (env, typeconst) ->
       let env =
@@ -231,20 +237,29 @@ and create_root_from_type_constant env class_pos class_name root_ty (pos, tconst
              *)
             let dep_tys =
               List.map env.dep_tys (fun (r, (d, s)) -> r, (d, s @ [tconst])) in
-            { env with dep_tys = dep_ty::dep_tys; tenv = tenv }, cstr
+            let tenv, ty =
+              if as_tyvar_with_cnstr then
+                let tenv, tvar = Env.fresh_invariant_type_var tenv pos in
+                let tenv = Typing_utils.sub_type tenv tvar cstr in
+                tenv, tvar
+              else tenv, cstr in
+            { env with dep_tys = dep_ty::dep_tys; tenv }, ty
         | _ ->
-            let ty =
-              Reason.Rwitness (fst typeconst.ttc_name),
-              Tabstract (AKgeneric (class_name^"::"^tconst), None) in
-              let dep_tys =
+            let tenv, ty =
+              if as_tyvar_with_cnstr then Env.fresh_invariant_type_var tenv pos
+              else
+                let reason = Reason.Rwitness (fst typeconst.ttc_name) in
+                let ty = (reason, Tabstract (AKgeneric (class_name^"::"^tconst), None)) in
+                tenv, ty in
+            let dep_tys =
               List.map env.dep_tys (fun (r, (d, s)) -> r, (d, s @ [tconst])) in
-            { env with dep_tys = dep_tys }, ty
+            { env with dep_tys; tenv }, ty
       end
 
 (* Looks up the type constant within the given class. This also checks for
  * potential cycles by examining the expansions we have already performed.
  *)
-and get_typeconst env class_pos class_name pos tconst =
+and get_typeconst env class_pos class_name pos tconst ~as_tyvar_with_cnstr =
   try
     let class_ = match Env.get_class env.tenv class_name with
       | None ->
@@ -253,8 +268,9 @@ and get_typeconst env class_pos class_name pos tconst =
       | Some c -> c in
     let typeconst = match Env.get_typeconst env.tenv class_ tconst with
       | None ->
-          Errors.smember_not_found
-            `class_typeconst pos ((Cls.pos class_), class_name) tconst `no_hint;
+          if not as_tyvar_with_cnstr then
+            Errors.smember_not_found
+              `class_typeconst pos ((Cls.pos class_), class_name) tconst `no_hint;
           raise Exit
       | Some tc -> tc in
     let tc_tuple = ((Cls.name class_), snd typeconst.ttc_name, pos) in

hphp/hack/src/typing/typing_utils.ml

@@ -84,8 +84,8 @@ let (expand_type_and_solve_ref: expand_type_and_solve_type ref) = ref not_implem
 let expand_type_and_solve x = !expand_type_and_solve_ref x
 
 type expand_typeconst =
-  expand_env -> Env.env -> Reason.t -> locl ty -> Nast.sid list ->
-  Env.env * ety
+  expand_env -> Env.env -> ?as_tyvar_with_cnstr:bool -> Reason.t -> locl ty ->
+  Nast.sid list -> Env.env * ety
 let (expand_typeconst_ref: expand_typeconst ref) = ref not_implemented
 let expand_typeconst x = !expand_typeconst_ref x
 

hphp/hack/test/typecheck/new_inference/tconst/HH_FLAGS

@@ -0,0 +1,2 @@
+--new-inference
+--all-errors