mirrored from https://gitlab.haskell.org/ghc/ghc.git
-
Notifications
You must be signed in to change notification settings - Fork 704
/
TcSMonad.lhs
1764 lines (1424 loc) · 67.7 KB
/
TcSMonad.lhs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\begin{code}
{-# OPTIONS -fno-warn-tabs -w #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details
-- Type definitions for the constraint solver
module TcSMonad (
-- Canonical constraints, definition is now in TcRnTypes
WorkList(..), isEmptyWorkList, emptyWorkList,
workListFromEq, workListFromNonEq, workListFromCt,
extendWorkListEq, extendWorkListFunEq,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
withWorkList, workListSize,
updWorkListTcS, updWorkListTcS_return,
updTcSImplics,
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
emitInsoluble,
isWanted, isDerived,
isGivenCt, isWantedCt, isDerivedCt,
canRewrite, canSolve,
mkGivenLoc,
TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
traceFireTcS, bumpStepCountTcS,
tryTcS, nestTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
-- Getting and setting the flattening cache
addSolvedDict, addSolvedFunEq, getFlattenSkols,
deferTcSForAllEq,
setEvBind,
XEvTerm(..),
MaybeNew (..), isFresh, freshGoals, getEvTerms,
xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
newDerived,
-- Creation of evidence variables
setWantedTyBind,
getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsMap, getTcSTyBinds, getTcSTyBindsMap,
lookupFlatEqn, newFlattenSkolem, -- Flatten skolems
-- Deque
Deque(..), insertDeque, emptyDeque,
-- Inerts
InertSet(..), InertCans(..),
getInertEqs,
emptyInert, getTcSInerts, lookupInInerts,
getInertUnsolved, checkAllSolved,
prepareInertsForImplications,
modifyInertTcS,
insertInertItemTcS, partitionCCanMap, partitionEqMap,
getRelevantCts, extractRelevantInerts,
CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
PredMap, FamHeadMap,
partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
filterSolved,
instDFunType, -- Instantiation
newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
cloneMetaTyVar,
compatKind, mkKindErrorCtxtTcS,
Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
zonkTyVarsAndFV,
getDefaultInfo, getDynFlags,
matchClass, matchFam, matchOpenFam, MatchInstResult (..),
checkWellStagedDFun,
pprEq -- Smaller utils, re-exported from TcM
-- TODO (DV): these are only really used in the
-- instance matcher in TcSimplify. I am wondering
-- if the whole instance matcher simply belongs
-- here
) where
#include "HsVersions.h"
import HscTypes
import Inst
import InstEnv
import FamInst
import FamInstEnv
import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcGetDefaultTys )
import {-# SOURCE #-} qualified TcUnify as TcM ( mkKindErrorCtxt )
import Kind
import TcType
import DynFlags
import Type
import TcEvidence
import Class
import TyCon
import Name
import Var
import VarEnv
import Outputable
import Bag
import MonadUtils
import FastString
import Util
import Id
import TcRnTypes
import Unique
import UniqFM
import Maybes ( orElse, catMaybes, firstJust )
import Pair ( pSnd )
import Control.Monad( unless, when, zipWithM )
import Data.IORef
import TrieMap
#ifdef DEBUG
import StaticFlags( opt_PprStyle_Debug )
import VarSet
import Digraph
#endif
\end{code}
\begin{code}
compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `tcIsSubKind` k2 || k2 `tcIsSubKind` k1
mkKindErrorCtxtTcS :: Type -> Kind
-> Type -> Kind
-> ErrCtxt
mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
= (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)
\end{code}
%************************************************************************
%* *
%* Worklists *
%* Canonical and non-canonical constraints that the simplifier has to *
%* work on. Including their simplification depths. *
%* *
%* *
%************************************************************************
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavors).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.
As a simple form of priority queue, our worklist separates out
equalities (wl_eqs) from the rest of the canonical constraints,
so that it's easier to deal with them first, but the separation
is not strictly necessary. Notice that non-canonical constraints
are also parts of the worklist.
Note [NonCanonical Semantics]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that canonical constraints involve a CNonCanonical constructor. In the worklist
we use this constructor for constraints that have not yet been canonicalized such as
[Int] ~ [a]
In other words, all constraints start life as NonCanonicals.
On the other hand, in the Inert Set (see below) the presence of a NonCanonical somewhere
means that we have a ``frozen error''.
NonCanonical constraints never interact directly with other constraints -- but they can
be rewritten by equalities (for instance if a non canonical exists in the inert, we'd
better rewrite it as much as possible before reporting it as an error to the user)
\begin{code}
data Deque a = DQ [a] [a] -- Insert in RH field, remove from LH field
-- First to remove is at head of LH field
instance Outputable a => Outputable (Deque a) where
ppr (DQ as bs) = ppr (as ++ reverse bs) -- Show first one to come out at the start
emptyDeque :: Deque a
emptyDeque = DQ [] []
isEmptyDeque :: Deque a -> Bool
isEmptyDeque (DQ as bs) = null as && null bs
dequeSize :: Deque a -> Int
dequeSize (DQ as bs) = length as + length bs
insertDeque :: a -> Deque a -> Deque a
insertDeque b (DQ as bs) = DQ as (b:bs)
appendDeque :: Deque a -> Deque a -> Deque a
appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2
extractDeque :: Deque a -> Maybe (Deque a, a)
extractDeque (DQ [] []) = Nothing
extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
extractDeque (DQ [] bs) = case reverse bs of
(a:as) -> Just (DQ as [], a)
[] -> panic "extractDeque"
-- See Note [WorkList priorities]
data WorkList = WorkList { wl_eqs :: [Ct]
, wl_funeqs :: Deque Ct
, wl_rest :: [Ct]
}
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList new_wl orig_wl
= WorkList { wl_eqs = wl_eqs new_wl ++ wl_eqs orig_wl
, wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
, wl_rest = wl_rest new_wl ++ wl_rest orig_wl }
workListSize :: WorkList -> Int
workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
= length eqs + dequeSize funeqs + length rest
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
extendWorkListEq ct wl
| Just {} <- isCFunEqCan_Maybe ct
= extendWorkListFunEq ct wl
| otherwise
= wl { wl_eqs = ct : wl_eqs wl }
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl
= wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
-- Append a list of equalities
extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
extendWorkListNonEq ct wl
= wl { wl_rest = ct : wl_rest wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
| isEqPred (ctPred ct) = extendWorkListEq ct wl
| otherwise = extendWorkListNonEq ct wl
extendWorkListCts :: [Ct] -> WorkList -> WorkList
-- Agnostic
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList wl
= null (wl_eqs wl) && null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
emptyWorkList :: WorkList
emptyWorkList = WorkList { wl_eqs = [], wl_rest = [], wl_funeqs = emptyDeque }
workListFromEq :: Ct -> WorkList
workListFromEq ct = extendWorkListEq ct emptyWorkList
workListFromNonEq :: Ct -> WorkList
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
workListFromCt :: Ct -> WorkList
-- Agnostic
workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct
| otherwise = workListFromNonEq ct
selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
= case (eqs,feqs,rest) of
(ct:cts,_,_) -> (Just ct, wl { wl_eqs = cts })
(_,fun_eqs,_) | Just (fun_eqs', ct) <- extractDeque fun_eqs
-> (Just ct, wl { wl_funeqs = fun_eqs' })
(_,_,(ct:cts)) -> (Just ct, wl { wl_rest = cts })
(_,_,_) -> (Nothing,wl)
-- Pretty printing
instance Outputable WorkList where
ppr wl = vcat [ text "WorkList (eqs) = " <+> ppr (wl_eqs wl)
, text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
, text "WorkList (rest) = " <+> ppr (wl_rest wl)
]
-- Canonical constraint maps
data CCanMap a
= CCanMap { cts_given :: UniqFM Cts -- All Given
, cts_derived :: UniqFM Cts -- All Derived
, cts_wanted :: UniqFM Cts } -- All Wanted
keepGivenCMap :: CCanMap a -> CCanMap a
keepGivenCMap cc = emptyCCanMap { cts_given = cts_given cc }
instance Outputable (CCanMap a) where
ppr (CCanMap given derived wanted) = ptext (sLit "CCanMap") <+> (ppr given) <+> (ppr derived) <+> (ppr wanted)
cCanMapToBag :: CCanMap a -> Cts
cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap)
where rest_wder = foldUFM unionBags rest_der (cts_wanted cmap)
rest_der = foldUFM unionBags emptyCts (cts_derived cmap)
emptyCCanMap :: CCanMap a
emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM }
updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a
updCCanMap (a,ct) cmap
= case cc_ev ct of
CtWanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) }
CtGiven {} -> cmap { cts_given = insert_into (cts_given cmap) }
CtDerived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
where
insert_into m = addToUFM_C unionBags m a (singleCt ct)
getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a)
-- Gets the relevant constraints and returns the rest of the CCanMap
getRelevantCts a cmap
= let relevant = lookup (cts_wanted cmap) `unionBags`
lookup (cts_given cmap) `unionBags`
lookup (cts_derived cmap)
residual_map = cmap { cts_wanted = delFromUFM (cts_wanted cmap) a
, cts_given = delFromUFM (cts_given cmap) a
, cts_derived = delFromUFM (cts_derived cmap) a }
in (relevant, residual_map)
where
lookup map = lookupUFM map a `orElse` emptyCts
lookupCCanMap :: Uniquable a => a -> (CtEvidence -> Bool) -> CCanMap a -> Maybe CtEvidence
lookupCCanMap a pick_me map
= findEvidence pick_me possible_cts
where
possible_cts = lookupUFM (cts_given map) a `plus` (
lookupUFM (cts_wanted map) a `plus` (
lookupUFM (cts_derived map) a `plus` emptyCts))
plus Nothing cts2 = cts2
plus (Just cts1) cts2 = cts1 `unionBags` cts2
findEvidence :: (CtEvidence -> Bool) -> Cts -> Maybe CtEvidence
findEvidence pick_me cts
= foldrBag pick Nothing cts
where
pick :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev
| otherwise = deflt
partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a)
-- All constraints that /match/ the predicate go in the bag, the rest remain in the map
partitionCCanMap pred cmap
= let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap)
(ds_map,ds) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_derived cmap)
(gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap)
in (ws `andCts` ds `andCts` gs, cmap { cts_wanted = ws_map
, cts_given = gs_map
, cts_derived = ds_map })
where aux k this_cts (mp,acc_cts) = (new_mp, new_acc_cts)
where new_mp = addToUFM mp k cts_keep
new_acc_cts = acc_cts `andCts` cts_out
(cts_out, cts_keep) = partitionBag pred this_cts
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
partitionEqMap pred isubst
= let eqs_out = foldVarEnv extend_if_pred [] isubst
eqs_in = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst
in (eqs_out, eqs_in)
where extend_if_pred (ct,_) cts = if pred ct then ct : cts else cts
extractUnsolvedCMap :: CCanMap a -> Cts
-- Gets the wanted or derived constraints
extractUnsolvedCMap cmap = foldUFM unionBags emptyCts (cts_wanted cmap)
`unionBags` foldUFM unionBags emptyCts (cts_derived cmap)
-- Maps from PredTypes to Constraints
type CtTypeMap = TypeMap Ct
type CtPredMap = PredMap Ct
type CtFamHeadMap = FamHeadMap Ct
newtype PredMap a = PredMap { unPredMap :: TypeMap a } -- Indexed by TcPredType
newtype FamHeadMap a = FamHeadMap { unFamHeadMap :: TypeMap a } -- Indexed by family head
instance Outputable a => Outputable (PredMap a) where
ppr (PredMap m) = ppr (foldTM (:) m [])
instance Outputable a => Outputable (FamHeadMap a) where
ppr (FamHeadMap m) = ppr (foldTM (:) m [])
sizePredMap :: PredMap a -> Int
sizePredMap (PredMap m) = foldTypeMap (\_ x -> x+1) 0 m
emptyFamHeadMap :: FamHeadMap a
emptyFamHeadMap = FamHeadMap emptyTM
sizeFamHeadMap :: FamHeadMap a -> Int
sizeFamHeadMap (FamHeadMap m) = foldTypeMap (\_ x -> x+1) 0 m
ctTypeMapCts :: TypeMap Ct -> Cts
ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
lookupFamHead (FamHeadMap m) key = lookupTM key m
insertFamHead :: FamHeadMap a -> TcType -> a -> FamHeadMap a
insertFamHead (FamHeadMap m) key value = FamHeadMap (alterTM key (const (Just value)) m)
delFamHead :: FamHeadMap a -> TcType -> FamHeadMap a
delFamHead (FamHeadMap m) key = FamHeadMap (alterTM key (const Nothing) m)
anyFamHeadMap :: (Ct -> Bool) -> CtFamHeadMap -> Bool
anyFamHeadMap f ctmap = foldTM ((||) . f) (unFamHeadMap ctmap) False
partCtFamHeadMap :: (Ct -> Bool)
-> CtFamHeadMap
-> (Cts, CtFamHeadMap)
partCtFamHeadMap f ctmap
= let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
in (cts, FamHeadMap tymap_final)
where
tymap_inside = unFamHeadMap ctmap
upd_acc ct (cts,acc_map)
| f ct = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
| otherwise = (cts,acc_map)
where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
= ty1
| otherwise
= panic "partCtFamHeadMap, encountered non equality!"
filterSolved :: (CtEvidence -> Bool) -> PredMap CtEvidence -> PredMap CtEvidence
filterSolved p (PredMap mp) = PredMap (foldTM upd mp emptyTM)
where upd a m = if p a then alterTM (ctEvPred a) (\_ -> Just a) m
else m
\end{code}
%************************************************************************
%* *
%* Inert Sets *
%* *
%* *
%************************************************************************
Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
1 All canonical
2 All Given or Wanted or Derived. No (partially) Solved
3 No two dictionaries with the same head
4 No two family equations with the same head
NB: This is enforced by construction since we use a CtFamHeadMap for inert_funeqs
5 Family equations inert wrt top-level family axioms
6 Dictionaries have no matching top-level instance
7 Non-equality constraints are fully rewritten with respect to the equalities (CTyEqCan)
8 Equalities _do_not_ form an idempotent substitution, but they are
guaranteed to not have any occurs errors. Additional notes:
- The lack of idempotence of the inert substitution implies
that we must make sure that when we rewrite a constraint we
apply the substitution /recursively/ to the types
involved. Currently the one AND ONLY way in the whole
constraint solver that we rewrite types and constraints wrt
to the inert substitution is TcCanonical/flattenTyVar.
- In the past we did try to have the inert substitution as
idempotent as possible but this would only be true for
constraints of the same flavor, so in total the inert
substitution could not be idempotent, due to flavor-related
issued. Note [Non-idempotent inert substitution] explains
what is going on.
- Whenever a constraint ends up in the worklist we do
recursively apply exhaustively the inert substitution to it
to check for occurs errors. But if an equality is already in
the inert set and we can guarantee that adding a new equality
will not cause the first equality to have an occurs check
then we do not rewrite the inert equality. This happens in
TcInteract, rewriteInertEqsFromInertEq.
See Note [Delicate equality kick-out] to see which inert
equalities can safely stay in the inert set and which must be
kicked out to be rewritten and re-checked for occurs errors.
9 Given family or dictionary constraints don't mention touchable unification variables
Note [Solved constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~
When we take a step to simplify a constraint 'c', we call the original constraint "solved".
For example: Wanted: ev :: [s] ~ [t]
New goal: ev1 :: s ~ t
Then 'ev' is now "solved".
The reason for all this is simply to avoid re-solving goals we have solved already.
* A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not
use it to rewrite a Given; in that sense the solved goal is still a Wanted
* A solved Given is just given
* A solved Derived in inert_solved is possible; purpose is to avoid
creating tons of identical Derived goals.
But there are no solved Deriveds in inert_solved_funeqs
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type-family equations, of form (ev : F tys ~ ty), live in four places
* The work-list, of course
* The inert_flat_cache. This is used when flattening, to get maximal
sharing. It contains lots of things that are still in the work-list.
E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work
list. Now if we flatten w2 before we get to w3, we still want to
share that (G a).
Because it contains work-list things, DO NOT use the flat cache to solve
a top-level goal. Eg in the above example we don't want to solve w3
using w3 itself!
* The inert_solved_funeqs. These are all "solved" goals (see Note [Solved constraints]),
the result of using a top-level type-family instance.
* THe inert_funeqs are un-solved but fully processed and in the InertCans.
\begin{code}
-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
data InertCans
= IC { inert_eqs :: TyVarEnv Ct
-- Must all be CTyEqCans! If an entry exists of the form:
-- a |-> ct,co
-- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
-- And co : a ~ xi
, inert_dicts :: CCanMap Class
-- Dictionaries only, index is the class
-- NB: index is /not/ the whole type because FD reactions
-- need to match the class but not necessarily the whole type.
, inert_funeqs :: CtFamHeadMap
-- Family equations, index is the whole family head type.
, inert_irreds :: Cts
-- Irreducible predicates
, inert_insols :: Cts
-- Frozen errors (as non-canonicals)
}
-- The Inert Set
data InertSet
= IS { inert_cans :: InertCans
-- Canonical Given, Wanted, Derived (no Solved)
-- Sometimes called "the inert set"
, inert_flat_cache :: FamHeadMap (CtEvidence, TcType)
-- See Note [Type family equations]
-- Just a hash-cons cache for use when flattening only
-- These include entirely un-processed goals, so don't use
-- them to solve a top-level goal, else you may end up solving
-- (w:F ty ~ a) by setting w:=w! We just use the flat-cache
-- when allocating a new flatten-skolem.
-- Not necessarily inert wrt top-level equations (or inert_cans)
, inert_fsks :: [TcTyVar] -- Rigid flatten-skolems (arising from givens)
-- allocated in this local scope
, inert_solved_funeqs :: FamHeadMap (CtEvidence, TcType)
-- See Note [Type family equations]
-- Of form co :: F xis ~ xi
-- Always the result of using a top-level family axiom F xis ~ tau
-- No Deriveds
-- Not necessarily fully rewritten (by type substitutions)
, inert_solved_dicts :: PredMap CtEvidence
-- Of form ev :: C t1 .. tn
-- Always the result of using a top-level instance declaration
-- See Note [Solved constraints]
-- - Used to avoid creating a new EvVar when we have a new goal
-- that we have solved in the past
-- - Stored not necessarily as fully rewritten
-- (ToDo: rewrite lazily when we lookup)
}
instance Outputable InertCans where
ppr ics = vcat [ ptext (sLit "Equalities:")
<+> vcat (map ppr (varEnvElts (inert_eqs ics)))
, ptext (sLit "Type-function equalities:")
<+> vcat (map ppr (Bag.bagToList $
ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
, ptext (sLit "Dictionaries:")
<+> vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
, ptext (sLit "Irreds:")
<+> vcat (map ppr (Bag.bagToList $ inert_irreds ics))
, text "Insolubles =" <+> -- Clearly print frozen errors
braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
]
instance Outputable InertSet where
ppr is = vcat [ ppr $ inert_cans is
, text "Solved dicts" <+> int (sizePredMap (inert_solved_dicts is))
, text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
emptyInert :: InertSet
emptyInert
= IS { inert_cans = IC { inert_eqs = emptyVarEnv
, inert_dicts = emptyCCanMap
, inert_funeqs = emptyFamHeadMap
, inert_irreds = emptyCts
, inert_insols = emptyCts }
, inert_fsks = []
, inert_flat_cache = emptyFamHeadMap
, inert_solved_dicts = PredMap emptyTM
, inert_solved_funeqs = emptyFamHeadMap }
insertInertItem :: Ct -> InertSet -> InertSet
-- Add a new inert element to the inert set.
insertInertItem item is
= -- A canonical Given, Wanted, or Derived
is { inert_cans = upd_inert_cans (inert_cans is) item }
where upd_inert_cans :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
upd_inert_cans ics item
| isCTyEqCan item
= let upd_err a b = pprPanic "insertInertItem" $
vcat [ text "Multiple inert equalities:"
, text "Old (already inert):" <+> ppr a
, text "Trying to insert :" <+> ppr b ]
eqs' = extendVarEnv_C upd_err (inert_eqs ics)
(cc_tyvar item) item
in ics { inert_eqs = eqs' }
| isCIrredEvCan item -- Presently-irreducible evidence
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
| Just cls <- isCDictCan_Maybe item -- Dictionary
= ics { inert_dicts = updCCanMap (cls,item) (inert_dicts ics) }
| Just _tc <- isCFunEqCan_Maybe item -- Function equality
= let fam_head = mkTyConApp (cc_fun item) (cc_tyargs item)
upd_funeqs Nothing = Just item
upd_funeqs (Just _already_there)
= panic "insertInertItem: item already there!"
in ics { inert_funeqs = FamHeadMap
(alterTM fam_head upd_funeqs $
(unFamHeadMap $ inert_funeqs ics)) }
| otherwise
= pprPanic "upd_inert set: can't happen! Inserting " $
ppr item -- Can't be CNonCanonical, CHoleCan,
-- because they only land in inert_insols
insertInertItemTcS :: Ct -> TcS ()
-- Add a new item in the inerts of the monad
insertInertItemTcS item
= do { traceTcS "insertInertItemTcS {" $
text "Trying to insert new inert item:" <+> ppr item
; updInertTcS (insertInertItem item)
; traceTcS "insertInertItemTcS }" $ empty }
addSolvedDict :: CtEvidence -> TcS ()
-- Add a new item in the solved set of the monad
addSolvedDict item
| isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
= return ()
| otherwise
= do { traceTcS "updSolvedSetTcs:" $ ppr item
; updInertTcS upd_solved_dicts }
where
upd_solved_dicts is
= is { inert_solved_dicts = PredMap $ alterTM pred upd_solved $
unPredMap $ inert_solved_dicts is }
pred = ctEvPred item
upd_solved _ = Just item
addSolvedFunEq :: TcType -> CtEvidence -> TcType -> TcS ()
addSolvedFunEq fam_ty ev rhs_ty
= updInertTcS $ \ inert ->
inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert)
fam_ty (ev, rhs_ty) }
modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a
-- Modify the inert set with the supplied function
modifyInertTcS upd
= do { is_var <- getTcSInertsRef
; curr_inert <- wrapTcS (TcM.readTcRef is_var)
; let (a, new_inert) = upd curr_inert
; wrapTcS (TcM.writeTcRef is_var new_inert)
; return a }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
-- Modify the inert set with the supplied function
updInertTcS upd
= do { is_var <- getTcSInertsRef
; curr_inert <- wrapTcS (TcM.readTcRef is_var)
; let new_inert = upd curr_inert
; wrapTcS (TcM.writeTcRef is_var new_inert) }
prepareInertsForImplications :: InertSet -> InertSet
-- See Note [Preparing inert set for implications]
prepareInertsForImplications is
= is { inert_cans = getGivens (inert_cans is)
, inert_fsks = []
, inert_flat_cache = emptyFamHeadMap }
where
getGivens (IC { inert_eqs = eqs
, inert_irreds = irreds
, inert_funeqs = FamHeadMap funeqs
, inert_dicts = dicts })
= IC { inert_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
, inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
, inert_irreds = Bag.filterBag isGivenCt irreds
, inert_dicts = keepGivenCMap dicts
, inert_insols = emptyCts }
given_from_wanted funeq -- This is where the magic processing happens
| isGiven ev = funeq -- for type-function equalities
-- See Note [Preparing inert set for implications]
| otherwise = funeq { cc_ev = given_ev }
where
ev = ctEvidence funeq
given_ev = CtGiven { ctev_evtm = EvId (ctev_evar ev)
, ctev_pred = ctev_pred ev }
\end{code}
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we trim the inert set,
retaining only Givens. These givens can be used when solving
the inner implications.
With one wrinkle! We take all *wanted* *funeqs*, and turn them into givens.
Consider (Trac #4935)
type instance F True a b = a
type instance F False a b = b
[w] F c a b ~ gamma
(c ~ True) => a ~ gamma
(c ~ False) => b ~ gamma
Obviously this is soluble with gamma := F c a b. But
Since solveCTyFunEqs happens at the very end of solving, the only way
to solve the two implications is temporarily consider (F c a b ~ gamma)
as Given and push it inside the implications. Now, when we come
out again at the end, having solved the implications solveCTyFunEqs
will solve this equality.
Turning type-function equalities into Givens is easy becase they
*stay inert*. No need to re-process them.
We don't try to turn any *other* Wanteds into Givens:
* For example, we should not push given dictionaries in because
of example LongWayOverlapping.hs, where we might get strange
overlap errors between far-away constraints in the program.
There might be cases where interactions between wanteds can help
to solve a constraint. For example
class C a b | a -> b
(C Int alpha), (forall d. C d blah => C Int a)
If we push the (C Int alpha) inwards, as a given, it can produce a
fundep (alpha~a) and this can float out again and be used to fix
alpha. (In general we can't float class constraints out just in case
(C d blah) might help to solve (C Int a).) But we ignore this possiblity.
\begin{code}
getInertEqs :: TcS (TyVarEnv Ct)
getInertEqs = do { inert <- getTcSInerts
; return (inert_eqs (inert_cans inert)) }
getInertUnsolved :: TcS (Cts, Cts)
-- Return (unsolved-wanteds, insolubles)
-- Both consist of a mixture of Wanted and Derived
getInertUnsolved
= do { is <- getTcSInerts
; let icans = inert_cans is
unsolved_irreds = Bag.filterBag is_unsolved (inert_irreds icans)
unsolved_dicts = extractUnsolvedCMap (inert_dicts icans)
(unsolved_funeqs,_) = partCtFamHeadMap is_unsolved (inert_funeqs icans)
unsolved_eqs = foldVarEnv add_if_unsolved emptyCts (inert_eqs icans)
unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_dicts `unionBags` unsolved_funeqs
; return (unsolved_flats, inert_insols icans) }
where
add_if_unsolved ct cts
| is_unsolved ct = cts `extendCts` ct
| otherwise = cts
is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
checkAllSolved :: TcS Bool
-- True if there are no unsolved wanteds
-- Ignore Derived for this purpose, unless in insolubles
checkAllSolved
= do { is <- getTcSInerts
; let icans = inert_cans is
unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
unsolved_dicts = not (isNullUFM (cts_wanted (inert_dicts icans)))
unsolved_funeqs = anyFamHeadMap isWantedCt (inert_funeqs icans)
unsolved_eqs = foldVarEnv ((||) . isWantedCt) False (inert_eqs icans)
; return (not (unsolved_eqs || unsolved_irreds
|| unsolved_dicts || unsolved_funeqs
|| not (isEmptyBag (inert_insols icans)))) }
extractRelevantInerts :: Ct -> TcS Cts
-- Returns the constraints from the inert set that are 'relevant' to react with
-- this constraint. The monad is left with the 'thinner' inerts.
-- NB: This function contains logic specific to the constraint solver, maybe move there?
extractRelevantInerts wi
= modifyInertTcS (extract_relevants wi)
where
extract_relevants :: Ct -> InertSet -> (Cts,InertSet)
extract_relevants wi is
= let (cts,ics') = extract_ics_relevants wi (inert_cans is)
in (cts, is { inert_cans = ics' })
extract_ics_relevants :: Ct -> InertCans -> (Cts, InertCans)
extract_ics_relevants (CDictCan {cc_class = cl}) ics =
let (cts,dict_map) = getRelevantCts cl (inert_dicts ics)
in (cts, ics { inert_dicts = dict_map })
extract_ics_relevants ct@(CFunEqCan {}) ics@(IC { inert_funeqs = funeq_map })
| Just ct <- lookupFamHead funeq_map fam_head
= (singleCt ct, ics { inert_funeqs = delFamHead funeq_map fam_head })
| otherwise
= (emptyCts, ics)
where
fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
extract_ics_relevants (CHoleCan {}) ics
= pprPanic "extractRelevantInerts" (ppr wi)
-- Holes are put straight into inert_frozen, so never get here
extract_ics_relevants (CIrredEvCan { }) ics =
let cts = inert_irreds ics
in (cts, ics { inert_irreds = emptyCts })
extract_ics_relevants _ ics = (emptyCts,ics)
lookupFlatEqn :: TcType -> TcS (Maybe (CtEvidence, TcType))
lookupFlatEqn fam_ty
= do { IS { inert_solved_funeqs = solved_funeqs
, inert_flat_cache = flat_cache
, inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
; return (lookupFamHead solved_funeqs fam_ty `firstJust`
lookup_in_inerts inert_funeqs `firstJust`
lookupFamHead flat_cache fam_ty) }
where
lookup_in_inerts inert_funeqs
= case lookupFamHead inert_funeqs fam_ty of
Nothing -> Nothing
Just ct -> Just (ctEvidence ct, cc_rhs ct)
lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
lookupInInerts pty
= do { inerts <- getTcSInerts
; case lookupSolvedDict inerts pty of
Just ctev -> return (Just ctev)
Nothing -> return (lookupInInertCans inerts pty) }
lookupSolvedDict :: InertSet -> TcPredType -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict (IS { inert_solved_dicts = solved }) pty
= lookupTM pty (unPredMap solved)
lookupInInertCans :: InertSet -> TcPredType -> Maybe CtEvidence
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans (IS { inert_cans = ics }) pty
= case (classifyPredType pty) of
ClassPred cls _
-> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)
EqPred ty1 _ty2
| Just tv <- getTyVar_maybe ty1 -- Tyvar equation
, Just ct <- lookupVarEnv (inert_eqs ics) tv
, let ctev = ctEvidence ct
, ctEvPred ctev `eqType` pty
-> Just ctev
| Just _ <- splitTyConApp_maybe ty1 -- Family equation
, Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
, let ctev = ctEvidence ct
, ctEvPred ctev `eqType` pty
-> Just ctev
IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics)
_other -> Nothing -- NB: No caching for IPs or holes
\end{code}
%************************************************************************
%* *
%* The TcS solver monad *
%* *
%************************************************************************
Note [The TcS monad]
~~~~~~~~~~~~~~~~~~~~
The TcS monad is a weak form of the main Tc monad
All you can do is
* fail
* allocate new variables
* fill in evidence variables
Filling in a dictionary evidence variable means to create a binding
for it, so TcS carries a mutable location where the binding can be
added. This is initialised from the innermost implication constraint.
\begin{code}
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
-- Global type bindings
tcs_count :: IORef Int, -- Global step count
tcs_inerts :: IORef InertSet, -- Current inert set
tcs_worklist :: IORef WorkList, -- Current worklist
-- Residual implication constraints that are generated
-- while solving or canonicalising the current worklist.
-- Specifically, when canonicalising (forall a. t1 ~ forall a. t2)
-- from which we get the implication (forall a. t1 ~ t2)
tcs_implics :: IORef (Bag Implication)
}
\end{code}
\begin{code}
---------------
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
instance Functor TcS where
fmap f m = TcS $ fmap f . unTcS m
instance Monad TcS where
return x = TcS (\_ -> return x)
fail err = TcS (\_ -> fail err)
m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
-- Basic functionality
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wrapTcS :: TcM a -> TcS a
-- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
-- and TcS is supposed to have limited functionality
wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
wrapErrTcS :: TcM a -> TcS a
-- The thing wrapped should just fail
-- There's no static check; it's up to the user
-- Having a variant for each error message is too painful