Fix unification pertaining to evidence

Author: isovector

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

@@ -18,7 +18,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
@@ -67,7 +66,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
 
         let names_in_scope = hyNamesInScope hy

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

@@ -18,7 +18,7 @@ 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           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst)
 #if __GLASGOW_HASKELL__ > 806
 import           GhcPlugins (eqTyCon)
 #else
@@ -77,8 +77,8 @@ getEvidenceAtHole (unTrack -> dst)
 
 ------------------------------------------------------------------------------
 -- | Update our knowledge of which types are equal.
-evidenceToSubst :: Evidence -> TacticState -> TacticState
-evidenceToSubst (EqualityOfTypes a b) ts =
+hi :: Evidence -> TacticState -> TacticState
+hi (EqualityOfTypes a b) ts =
   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
@@ -89,7 +89,22 @@ evidenceToSubst (EqualityOfTypes a b) ts =
   case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
     Just subst -> updateSubst subst ts
     Nothing -> ts
-evidenceToSubst HasInstance{} ts = ts
+hi HasInstance{} ts = ts
+
+substEvidence :: TCvSubst -> Evidence -> Evidence
+substEvidence subst (EqualityOfTypes ty ty') =
+  EqualityOfTypes (substTy subst ty) (substTy subst ty')
+substEvidence _ x = x
+
+allEvidenceToSubst :: [Evidence] -> TCvSubst
+allEvidenceToSubst [] = emptyTCvSubst
+allEvidenceToSubst (HasInstance{} : evs) = allEvidenceToSubst evs
+allEvidenceToSubst (eq@EqualityOfTypes{} : evs) =
+  let subst = ts_unifier $ hi eq defaultTacticState
+   in unionTCvSubst subst $ allEvidenceToSubst $ fmap (substEvidence subst) evs
+
+evidenceToSubst :: [Evidence] -> TacticState -> TacticState
+evidenceToSubst = updateSubst . allEvidenceToSubst
 
 
 ------------------------------------------------------------------------------

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

@@ -270,9 +270,9 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
       already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs
       local_hy = spliceProvenance top_provs
                $ hypothesisFromBindings binds_rss binds
-      evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
+      evidence = traceIdX "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) $ mkFirstJudgement

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/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') = _
+