Comment by GregarianChild

I'm not an expert in this field, but the way I understand it is that Choice Trees extend the ITree signature by adding a choice operator. Some variant of this:

ITrees:

    CoInductive itree (E : Type -> Type) (R : Type) : Type :=
    | Ret (r : R)                                                                                                                                                                                                         
    | Tau (t : itree E R)                                                                                                                                                                                                 
    | Vis {T : Type} (e : E T) (k : T -> itree E R)                                                                                                                                                                       

ChoiceTrees:

    CoInductive ctree (E : Type -> Type) (C : Type -> Type) (R : Type) : Type :=
    | Ret (r : R)                                                                                                                                                                                                         
    | Tau (t : ctree E C R)                                                                                                                                                                                               
    | Vis {T : Type} (e : E T) (k : T -> ctree E C R)                                                                                                                                                                     
    | Choice {T : Type} (c : C T) (k : T -> ctree E C R)                                                                                                                                                                  

One can see "Choice" constructor as modelling internal non-determinism, complementing the external non-determinism that ITrees already allow with "Vis" and that arises from interaction with the environment. (Process calculi like CCS, CSP and Pi, as well as session types and linear logic also make this distinction).