I was writing the VerifiedMonad and VerifiedFunctor typeclasses (you
can see my full code here: https://gist.github.com/3316784 ) . The
problem was initially with the identity Functor law, which would not
typecheck like this:

-- "Incomplete term" error
class Functor f => VerifiedFunctor (f : Set -> Set) where
  identity : (fa : f a) -> fmap id fa = fa

However, it did work like this:

class Functor f => VerifiedFunctor (f : Set -> Set) where
  identity : (fa : f a) -> fmapid fa = fa

-- Need this to avoid "Incomplete term" error
fmapid : Functor f => f a -> f a
fmapid = fmap id

I had the same issue with (>>= return) which was fixed similarly.

Regards,

Alan