Addendum to PR#7374: ensure that paths hidden by definitions are chec…

…ked too in local_non_recursive_abbrev

testsuite/tests/typing-gadts/pr7374.ml

@@ -33,3 +33,17 @@ module Bad = Fix(Id)
 let segfault () =
   print_endline (cast (trans (Bad.uniq Refl) (Bad.uniq Refl)) 0)
 *)
+
+(* addendum: ensure that hidden paths are checked too *)
+module F (X : sig type 'a t end) = struct
+  open X
+  let f : type a b. (a, b t) eq -> (b, a t) eq -> (a, a t t) eq =
+    fun Refl Refl -> Refl;;
+end;; (* should fail *)
+[%%expect{|
+Line _, characters 21-25:
+Error: This expression has type (a, a) eq
+       but an expression was expected of type (a, a X.t X.t) eq
+       Type a = b X.t is not compatible with type a X.t X.t
+       Type b is not compatible with type a X.t
+|}]

typing/ctype.ml

@@ -1641,13 +1641,11 @@ let rec local_non_recursive_abbrev strict visited env p ty =
         if Path.same p p' then raise Occur;
         if is_contractive env p' then () else
         let visited = ty :: visited in
-        begin try
-          List.iter (local_non_recursive_abbrev true visited env p) args
-        with Occur -> try
+        begin try (* try expanding first, since [p] could be hidden *)
           local_non_recursive_abbrev strict visited env p
             (try_expand_head try_expand_once env ty)
         with Cannot_expand ->
-          raise Occur
+          List.iter (local_non_recursive_abbrev true visited env p) args
         end
     | _ ->
         if strict then (* PR#7374 *)