Skip to content

Commit 1163ae7

Browse files
isovectormergify[bot]
isovector
and
mergify[bot]
authored
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>
1 parent 4091538 commit 1163ae7

13 files changed

+155
-39
lines changed

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ import Data.Bool (bool)
1919
import Data.Functor ((<&>))
2020
import Data.Generics.Labels ()
2121
import Data.List
22-
import Data.Monoid (Endo(..))
2322
import qualified Data.Set as S
2423
import Data.Traversable
2524
import DataCon
@@ -68,7 +67,7 @@ destructMatches use_field_puns f scrut t jdg = do
6867
-- #syn_scoped
6968
method_hy = foldMap evidenceToHypothesis ev
7069
args = conLikeInstOrigArgTys' con apps
71-
modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
70+
modify $ evidenceToSubst ev
7271
subst <- gets ts_unifier
7372
ctx <- ask
7473

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

Lines changed: 40 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,16 @@ module Wingman.Judgements.Theta
1212

1313
import Class (classTyVars)
1414
import Control.Applicative (empty)
15+
import Control.Lens (preview)
1516
import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
17+
import Data.Generics.Sum (_Ctor)
1618
import Data.Set (Set)
1719
import qualified Data.Set as S
1820
import Development.IDE.Core.UseStale
1921
import Development.IDE.GHC.Compat
20-
import Generics.SYB hiding (tyConName, empty)
21-
import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
22+
import Generics.SYB hiding (tyConName, empty, Generic)
23+
import GHC.Generics
24+
import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst)
2225
#if __GLASGOW_HASKELL__ > 806
2326
import GhcPlugins (eqTyCon)
2427
#else
@@ -40,7 +43,7 @@ data Evidence
4043
= EqualityOfTypes Type Type
4144
-- | We have an instance in scope
4245
| HasInstance PredType
43-
deriving (Show)
46+
deriving (Show, Generic)
4447

4548

4649
------------------------------------------------------------------------------
@@ -75,21 +78,46 @@ getEvidenceAtHole (unTrack -> dst)
7578
. unTrack
7679

7780

78-
------------------------------------------------------------------------------
79-
-- | Update our knowledge of which types are equal.
80-
evidenceToSubst :: Evidence -> TacticState -> TacticState
81-
evidenceToSubst (EqualityOfTypes a b) ts =
81+
mkSubst :: Set TyVar -> Type -> Type -> TCvSubst
82+
mkSubst skolems a b =
8283
let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b]
8384
-- If we can unify our skolems, at least one is no longer a skolem.
8485
-- Removing them from this set ensures we can get a subtitution between
8586
-- the two. But it's okay to leave them in 'ts_skolems' in general, since
8687
-- they won't exist after running this substitution.
87-
skolems = ts_skolems ts S.\\ tyvars
88+
skolems' = skolems S.\\ tyvars
8889
in
89-
case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
90-
Just subst -> updateSubst subst ts
91-
Nothing -> ts
92-
evidenceToSubst HasInstance{} ts = ts
90+
case tryUnifyUnivarsButNotSkolems skolems' (CType a) (CType b) of
91+
Just subst -> subst
92+
Nothing -> emptyTCvSubst
93+
94+
95+
substPair :: TCvSubst -> (Type, Type) -> (Type, Type)
96+
substPair subst (ty, ty') = (substTy subst ty, substTy subst ty')
97+
98+
99+
------------------------------------------------------------------------------
100+
-- | Construct a substitution given a list of types that are equal to one
101+
-- another. This is more subtle than it seems, since there might be several
102+
-- equalities for the same type. We must be careful to push the accumulating
103+
-- substitution through each pair of types before adding their equalities.
104+
allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst
105+
allEvidenceToSubst _ [] = emptyTCvSubst
106+
allEvidenceToSubst skolems ((a, b) : evs) =
107+
let subst = mkSubst skolems a b
108+
in unionTCvSubst subst
109+
$ allEvidenceToSubst skolems
110+
$ fmap (substPair subst) evs
111+
112+
------------------------------------------------------------------------------
113+
-- | Update our knowledge of which types are equal.
114+
evidenceToSubst :: [Evidence] -> TacticState -> TacticState
115+
evidenceToSubst evs ts =
116+
updateSubst
117+
(allEvidenceToSubst (ts_skolems ts)
118+
$ mapMaybe (preview $ _Ctor @"EqualityOfTypes")
119+
$ evs)
120+
ts
93121

94122

