recursive case type: make bound check less restrictive

Summary:
This diff aims at supporting cases like:
```
case type CT1 as shape(?'a' => nonnull) = shape(?'a' => CT1);
case type CT2 as shape(?'a' => shape(?'a' => nonnull)) = shape(?'a' => CT2);
```
The previous behaviour was to localize CT1/CT2 as mixed and therefore fail the bound check.
That localization to mixed was due to passing `~report_cycle:CT1/2` to `localize`. Upon detection of any cycle, localization stops and creates a mixed. Passing `~report_cycle:CT1/2` makes it localize the CT1/2 to mixed, which is wrong for further usages.

This diff calls localize twice, once to report cycles, and once to use the result for bound checks and other checks.

Reviewed By: andrewjkennedy

Differential Revision: D67938199

fbshipit-source-id: bdd850d909294abafaba5ff76fcc37f1229515e3

Author: Catherine Gasnier

hphp/hack/src/typing/typing_typedef.ml

@@ -205,6 +205,22 @@ let casetype_def env typedef =
     Option.iter ~f:(Typing_error_utils.add_typing_error ~env) err2;
     env
 
+let check_cycles env (t_pos, t_name) hints =
+  let (env, cycles) =
+    List.fold_left hints ~init:(env, []) ~f:(fun (env, cycles) hint ->
+        let ((env, _ty_err_opt, new_cycles), _ty) =
+          Phase.localize_hint_no_subst_report_cycles
+            env
+            ~ignore_errors:true
+            ~report_cycle:(t_pos, Type_expansions.Expandable.Type_alias t_name)
+            hint
+        in
+        (env, new_cycles @ cycles))
+  in
+  Type_expansions.report cycles
+  |> Option.iter ~f:(Typing_error_utils.add_typing_error ~env);
+  env
+
 let typedef_def ctx typedef =
   let env = EnvFromDef.typedef_env ~origin:Decl_counters.TopLevel ctx typedef in
   let {
@@ -242,7 +258,6 @@ let typedef_def ctx typedef =
           not (recursive_case_types env)),
         List.map (variant :: variants) ~f:(fun v -> v.tctv_hint) )
   in
-  let (t_pos, t_name_) = t_name in
   let env = Env.set_current_module env t_module in
   let env = Env.set_internal env t_internal in
   let env = Env.set_current_package_membership env t_package in
@@ -260,28 +275,24 @@ let typedef_def ctx typedef =
   Typing_variance.typedef env typedef;
 
   let env =
-    let (env, ty_err_opt2, cycles, tys) =
+    if do_report_cycles env then
+      check_cycles env t_name hints
+    else
+      env
+  in
+  let env =
+    let (env, ty_err_opt2, tys) =
       List.fold_left
         hints
-        ~init:(env, None, [], [])
-        ~f:(fun (env, ty_err_opt2, cycles, tys) hint ->
-          let ((env, new_ty_err_opt2, new_cycles), ty) =
-            (* This also detects cyclic definitions *)
-            Phase.localize_hint_no_subst_report_cycles
-              env
-              ~ignore_errors:false
-              ~report_cycle:
-                (t_pos, Type_expansions.Expandable.Type_alias t_name_)
-              hint
+        ~init:(env, None, [])
+        ~f:(fun (env, ty_err_opt2, tys) hint ->
+          let ((env, new_ty_err_opt2), ty) =
+            Phase.localize_hint_no_subst env ~ignore_errors:false hint
           in
           ( env,
             Option.merge ~f:Typing_error.both new_ty_err_opt2 ty_err_opt2,
-            new_cycles @ cycles,
             ty :: tys ))
     in
-    if do_report_cycles env then
-      Type_expansions.report cycles
-      |> Option.iter ~f:(Typing_error_utils.add_typing_error ~env);
     let env = casetype_def env typedef in
     Option.iter ~f:(Typing_error_utils.add_typing_error ~env) ty_err_opt2;
 

hphp/hack/test/typecheck/case_type/recursive/bound_check1.php

@@ -0,0 +1,5 @@
+<?hh
+<<file: __EnableUnstableFeatures('case_types')>>
+
+case type CT1 as shape(?'a' => nonnull) = shape(?'a' => CT1);
+case type CT2 as shape(?'a' => shape(?'a' => nonnull)) = shape(?'a' => CT2);

hphp/hack/test/typecheck/case_type/recursive/bound_check1.php.exp

@@ -0,0 +1 @@
+No errors

hphp/hack/test/typecheck/case_type/recursive/empty_types1.php.exp

@@ -44,13 +44,13 @@ ERROR: File "empty_types1.php", line 27, characters 20-29:
 Invalid type hint (Typing[4062])
   File "empty_types1.php", line 27, characters 29-29:
   You are trying to access the type constant `T` but this is a mixed value
-  File "empty_types1.php", line 27, characters 21-29:
+  File "empty_types1.php", line 27, characters 11-16:
   Definition is here
 ERROR: File "empty_types1.php", line 28, characters 21-30:
 Invalid type hint (Typing[4062])
   File "empty_types1.php", line 28, characters 30-30:
   You are trying to access the type constant `T` but this is a mixed value
-  File "empty_types1.php", line 28, characters 21-30:
+  File "empty_types1.php", line 28, characters 11-17:
   Definition is here
 ERROR: File "empty_types1.php", line 29, characters 11-15:
 Invalid case type declaration. More than one variant of `Acces` could contain values with the same runtime tag (Typing[4475])

hphp/hack/test/typecheck/case_type/recursive/subtyping_simple1c.php.exp

@@ -1,8 +1,2 @@
 ERROR: File "subtyping_simple1c.php", line 4, characters 11-11:
-Invalid constraint on `newtype` (Typing[4332])
-  File "subtyping_simple1c.php", line 4, characters 16-21:
-  Expected `string`
-  File "subtyping_simple1c.php", line 4, characters 25-25:
-  But got `mixed`. Using `mixed` instead of A because this is an illegal recursive use of A in the definition of A
-ERROR: File "subtyping_simple1c.php", line 4, characters 11-11:
 This recursive case type is not supported. `A` should not be at the top-level. (Typing[4485])

hphp/hack/test/typecheck/case_type/recursive/subtyping_simple2b.php.exp

@@ -6,9 +6,3 @@ Invalid case type declaration. More than one variant of `A` could contain values
     via this variant of the case type `A`
   File "subtyping_simple2b.php", line 5, characters 5-7:
   It overlaps with `int`, which also includes **ints**
-ERROR: File "subtyping_simple2b.php", line 4, characters 11-11:
-Invalid constraint on `newtype` (Typing[4332])
-  File "subtyping_simple2b.php", line 4, characters 16-18:
-  Expected `int`
-  File "subtyping_simple2b.php", line 4, characters 22-22:
-  But got `mixed`. Using `mixed` instead of A because this is an illegal recursive use of A in the definition of A