Skip to content

Wingman incorrectly unifies skolems across apart GADT matches #1937

Closed
@isovector

Description

@isovector
data AST a where
    BoolLit :: Bool -> AST Bool
    IntLit :: Int -> AST Int

eval :: AST a -> a
eval = [wingman| intros x, destruct x |]

with resulting goals:

2 goals

b :: Bool  
⊢ Bool

n :: Int  
⊢ Bool

Except that no! That second goal should be ⊢ Int.

What's happening here is that unification gets tracked in the TacticState, which is shared across the entire search tree. Thus, in the first branch, we learn that a ~ Bool, and this fact never gets invalidated when we enter the IntLit case.

@TOTBWF any good idea about what to do here?

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