Recursive definition of size is ill-formed.
In environment
size : P -> nat
d : P
p : box P
tu : box match tt with
         | tt => P
         end
Recursive call to size has principal argument equal to "let 'box_intro _ tu' := tu in tu'" instead of one of the following variables: "p" "tu".
Recursive definition is: "fun '(P_intro p) => match tt as t return (box match t with
                                                                        | tt => P
                                                                        end -> nat) with
                                              | tt => fun tu : box match tt with
                                                                   | tt => P
                                                                   end => size (let 'box_intro _ tu' := tu in tu')
                                              end p".