Fix unification pertaining to evidence (#1885)

* 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

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: isovector

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

@@ -19,7 +19,6 @@ import           Data.Bool (bool)
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
 import           Data.List
-import           Data.Monoid (Endo(..))
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
@@ -68,7 +67,7 @@ destructMatches use_field_puns f scrut t jdg = do
             -- #syn_scoped
             method_hy = foldMap evidenceToHypothesis ev
             args = conLikeInstOrigArgTys' con apps
-        modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
+        modify $ evidenceToSubst ev
         subst <- gets ts_unifier
         ctx <- ask
 

plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs

@@ -12,13 +12,16 @@ module Wingman.Judgements.Theta
 
 import           Class (classTyVars)
 import           Control.Applicative (empty)
+import           Control.Lens (preview)
 import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)
+import           Data.Generics.Sum (_Ctor)
 import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           Generics.SYB hiding (tyConName, empty)
-import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
+import           Generics.SYB hiding (tyConName, empty, Generic)
+import           GHC.Generics
+import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst)
 #if __GLASGOW_HASKELL__ > 806
 import           GhcPlugins (eqTyCon)
 #else
@@ -40,7 +43,7 @@ data Evidence
   = EqualityOfTypes Type Type
     -- | We have an instance in scope
   | HasInstance PredType
-  deriving (Show)
+  deriving (Show, Generic)
 
 
 ------------------------------------------------------------------------------
@@ -75,21 +78,46 @@ getEvidenceAtHole (unTrack -> dst)
   . unTrack
 
 
-------------------------------------------------------------------------------
--- | Update our knowledge of which types are equal.
-evidenceToSubst :: Evidence -> TacticState -> TacticState
-evidenceToSubst (EqualityOfTypes a b) ts =
+mkSubst :: Set TyVar -> Type -> Type -> TCvSubst
+mkSubst skolems a b =
   let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b]
       -- If we can unify our skolems, at least one is no longer a skolem.
       -- Removing them from this set ensures we can get a subtitution between
       -- the two. But it's okay to leave them in 'ts_skolems' in general, since
       -- they won't exist after running this substitution.
-      skolems = ts_skolems ts S.\\ tyvars
+      skolems' = skolems S.\\ tyvars
    in
-  case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
-    Just subst -> updateSubst subst ts
-    Nothing -> ts
-evidenceToSubst HasInstance{} ts = ts
+  case tryUnifyUnivarsButNotSkolems skolems' (CType a) (CType b) of
+    Just subst -> subst
+    Nothing -> emptyTCvSubst
+
+
+substPair :: TCvSubst -> (Type, Type) -> (Type, Type)
+substPair subst (ty, ty') = (substTy subst ty, substTy subst ty')
+
+
+------------------------------------------------------------------------------
+-- | Construct a substitution given a list of types that are equal to one
+-- another. This is more subtle than it seems, since there might be several
+-- equalities for the same type. We must be careful to push the accumulating
+-- substitution through each pair of types before adding their equalities.
+allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst
+allEvidenceToSubst _ [] = emptyTCvSubst
+allEvidenceToSubst skolems ((a, b) : evs) =
+  let subst = mkSubst skolems a b
+   in unionTCvSubst subst
+    $ allEvidenceToSubst skolems
+    $ fmap (substPair subst) evs
+
+------------------------------------------------------------------------------
+-- | Update our knowledge of which types are equal.
+evidenceToSubst :: [Evidence] -> TacticState -> TacticState
+evidenceToSubst evs ts =
+  updateSubst
+    (allEvidenceToSubst (ts_skolems ts)
+      $ mapMaybe (preview $ _Ctor @"EqualityOfTypes")
+      $ evs)
+    ts
 
 
 ------------------------------------------------------------------------------

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

@@ -272,7 +272,7 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
                $ hypothesisFromBindings binds_rss binds
       evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
