Translating Definitions of Applicative and Functor instances based on Control.Monad

[lastland]

The following way of declaring a monad instance is quite common in Haskell:

instance Monad Hp where
  return = returnHp
  m >>= f = bindHp m f

instance Applicative Hp where
  pure = return
  (<*>) = ap

instance Functor Hp where
  fmap = liftM

However, it cannot be translated to Coq directly using hs-to-coq. Reordering would not help, either, because of the entangled dependency.

[nomeata]

I don't think an automatic solution will happen any time soon. You can redefine (rename? rewrite?) Applicative_Hp__ap to Monad_Hp__return, that should work.