Wingman: FIx evidence when using GADT constructors (#1889)

* Fix unification pertaining to evidence

* Cleanup interface; better names

* Need to reapply the substituion after each arg

* Reenable error debugging

* Add destruct_all evidence test

* Fix tests that were accidentally sorted incorrectly

* FIx evidence when splitting GADTs

Author: isovector

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

@@ -253,7 +253,22 @@ buildDataCon
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (Synthesized (LHsExpr GhcPs))
 buildDataCon should_blacklist jdg dc tyapps = do
-  let args = conLikeInstOrigArgTys' dc tyapps
+  args <- case dc of
+    RealDataCon dc' -> do
+      let (skolems', theta, args) = dataConInstSig dc' tyapps
+      modify $ \ts ->
+        evidenceToSubst (foldMap mkEvidence theta) ts
+          & #ts_skolems <>~ S.fromList skolems'
+      pure args
+    _ ->
+      -- If we have a 'PatSyn', we can't continue, since there is no
+      -- 'dataConInstSig' equivalent for 'PatSyn's. I don't think this is
+      -- a fundamental problem, but I don't know enough about the GHC internals
+      -- to implement it myself.
+      --
+      -- Fortunately, this isn't an issue in practice, since 'PatSyn's are
+      -- never in the hypothesis.
+      throwError $ TacticPanic "Can't build Pattern constructors yet"
   ext
       <- fmap unzipTrace
        $ traverse ( \(arg, n) ->

plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs

@@ -66,6 +66,7 @@ spec = do
     autoTest  6 10 "AutoThetaRefl"
     autoTest  6  8 "AutoThetaReflDestruct"
     autoTest 19 30 "AutoThetaMultipleUnification"
+    autoTest 16  9 "AutoThetaSplitUnification"
 
   describe "known" $ do
     autoTest 25 13 "GoldenArbitrary"
@@ -83,4 +84,5 @@ spec = do
 
   describe "messages" $ do
     mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA" TacticErrors
+    mkShowMessageTest allFeatures Auto "" 7 8 "MessageCantUnify" TacticErrors
 

plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.expected.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+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 = Pairrow
+

plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+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 = _
+

plugins/hls-tactics-plugin/test/golden/MessageCantUnify.hs

@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, GADTs #-}
+
+data Z ab where
+  Z :: (a -> b) -> Z '(a, b)
+
+test :: Z ab
+test = _
+