95123
------------------------------------------------------------------------------

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -272,7 +272,7 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
272272
$ hypothesisFromBindings binds_rss binds
273273
evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
274274
cls_hy = foldMap evidenceToHypothesis evidence
275-
subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
275+
subst = ts_unifier $ evidenceToSubst evidence defaultTacticState
276276
pure $
277277
( disallowing AlreadyDestructed already_destructed
278278
$ fmap (CType . substTyAddInScope subst . unCType) $

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,9 @@ tacticCmd tac pId state (TacticParams uri range var_name)
121121

122122
timingOut (cfg_timeout_seconds cfg * seconds) $ join $
123123
case runTactic hj_ctx hj_jdg t of
124-
Left _ -> Left TacticErrors
124+
Left errs -> do
125+
traceMX "errs" errs
126+
Left TacticErrors
125127
Right rtr ->
126128
case rtr_extract rtr of
127129
L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->

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

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ import Control.Lens ((&), (%~), (<>~))
1111
import Control.Monad (unless)
1212
import Control.Monad.Except (throwError)
1313
import Control.Monad.Reader.Class (MonadReader (ask))
14-
import Control.Monad.State.Strict (StateT(..), runStateT)
14+
import Control.Monad.State.Strict (StateT(..), runStateT, gets)
1515
import Data.Bool (bool)
1616
import Data.Foldable
1717
import Data.Functor ((<&>))
@@ -161,7 +161,7 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
161161
attemptWhen
162162
(rule $ destruct' False (\dc jdg ->
163163
buildDataCon False jdg dc $ snd $ splitAppTys g) hi)
164-
(rule $ destruct' False (const subgoal) hi)
164+
(rule $ destruct' False (const newSubgoal) hi)
165165
$ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of
166166
(Just (gtc, _), Just (tytc, _)) -> gtc == tytc
167167
_ -> False
@@ -171,14 +171,14 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
171171
-- | Case split, and leave holes in the matches.
172172
destruct :: HyInfo CType -> TacticsM ()
173173
destruct hi = requireConcreteHole $ tracing "destruct(user)" $
174-
rule $ destruct' False (const subgoal) hi
174+
rule $ destruct' False (const newSubgoal) hi
175175

176176

177177
------------------------------------------------------------------------------
178178
-- | Case split, and leave holes in the matches. Performs record punning.
179179
destructPun :: HyInfo CType -> TacticsM ()
180180
destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $
181-
rule $ destruct' True (const subgoal) hi
181+
rule $ destruct' True (const newSubgoal) hi
182182

183183

184184
------------------------------------------------------------------------------
@@ -192,7 +192,7 @@ homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->
192192
-- | LambdaCase split, and leave holes in the matches.
193193
destructLambdaCase :: TacticsM ()
194194
destructLambdaCase =
195-
tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const subgoal)
195+
tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const newSubgoal)
196196

197197

