well founded recursion for size on rose trees

RoseTreeWF.idr

%default total 

-- Our type of rose trees.
data PfTree : Type -> Type where
  Grow : a -> List (PfTree a) -> PfTree a

-- We want to show that recursion on rose trees is well-founded.
-- This is a little tricky. Idris has pre-existing well-founded proofs in the
-- prelude (WellFounded.idr). These are designed in such a way that if one can
-- conform to a 'Sized' interface, then the proof of well founded recursion is
-- subsequently implied. Sized requires conformance to `size : a -> Nat`.

-- Firstly, there is a pre-existing implementation of 'Sized (List a)' in the
-- Idris prelude. We need to define a named implementation for Lists of
-- PfTrees in order to avoid overlapping instances.
implementation [pftreesize] Sized (List (PfTree a)) where
  size [] = S Z 
  size (Grow e ys :: xs) = 
    let s = size ys
        rec = size xs
    in s + rec 

-- Once we've shown that a list of PfTrees conforms to Sized then showing that
-- a single PfTree is Sized is easy (it's just a wrapper around a List!)
implementation Sized (PfTree a) using pftreesize where
  size (Grow e xs) = size xs

-- and here we have some examples and corresponding proofs!
ex : PfTree Bool
ex = Grow True [Grow True [], Grow False [Grow True []]]

ex2 : PfTree Bool
ex2 = Grow True [Grow True [], Grow True []]

check : size (Grow True [Grow True [], Grow False [Grow True []]]) = 4
check = Refl

check2 : size (Grow True [Grow True [], Grow True []]) = 3
check2 = Refl

-- NOTE! size ex = 4 does not typecheck! Is this a bug!?