Wingman incorrectly unifies skolems across apart GADT matches

[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?

[isovector]

I've always wondered, but maybe this is what coercions do. If they exist at the value level, then they'd go out of scope between the GADT matches. Maybe we can do something similar, tracking coercions in the Judgement, and combining their evidence with the TacticState unification just in time.

[isovector]

On further thought, I don't think this is directly related to the TacticState at all. The only time we change the TCvSubst is for type variables that are not skolems, which means it's definitely the GADT evidence going wrong here. I think those get directly injected into the ts_subst, rather than doing anything scoped.