198198
------------------------------------------------------------------------------
@@ -336,7 +336,7 @@ destructAll :: TacticsM ()
336336
destructAll = do
337337
jdg <- goal
338338
let args = fmap fst
339-
$ sort
339+
$ sortOn snd
340340
$ mapMaybe (\(hi, prov) ->
341341
case prov of
342342
TopLevelArgPrv _ idx _ -> pure (hi, idx)
@@ -346,7 +346,9 @@ destructAll = do
346346
$ filter (isAlgType . unCType . hi_type)
347347
$ unHypothesis
348348
$ jHypothesis jdg
349-
for_ args destruct
349+
for_ args $ \arg -> do
350+
subst <- gets ts_unifier
351+
destruct $ fmap (coerce substTy subst) arg
350352

351353
--------------------------------------------------------------------------------
352354
-- | User-facing tactic to implement "Use constructor <x>"

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,7 @@ spec = do
6565
autoTest 6 8 "AutoThetaEqGADTDestruct"
6666
autoTest 6 10 "AutoThetaRefl"
6767
autoTest 6 8 "AutoThetaReflDestruct"
68+
autoTest 19 30 "AutoThetaMultipleUnification"
6869

6970
describe "known" $ do
7071
autoTest 25 13 "GoldenArbitrary"

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,4 +34,5 @@ spec = do
3434
destructAllTest 4 23 "DestructAllMany"
3535
destructAllTest 2 18 "DestructAllNonVarTopMatch"
3636
destructAllTest 2 18 "DestructAllFunc"
37+
destructAllTest 19 18 "DestructAllGADTEvidence"
3738

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE GADTs #-}
3+
{-# LANGUAGE KindSignatures #-}
4+
{-# LANGUAGE TypeOperators #-}
5+
6+
import Data.Kind
7+
8+
data Nat = Z | S Nat
9+
10+
data HList (ls :: [Type]) where
11+
HNil :: HList '[]
12+
HCons :: t -> HList ts -> HList (t ': ts)
13+
14+
data ElemAt (n :: Nat) t (ts :: [Type]) where
15+
AtZ :: ElemAt 'Z t (t ': ts)
16+
AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
17+
18+
lookMeUp :: ElemAt i ty tys -> HList tys -> ty
19+
lookMeUp AtZ (HCons t _) = t
20+
lookMeUp (AtS ea') (HCons t hl') = _
21+

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE GADTs #-}
3+
{-# LANGUAGE KindSignatures #-}
4+
{-# LANGUAGE TypeOperators #-}
5+
6+
import Data.Kind
7+
8+
data Nat = Z | S Nat
9+
10+
data HList (ls :: [Type]) where
11+
HNil :: HList '[]
12+
HCons :: t -> HList ts -> HList (t ': ts)
13+
14+
data ElemAt (n :: Nat) t (ts :: [Type]) where
15+
AtZ :: ElemAt 'Z t (t ': ts)
16+
AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
17+
18+
lookMeUp :: ElemAt i ty tys -> HList tys -> ty
19+
lookMeUp AtZ (HCons t hl') = _
20+
lookMeUp (AtS ea') (HCons t hl') = _
21+

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE GADTs #-}
3+
{-# LANGUAGE KindSignatures #-}
4+
{-# LANGUAGE TypeOperators #-}
5+
6+
import Data.Kind
7+
8+
data Nat = Z | S Nat
9+
10+
data HList (ls :: [Type]) where
11+
HNil :: HList '[]
12+
HCons :: t -> HList ts -> HList (t ': ts)
13+
14+
data ElemAt (n :: Nat) t (ts :: [Type]) where
15+
AtZ :: ElemAt 'Z t (t ': ts)
16+
AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
17+
18+
lookMeUp :: ElemAt i ty tys -> HList tys -> ty
19+
lookMeUp AtZ (HCons t hl') = _
20+
lookMeUp (AtS ea') (HCons t hl') = _
21+

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE GADTs #-}
3+
{-# LANGUAGE KindSignatures #-}
4+
{-# LANGUAGE TypeOperators #-}
5+
6+
import Data.Kind
7+
8+
data Nat = Z | S Nat
9+
10+
data HList (ls :: [Type]) where
11+
HNil :: HList '[]
12+
HCons :: t -> HList ts -> HList (t ': ts)
13+
14+
data ElemAt (n :: Nat) t (ts :: [Type]) where
15+
AtZ :: ElemAt 'Z t (t ': ts)
16+
AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
17+
18+
lookMeUp :: ElemAt i ty tys -> HList tys -> ty
19+
lookMeUp ea hl = _
20+

‎plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2,26 +2,26 @@ data ABC = A | B | C
22

33
many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()
44
many () (Left a) False Nothing A = _
5-
many () (Left a) False (Just abc') A = _
6-
many () (Right b') False Nothing A = _
7-
many () (Right b') False (Just abc') A = _
8-
many () (Left a) True Nothing A = _
9-
many () (Left a) True (Just abc') A = _
10-
many () (Right b') True Nothing A = _
11-
many () (Right b') True (Just abc') A = _
125
many () (Left a) False Nothing B = _
6+
many () (Left a) False Nothing C = _
7+
many () (Left a) False (Just abc') A = _
138
many () (Left a) False (Just abc') B = _
14-
many () (Right b') False Nothing B = _
15-
many () (Right b') False (Just abc') B = _
9+
many () (Left a) False (Just abc') C = _
10+
many () (Left a) True Nothing A = _
1611
many () (Left a) True Nothing B = _
12+
many () (Left a) True Nothing C = _
13+
many () (Left a) True (Just abc') A = _
1714
many () (Left a) True (Just abc') B = _
18-
many () (Right b') True Nothing B = _
19-
many () (Right b') True (Just abc') B = _
20-
many () (Left a) False Nothing C = _
21-
many () (Left a) False (Just abc') C = _
15+
many () (Left a) True (Just abc') C = _
16+
many () (Right b') False Nothing A = _
17+
many () (Right b') False Nothing B = _
2218
many () (Right b') False Nothing C = _
19+
many () (Right b') False (Just abc') A = _
20+
many () (Right b') False (Just abc') B = _
2321
many () (Right b') False (Just abc') C = _
24-
many () (Left a) True Nothing C = _
25-
many () (Left a) True (Just abc') C = _
22+
many () (Right b') True Nothing A = _
23+
many () (Right b') True Nothing B = _
2624
many () (Right b') True Nothing C = _
25+
many () (Right b') True (Just abc') A = _
26+
many () (Right b') True (Just abc') B = _
2727
many () (Right b') True (Just abc') C = _

‎plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b
22
maybeAp Nothing Nothing = Nothing
3-
maybeAp (Just _) Nothing = Nothing
43
maybeAp Nothing (Just _) = Nothing
4+
maybeAp (Just _) Nothing = Nothing
55
maybeAp (Just fab) (Just a) = Just (fab a)

0 commit comments

Comments
 (0)