Par : Node_Id;
       S   : Entity_Id;
 
+      Check_Disabled : constant Boolean := (not Predicate_Enabled (Typ))
+        or else not Predicate_Check_In_Scope (N);
    begin
-      if not Predicate_Enabled (Typ)
-        or else not Predicate_Check_In_Scope (N)
-      then
-         return;
-      end if;
-
       S := Current_Scope;
       while Present (S) and then not Is_Subprogram (S) loop
          S := Scope (S);
       --  If the check appears within the predicate function itself, it means
       --  that the user specified a check whose formal is the predicated
       --  subtype itself, rather than some covering type. This is likely to be
-      --  a common error, and thus deserves a warning.
+      --  a common error, and thus deserves a warning. We want to emit this
+      --  warning even if predicate checking is disabled (in which case the
+      --  warning is still useful even if it is not strictly accurate).
 
       if Present (S) and then S = Predicate_Function (Typ) then
          Error_Msg_NE
                Parent (N), Typ);
          end if;
 
-         Insert_Action (N,
-           Make_Raise_Storage_Error (Sloc (N),
-             Reason => SE_Infinite_Recursion));
+         if not Check_Disabled then
+            Insert_Action (N,
+              Make_Raise_Storage_Error (Sloc (N),
+                Reason => SE_Infinite_Recursion));
+            return;
+         end if;
+      end if;
+
+      if Check_Disabled then
          return;
       end if;
 
 
       Exp : Node_Id := Expression (N);
       pragma Assert (Present (Exp));
 
+      Exp_Is_Function_Call : constant Boolean :=
+        Nkind (Exp) = N_Function_Call
+          or else (Nkind (Exp) = N_Explicit_Dereference
+                   and then Is_Entity_Name (Prefix (Exp))
+                   and then Ekind (Entity (Prefix (Exp))) = E_Constant
+                   and then Is_Related_To_Func_Return (Entity (Prefix (Exp))));
+
       Exp_Typ : constant Entity_Id := Etype (Exp);
       --  The type of the expression (not necessarily the same as R_Type)
 
             Decl : Node_Id;
             Ent  : Entity_Id;
          begin
-            if Nkind (Exp) /= N_Function_Call
+            if not Exp_Is_Function_Call
               and then Has_Discriminants (Ubt)
               and then not Is_Constrained (Ubt)
               and then not Has_Unchecked_Union (Ubt)
               (not Is_Array_Type (Exp_Typ)
                 or else Is_Constrained (Exp_Typ) = Is_Constrained (R_Type)
                 or else CW_Or_Has_Controlled_Part (Utyp))
-           and then Nkind (Exp) = N_Function_Call
+           and then Exp_Is_Function_Call
          then
             Set_By_Ref (N);
 
 
       --  the predicate still applies.
 
       if not Suppress_Assignment_Checks (N)
-        and then Predicate_Enabled (T)
+        and then (Predicate_Enabled (T) or else Has_Static_Predicate (T))
         and then
           (not No_Initialization (N)
             or else (Present (E) and then Nkind (E) = N_Aggregate))
       then
          --  If the type has a static predicate and the expression is known at
          --  compile time, see if the expression satisfies the predicate.
+         --  In the case of a static expression, this must be done even if
+         --  the predicate is not enabled (as per static expression rules).
 
          if Present (E) then
             Check_Expression_Against_Static_Predicate (E, T);
          end if;
 
+         --  Do not perform further predicate-related checks unless
+         --  predicates are enabled for the subtype.
+
+         if not Predicate_Enabled (T) then
+            null;
+
          --  If the type is a null record and there is no explicit initial
          --  expression, no predicate check applies.
 
-         if No (E) and then Is_Null_Record_Type (T) then
+         elsif No (E) and then Is_Null_Record_Type (T) then
             null;
 
          --  Do not generate a predicate check if the initialization expression
 
          Set_Has_Pragma_Unreferenced_Objects
                                      (Priv, Has_Pragma_Unreferenced_Objects
                                                                        (Full));
+         Set_Predicates_Ignored      (Priv, Predicates_Ignored         (Full));
          if Is_Unchecked_Union (Full) then
             Set_Is_Unchecked_Union (Base_Type (Priv));
          end if;
 
          --  is folded, and since this is definitely a failure, extra checks
          --  are OK.
 
-         Insert_Action (Expr,
-           Make_Predicate_Check
-             (Typ, Duplicate_Subexpr (Expr)), Suppress => All_Checks);
+         if Predicate_Enabled (Typ) then
+            Insert_Action (Expr,
+              Make_Predicate_Check
+                (Typ, Duplicate_Subexpr (Expr)), Suppress => All_Checks);
+         end if;
       end if;
    end Check_Expression_Against_Static_Predicate;
 
 
             Set_Has_Delayed_Freeze (Typ);
 
             Set_Predicates_Ignored (Typ,
-              Present (Check_Policy_List)
-                and then
-                  Policy_In_Effect (Name_Dynamic_Predicate) = Name_Ignore);
+              Policy_In_Effect (Name_Dynamic_Predicate) = Name_Ignore);
             Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
          end Predicate;