You are quite right.  I went back to even PDDL 2, and this nesting is, as you 
say, prohibited by the grammar.

My apologies.  I will change this to "wish" request.  Please think about it: I 
will quite understand if you just close it as WONTFIX.  The macro/machine-
generated code argument is a reason to permit this.  But such constructs could be 
flattened in a preprocessing step.  The need is no longer so pressing for me, 
anyway.

I am not sure whether this is really a bug.

An effect of the form
(forall (?X - foo)
  (when (pred ?X)
    (forall (?Y - bar)
      ....)))
would at least not be allowed by the BNF for PDDL 3.0:

A conditional effect can only have a <cond-effect> as sub-effect. A
<cond-effect> is (in the non-numerical case) a conjunction of literals
(<p-effect>s).

So I would classify this as a feature request. I do not know whether we should
support this in the planner, or whether we leave the reformulation to the author
of the domain. I think it would be nice to support it directly in the planner
but I do not see that we have the resources to do this anytime soon (also given
that the bug is more than a year old).

Thanks, Robert! I would indeed reclassify this as a bug; there are some PDDL
features we intentionally do not support (since for now we thought it'd be too
much work to implement them), but this is one we thought we supported properly.
So not just a missing feature but a bug.

Three attached files:  trap.pddl and login-problem.pddl pass through translate.py.  
trap-nested.pddl and login-problem.pddl do NOT.

fast downward will not allow me to have an effect of the following form

(forall (?X - foo)
  (when (pred ?X)
    (forall (?Y - bar)
      ....)))

I believe that when parsing, effects.py checks to see if a quantified
effect contains either (a) a simple effect or (b) a conditional effect
(line 170).

Would this be difficult to change?

I have a somewhat oddball reason to request this:  in my domain, the
nested FORALL in the above example is generated by a macro.  This
permits me to put the same code (representing a single ramification)
in multiple places in my PDDL file.  If I am forced to lift the nested
quantifier out above the when (which works), then I cannot use a macro
to repeat the same logic in multiple places.  This exposes my PDDL
domain to errors that arise from inconsistencies in multiple copies of
the same logic.

Here's the exact example:

  (and
    (not (authenticated ?U ?O))
    (console_user nobody nouid ?O)
    (not (console_user ?H ?U ?O))
    (and (forall (?HH - c_host) (not (has_session ?HH ?Sess)))
            (forall (?PP - c_process) (not (session_process ?Sess ?PP)))
            (forall (?HH - c_human) (not (session_owner ?Sess ?HH))))
    (forall (?P - c_process)
      (when (session_process ?Sess ?P)
         ;; this seems to be the problematic line:
        (forall (?U - c_uid ?Prog - c_program)
          (and (when (euid ?O ?P ?U) (not (euid ?O ?P ?U)))
             (when (running_prog ?O ?P ?Prog)
               (not (running_prog ?O ?P ?Prog)))
             (not (has_process ?O ?P))))))
  ))

This version parses successfully:
  :effect
  (and
    (not (authenticated ?U ?O))
    (console_user nobody nouid ?O)
    (not (console_user ?H ?U ?O))
    (and (forall (?HH - c_host) (not (has_session ?HH ?Sess)))
           (forall (?PP - c_process) (not (session_process ?Sess ?
PP)))
           (forall (?HH - c_human) (not (session_owner ?Sess ?HH))))
    (forall (?P - c_process ?U - c_uid ?Prog - c_program)
      (when (session_process ?Sess ?P)
          (and (when (euid ?O ?P ?U) (not (euid ?O ?P ?U)))
               (when (running_prog ?O ?P ?Prog)
               (not (running_prog ?O ?P ?Prog)))
               (not (has_process ?O ?P)))))
  ))

The logic is that I have a macro that says what it means to kill a
process: remove assertions about its euid, remove the assertion(s)
about the program(s) it runs, and delete it from the list of processes
on a host.  I have an operator that kills a session (?Sess), and I
want to quantify over the processes in that session.  (Similarly, the
nested conjunction in the above effect is what happens when you expand
the macro that says what it means to kill a session....)

I'm calling this a "feature," although it's arguably a bug: FD is rejecting what 
appears to be well-formed PDDL.