"Incomplete term" error

[Alan Pogrebinschi]

Hi,

I just started playing with Idris and got an error the I could isolate in this short repl session:

Idris> fmap (+ 5) (Just 1)

Just 6 : Maybe Int

Idris> fmap id (Just 1)

(input):0:Incomplete term fmap (id) (Just (fromInteger 1))

This works fine in ghci. My original error is in a proper idris module, not in the repl.

I'm using the latest github code.

Any hint?

Thanks,

Alan

[Alan Pogrebinschi]

Just writing to report the (ugly) workaround that I found for this.
However, it does seem to be a bug to me.

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