Do not re-build type for or-pattern if a ground type annotation is given

[garrigue]

This is an alternative fix to #11799 : rather than introduce a new behavior in case of failure, do not reconstruct the type if a ground type annotation is given. This one is conservative, as build_as_type already honors type annotations: if a ground type annotation is given, then the only possible type is that one.

See #11799 (comment) for a discussion leading to this approach.

[gasche]

I believe that the implementation is correct, but a bit unclear -- see inline comment.

It is nice that this change makes unrelated parts of the testsuite pass -- that were testing a typing failure involving GADTs under an annotation under an as-pattern.

[gasche]

I wish the in () part at the end was rewritten into in ignore t to silence the warning.

[gasche]

Two remarks:

1. There should be a comment here that points to the current PR, otherwise people reading the code in the future will have a hard time guessing why we special-case on ground constraints.

2. It is not clear when reading the code why newgenvar() is a reasonable choice here. I would have rather expected (an instance of) the cty.ctyp_type that was found above. If I understand correctly, the two are in fact equivalent because of the unification that happens below. This makes the code a bit convoluted in my opinion. I think you should either:

• rewrite it to be clearer
• or add a comment to explain why newgenvar() is acceptable here

Here would be a potential suggestion for a clearer implementation (sketch, untested).

  (* 11799, 12313: in the case of [(p : ty) as x] where [ty] is a ground type,
     we can return [ty] right away. *)
  let ground_constraint =
    List.find_map (function
    | Tpat_constrat {ctyp_type = ty}; _, _, _ when free_variables ty = [] -> Some ty
    | _ -> None
    ) p.pat_extra
  in
  match ground_constraint with
  | Some ty -> instance ty
  | None ->
     let as_ty = build_as_type_aux env p in
     List.fold_left ...

[gasche]

(Actually pointing at #11799 (comment) could be even more informative)

[garrigue]

The code you suggest is actually wrong: there might also be non-ground type annotations, and they might result in a different type from the point of view of ambivalence, so we must keep them. So better explain that do some extra work.
I added comments, in particular for the clearly wrong statement about unification below.

[gasche]

Okay, new attempt:

let rec build_as_type (env : Env.t) p =
  build_as_type_extra env p p.pat_extra

and build_as_type_extra env p = function
  | [] -> build_as_type_aux env p
  | (Tpat_type _ | Tpat_open _ | Tpat_unpack) :: rest ->
    build_as_type_extra env p rest
  | Tpat_constraint {cty_type = ty; _} :: _ when free_variables ty = [] ->
    (* TODO some explanation for this special case here *)
    instance ty
  | Tpat_constraint cty :: rest ->
    let as_ty = build_as_type_extra env p rest in
    (* [generic_instance] can only be used if the variables of the original
       type ([cty.ctyp_type] here) are not at [generic_level], which they are
       here.
       If we used [generic_instance] we would lose the sharing between
       [instance ty] and [ty].  *)
    let ty =
      with_local_level ~post:generalize_structure
        (fun () -> instance cty.ctyp_type)
    in
    (* This call to unify may only fail due to missing GADT equations *)
    unify_pat_types p.pat_loc env (instance as_ty) (instance ty);
    ty

[gasche]

(One reason why I find the current code unclear is that the as_ty variable does not have a clear specification, it only has meaning when has_ground_constraint is false.)

[garrigue]

OK, it goes against my policy of minimal textual change, but your code is fine so I'll use it...
Feels a bit CPS though..

[garrigue]

Followed suggestion and rebased.

[gasche]

Merged, thanks!