Skip to content

Wingman case split does the wrong thing on nested binds #1541

Closed
@isovector

Description

@isovector

@TOTBWF reports:

Found a case splitting bug

proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])]
proofs s p = go s [] pure p
    where
      go :: s -> [goal] -> (goal' -> ProofStateT ext ext err s m goal) -> ProofStateT ext ext err s m goal' -> m [Either err (ext, s, [goal])]
      go s goals cont p1  = _

splitting on p1 causes this

proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])]
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _

Metadata

Metadata

Assignees

No one assigned

    Labels

    component: wingmantype: bugSomething isn't right: doesn't work as intended, documentation is missing/outdated, etc..

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions