Closed
Description
Consider
data Fix f a = Fix (f (Fix f a))
instance Functor f => Functor (Fix f) where
fmap f (Fix x) = _
The tactics plugin fails to fill the hole. One potential solution would be
instance Functor f => Functor (Fix f) where
fmap f (Fix x) = Fix (fmap (fmap f) x)
Where the first fmap
is on the functor f
and the second fmap
is on the functor Fix f
(i.e. recursive call for this instance of fmap
). According to @isovector the two different types for fmap
combined with the way recursive calls are handled result in the tactic plugin failing to find a solution.
This has been tested as of commit 6c14163.