-      subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
+      subst = ts_unifier $ evidenceToSubst evidence defaultTacticState
   pure $
     ( disallowing AlreadyDestructed already_destructed
     $ fmap (CType . substTyAddInScope subst . unCType) $

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

@@ -121,7 +121,9 @@ tacticCmd tac pId state (TacticParams uri range var_name)
 
         timingOut (cfg_timeout_seconds cfg * seconds) $ join $
           case runTactic hj_ctx hj_jdg t of
-            Left _ -> Left TacticErrors
+            Left errs ->  do
+              traceMX "errs" errs
+              Left TacticErrors
             Right rtr ->
               case rtr_extract rtr of
                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->

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

@@ -11,7 +11,7 @@ import           Control.Lens ((&), (%~), (<>~))
 import           Control.Monad (unless)
 import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader (ask))
-import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Control.Monad.State.Strict (StateT(..), runStateT, gets)
 import           Data.Bool (bool)
 import           Data.Foldable
 import           Data.Functor ((<&>))
@@ -161,7 +161,7 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
   attemptWhen
       (rule $ destruct' False (\dc jdg ->
         buildDataCon False jdg dc $ snd $ splitAppTys g) hi)
-      (rule $ destruct' False (const subgoal) hi)
+      (rule $ destruct' False (const newSubgoal) hi)
     $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of
         (Just (gtc, _), Just (tytc, _)) -> gtc == tytc
         _ -> False
@@ -171,14 +171,14 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
 -- | Case split, and leave holes in the matches.
 destruct :: HyInfo CType -> TacticsM ()
 destruct hi = requireConcreteHole $ tracing "destruct(user)" $
-  rule $ destruct' False (const subgoal) hi
+  rule $ destruct' False (const newSubgoal) hi
 
 
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches. Performs record punning.
 destructPun :: HyInfo CType -> TacticsM ()
 destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $
-  rule $ destruct' True (const subgoal) hi
+  rule $ destruct' True (const newSubgoal) hi
 
 
 ------------------------------------------------------------------------------
@@ -192,7 +192,7 @@ homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->
 -- | LambdaCase split, and leave holes in the matches.
 destructLambdaCase :: TacticsM ()
 destructLambdaCase =
-  tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const subgoal)
+  tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const newSubgoal)
 
 
 ------------------------------------------------------------------------------
@@ -336,7 +336,7 @@ destructAll :: TacticsM ()
 destructAll = do
   jdg <- goal
   let args = fmap fst
-           $ sort
+           $ sortOn snd
            $ mapMaybe (\(hi, prov) ->
               case prov of
                 TopLevelArgPrv _ idx _ -> pure (hi, idx)
@@ -346,7 +346,9 @@ destructAll = do
            $ filter (isAlgType . unCType . hi_type)
            $ unHypothesis
            $ jHypothesis jdg
-  for_ args destruct
+  for_ args $ \arg -> do
+    subst <- gets ts_unifier
+    destruct $ fmap (coerce substTy subst) arg
 
 --------------------------------------------------------------------------------
 -- | User-facing tactic to implement "Use constructor <x>"

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

@@ -65,6 +65,7 @@ spec = do
     autoTest  6  8 "AutoThetaEqGADTDestruct"
     autoTest  6 10 "AutoThetaRefl"
     autoTest  6  8 "AutoThetaReflDestruct"
+    autoTest 19 30 "AutoThetaMultipleUnification"
 
   describe "known" $ do
     autoTest 25 13 "GoldenArbitrary"

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

@@ -34,4 +34,5 @@ spec = do
     destructAllTest 4 23 "DestructAllMany"
     destructAllTest 2 18 "DestructAllNonVarTopMatch"
     destructAllTest 2 18 "DestructAllFunc"
+    destructAllTest 19 18 "DestructAllGADTEvidence"
 

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

@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp AtZ (HCons t _) = t
+lookMeUp (AtS ea') (HCons t hl') = _
+

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

@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp AtZ (HCons t hl') = _
+lookMeUp (AtS ea') (HCons t hl') = _
+

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

@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp AtZ (HCons t hl') = _
+lookMeUp (AtS ea') (HCons t hl') = _
+