Wingman doesn't introduce new skolems for existentially bound variables

[isovector]

@masaeedu points out:

{-# LANGUAGE DataKinds, GADTs #-}

data Z ab where
  Z :: (a -> b) -> Z '(a, b)

test :: Z ab
test = _

produces

test = Z id

But it doesn't typecheck.

What's going wrong here? When we introduce the Z constructor, we should generate two new skolems a and b such that '(a, b) ~ ab. But instead we generate two new unification variables, which are thus free to unify with one another, and thus produce the bogus id.

[isovector]

data Z ab = forall a b. ab ~ '(a, b) => Z (a -> b)

also triggers it, so I'm guessing the theta evidence needs to be updated.

[isovector]

This also fails when there are no unknown variables in sight. Another example:

data A = A
data B = B
data X = X
data Y = Y


data Pairrow ax by  where
  Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y)

test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y)
test2 = _

The problem here appears to be in buildDataCon when building a Pairrow:

haskell-language-server/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

Line 192 in 607ae3b

let args = conLikeInstOrigArgTys' dc tyapps

the generated holes here have types a -> b and x -> y, but they SHOULD be A -> B and X -> Y. Unification isn't kicking in here.

[isovector]

I think the answer is to unify whatever newly introduced type variables we can, and then introduce the remainder as skolems in ts_skolems (to prevent them from unifying with one another.)

[isovector]

Looks like instantiation happens via https://hackage.haskell.org/package/ghc-8.8.1/docs/DataCon.html#v:dataConInstSig, which doesn't exist for ConLikes... yet. Additionally, this returns the resulting ThetaType which can be turned into evidence for type equalities.

[isovector]

So to put it all together, the play is to write conLikeInstSig, call it, turn the resulting ThetaType into evidence, compute the substitution from that evidence, and apply it to the new goals.

But it's not clear to me how this interacts with the original example. In that case we'll get an evidence of EqualityOfTypes ab '(a, b), and from that and the fact that we know ab is a skolem, transfer skolem-itude to a and b. But is that always valid?

[isovector]

Note to myself: when CONSTRUCTING a GADT that contains existential values, they are universal! You can choose anything you'd like to replace them! So there is no "skolemize any leftover newly bound variables" step.

And then this answers the when to skolemize question. Yes, if you have an equality of types with a skolem, those new tyvars should be skolems assuming the unification isn't trivial. Eg, if we have

ab ~ new

then this is trivial and we should just rewrite new => ab.

But in the case that

ab ~ new_f new_a new_b

then yes, absolutely, now we have introduced new variables and they should be skolems.

[isovector]

There's a related bug here, with the evidence that comes from dictionaries. Those should be emitted as holes, so that Wingman must solve the dictionaries in order to synthesize the term. Wingman doesn't solve dictionaries right now though.

[isovector]

Using dataConInstSig does indeed solve the problem with skolems and with bad unification. But there is no equivalent for conlikes, so I'll need to figure out how to implement it myself.