Skip to content

Tactics plugin fails to solve program involving two different instantiations for fmap #561

Closed
@siraben

Description

@siraben

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.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions