| ... |
... |
@@ -36,6 +36,7 @@ import GHC.Utils.Panic |
|
36
|
36
|
import GHC.Utils.Misc( filterOut )
|
|
37
|
37
|
|
|
38
|
38
|
import GHC.Data.Pair
|
|
|
39
|
+import Data.Maybe( mapMaybe )
|
|
39
|
40
|
|
|
40
|
41
|
|
|
41
|
42
|
{- Note [Overview of fundeps]
|
| ... |
... |
@@ -403,27 +404,27 @@ tryEqFunDeps :: EqCt -> SolverStage () |
|
403
|
404
|
tryEqFunDeps work_item@(EqCt { eq_lhs = lhs, eq_eq_rel = eq_rel })
|
|
404
|
405
|
| NomEq <- eq_rel
|
|
405
|
406
|
, TyFamLHS tc args <- lhs
|
|
406
|
|
- = do { improveLocalFunEqs tc args work_item
|
|
407
|
|
- ; improveTopFunEqs tc args work_item }
|
|
|
407
|
+ = do { tryLocalFamEqFDs tc args work_item
|
|
|
408
|
+ ; tryTopFamEqFDs tc args work_item }
|
|
408
|
409
|
| otherwise
|
|
409
|
410
|
= nopStage ()
|
|
410
|
411
|
|
|
411
|
412
|
--------------------
|
|
412
|
|
-improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> SolverStage ()
|
|
|
413
|
+tryTopFamEqFDs :: TyCon -> [TcType] -> EqCt -> SolverStage ()
|
|
413
|
414
|
-- TyCon is definitely a type family
|
|
414
|
415
|
-- See Note [FunDep and implicit parameter reactions]
|
|
415
|
|
-improveTopFunEqs fam_tc args eq_ct@(EqCt { eq_ev = ev, eq_rhs = rhs_ty })
|
|
|
416
|
+tryTopFamEqFDs fam_tc args eq_ct@(EqCt { eq_ev = ev, eq_rhs = rhs_ty })
|
|
416
|
417
|
= Stage $
|
|
417
|
418
|
do { imp <- if isGiven ev
|
|
418
|
|
- then improveGivenTopFunEqs fam_tc args ev rhs_ty
|
|
419
|
|
- else improveWantedTopFunEqs fam_tc args ev rhs_ty
|
|
|
419
|
+ then tryGivenTopFamEqFDs fam_tc args ev rhs_ty
|
|
|
420
|
+ else tryWantedTopFamEqFDs fam_tc args ev rhs_ty
|
|
420
|
421
|
; if imp then startAgainWith (CEqCan eq_ct)
|
|
421
|
422
|
else continueWith () }
|
|
422
|
423
|
|
|
423
|
|
-improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
|
|
|
424
|
+tryGivenTopFamEqFDs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
|
|
424
|
425
|
-- TyCon is definitely a type family
|
|
425
|
426
|
-- Work-item is a Given
|
|
426
|
|
-improveGivenTopFunEqs fam_tc args ev rhs_ty
|
|
|
427
|
+tryGivenTopFamEqFDs fam_tc args ev rhs_ty
|
|
427
|
428
|
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
|
|
428
|
429
|
= do { traceTcS "improveGivenTopFunEqs" (ppr fam_tc <+> ppr args $$ ppr ev $$ ppr rhs_ty)
|
|
429
|
430
|
; emitNewGivens (ctEvLoc ev) $
|
| ... |
... |
@@ -436,48 +437,44 @@ improveGivenTopFunEqs fam_tc args ev rhs_ty |
|
436
|
437
|
where
|
|
437
|
438
|
given_co :: Coercion = ctEvCoercion ev
|
|
438
|
439
|
|
|
439
|
|
-improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
|
|
|
440
|
+tryWantedTopFamEqFDs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
|
|
440
|
441
|
-- TyCon is definitely a type family
|
|
441
|
442
|
-- Work-item is a Wanted
|
|
442
|
|
-improveWantedTopFunEqs fam_tc args ev rhs_ty
|
|
443
|
|
- = do { fd_eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty
|
|
|
443
|
+tryWantedTopFamEqFDs fam_tc args ev rhs_ty
|
|
|
444
|
+ = do { fam_envs <- getFamInstEnvs
|
|
|
445
|
+ ; let fd_eqns = mWantedTopFamEqEqns fam_envs fam_tc args rhs_ty
|
|
444
|
446
|
; traceTcS "improveTopFunEqs" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr args
|
|
445
|
447
|
, text "rhs:" <+> ppr rhs_ty
|
|
446
|
448
|
, text "eqns:" <+> ppr fd_eqns ])
|
|
447
|
449
|
; solveFunDeps ev fd_eqns }
|
|
448
|
450
|
|
|
449
|
|
-improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi -> TcS [FunDepEqn]
|
|
|
451
|
+mWantedTopFamEqEqns :: (FamInstEnv, FamInstEnv) -> TyCon -> [TcType] -> Xi -> [FunDepEqn]
|
|
450
|
452
|
-- TyCon is definitely a type family
|
|
451
|
|
-improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty
|
|
|
453
|
+mWantedTopFamEqEqns fam_envs fam_tc lhs_tys rhs_ty
|
|
452
|
454
|
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
|
|
453
|
|
- = return [FDEqn { fd_qtvs = []
|
|
454
|
|
- , fd_eqs = map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty }]
|
|
|
455
|
+ = [FDEqn { fd_qtvs = []
|
|
|
456
|
+ , fd_eqs = map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty }]
|
|
455
|
457
|
|
|
456
|
458
|
-- ToDo: use ideas in #23162 for closed type families; injectivity only for open
|
|
457
|
459
|
|
|
458
|
460
|
-- See Note [Type inference for type families with injectivity]
|
|
459
|
461
|
-- Open, so look for inj
|
|
460
|
462
|
| Injective inj_args <- tyConInjectivityInfo fam_tc
|
|
461
|
|
- = do { fam_envs <- getFamInstEnvs
|
|
462
|
|
- ; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
|
|
463
|
|
- ; let local_eqns = improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty
|
|
464
|
|
- ; traceTcS "improve_wanted_top_fun_eqs" $
|
|
465
|
|
- vcat [ ppr fam_tc
|
|
466
|
|
- , text "local_eqns" <+> ppr local_eqns
|
|
467
|
|
- , text "top_eqns" <+> ppr top_eqns ]
|
|
|
463
|
+ , let top_eqns = mkInjWantedFamEqTopEqns fam_envs inj_args fam_tc lhs_tys rhs_ty
|
|
|
464
|
+ local_eqns = mkInjWantedFamEqSelfEqns inj_args fam_tc lhs_tys rhs_ty
|
|
|
465
|
+ = local_eqns ++ top_eqns
|
|
468
|
466
|
-- xxx ToDo: this does both local and top => bug?
|
|
469
|
|
- ; return (local_eqns ++ top_eqns) }
|
|
470
|
467
|
|
|
471
|
468
|
| otherwise -- No injectivity
|
|
472
|
|
- = return []
|
|
|
469
|
+ = []
|
|
473
|
470
|
|
|
474
|
|
-improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon
|
|
475
|
|
- -> [TcType] -> Xi -> TcS [FunDepEqn]
|
|
|
471
|
+mkInjWantedFamEqTopEqns :: FamInstEnvs -> [Bool] -> TyCon
|
|
|
472
|
+ -> [TcType] -> Xi -> [FunDepEqn]
|
|
476
|
473
|
-- Interact with top-level instance declarations
|
|
477
|
474
|
-- See Section 5.2 in the Injective Type Families paper
|
|
478
|
475
|
-- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are
|
|
479
|
|
-improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
|
|
480
|
|
- = concatMapM do_one branches
|
|
|
476
|
+mkInjWantedFamEqTopEqns fam_envs inj_args fam_tc lhs_tys rhs_ty
|
|
|
477
|
+ = mapMaybe do_one branches
|
|
481
|
478
|
where
|
|
482
|
479
|
branches :: [CoAxBranch]
|
|
483
|
480
|
branches | isOpenTypeFamilyTyCon fam_tc
|
| ... |
... |
@@ -490,72 +487,60 @@ improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty |
|
490
|
487
|
| otherwise
|
|
491
|
488
|
= []
|
|
492
|
489
|
|
|
493
|
|
- do_one :: CoAxBranch -> TcS [FunDepEqn]
|
|
494
|
|
- do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs })
|
|
|
490
|
+ do_one :: CoAxBranch -> Maybe FunDepEqn
|
|
|
491
|
+ do_one branch@(CoAxBranch { cab_tvs = branch_tvs
|
|
|
492
|
+ , cab_lhs = branch_lhs_tys
|
|
|
493
|
+ , cab_rhs = branch_rhs })
|
|
495
|
494
|
| let in_scope1 = in_scope `extendInScopeSetList` branch_tvs
|
|
496
|
495
|
, Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty
|
|
497
|
496
|
-- False: matching, not unifying
|
|
498
|
|
- = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst
|
|
499
|
|
- unsubstTvs = filterOut inSubst branch_tvs
|
|
500
|
|
- -- The order of unsubstTvs is important; it must be
|
|
|
497
|
+ , let branch_lhs_tys' = substTys subst branch_lhs_tys
|
|
|
498
|
+ , apartnessCheck branch_lhs_tys' branch
|
|
|
499
|
+ , let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst
|
|
|
500
|
+ qtvs = filterOut inSubst branch_tvs
|
|
|
501
|
+ -- The order of qtvs is important; it must be
|
|
501
|
502
|
-- in telescope order e.g. (k:*) (a:k)
|
|
502
|
|
-
|
|
503
|
|
- ; (_subst_tvs, subst1) <- instFlexiX subst unsubstTvs
|
|
504
|
|
- -- If the current substitution bind [k -> *], and
|
|
505
|
|
- -- one of the un-substituted tyvars is (a::k), we'd better
|
|
506
|
|
- -- be sure to apply the current substitution to a's kind.
|
|
507
|
|
- -- Hence instFlexiX. #13135 was an example.
|
|
508
|
|
-
|
|
509
|
|
- ; traceTcS "improve_inj_top" $
|
|
510
|
|
- vcat [ text "branch_rhs" <+> ppr branch_rhs
|
|
511
|
|
- , text "rhs_ty" <+> ppr rhs_ty
|
|
512
|
|
- , text "subst" <+> ppr subst
|
|
513
|
|
- , text "subst1" <+> ppr subst1 ]
|
|
514
|
|
- ; let branch_lhs_tys' = substTys subst1 branch_lhs_tys
|
|
515
|
|
- ; if apartnessCheck branch_lhs_tys' branch
|
|
516
|
|
- then do { traceTcS "improv_inj_top1" (ppr branch_lhs_tys')
|
|
517
|
|
- ; return [mkInjectivityFDEqn inj_args branch_lhs_tys' lhs_tys] }
|
|
518
|
|
- -- NB: The fresh unification variables (from unsubstTvs) are on the left
|
|
519
|
|
- -- See Note [Improvement orientation]
|
|
520
|
|
- else do { traceTcS "improve_inj_top2" empty; return [] } }
|
|
|
503
|
+ = Just (mkInjectivityFDEqn inj_args qtvs branch_lhs_tys' lhs_tys)
|
|
521
|
504
|
| otherwise
|
|
522
|
|
- = do { traceTcS "improve_inj_top:fail" (ppr branch_rhs $$ ppr rhs_ty $$ ppr in_scope $$ ppr branch_tvs)
|
|
523
|
|
- ; return [] }
|
|
|
505
|
+ = Nothing
|
|
524
|
506
|
|
|
525
|
507
|
in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty)
|
|
526
|
508
|
|
|
527
|
509
|
|
|
528
|
|
-improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [FunDepEqn]
|
|
|
510
|
+mkInjWantedFamEqSelfEqns :: [Bool] -> TyCon -> [TcType] -> Xi -> [FunDepEqn]
|
|
529
|
511
|
-- Interact with itself, specifically F s1 s2 ~ F t1 t2
|
|
530
|
512
|
-- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are
|
|
531
|
|
-improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty
|
|
|
513
|
+mkInjWantedFamEqSelfEqns inj_args fam_tc lhs_tys rhs_ty
|
|
532
|
514
|
| Just (tc, rhs_tys) <- tcSplitTyConApp_maybe rhs_ty
|
|
533
|
515
|
, tc == fam_tc
|
|
534
|
|
- = [mkInjectivityFDEqn inj_args lhs_tys rhs_tys]
|
|
|
516
|
+ = [mkInjectivityFDEqn inj_args [] lhs_tys rhs_tys]
|
|
535
|
517
|
| otherwise
|
|
536
|
518
|
= []
|
|
537
|
519
|
|
|
538
|
|
-mkInjectivityFDEqn :: [Bool] -> [TcType] -> [TcType] -> FunDepEqn
|
|
|
520
|
+mkInjectivityFDEqn :: [Bool] -- Injectivity flags
|
|
|
521
|
+ -> [TcTyVar] -- Quantify these
|
|
|
522
|
+ -> [TcType] -> [TcType] -- Make these equal
|
|
|
523
|
+ -> FunDepEqn
|
|
539
|
524
|
-- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True]
|
|
540
|
525
|
-- return the FDEqn { fd_eqs = [Pair s1 t1, Pair s3 t3] }
|
|
541
|
526
|
-- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are
|
|
542
|
|
-mkInjectivityFDEqn inj_args lhs_args rhs_args
|
|
543
|
|
- = FDEqn { fd_qtvs = [], fd_eqs = eqs }
|
|
|
527
|
+mkInjectivityFDEqn inj_args qtvs lhs_args rhs_args
|
|
|
528
|
+ = FDEqn { fd_qtvs = qtvs, fd_eqs = eqs }
|
|
544
|
529
|
where
|
|
545
|
530
|
eqs = [ Pair lhs_arg rhs_arg
|
|
546
|
531
|
| (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]
|
|
547
|
532
|
|
|
548
|
533
|
---------------------------------------------
|
|
549
|
|
-improveLocalFunEqs :: TyCon -> [TcType] -> EqCt -- F args ~ rhs
|
|
550
|
|
- -> SolverStage ()
|
|
|
534
|
+tryLocalFamEqFDs :: TyCon -> [TcType] -> EqCt -- F args ~ rhs
|
|
|
535
|
+ -> SolverStage ()
|
|
551
|
536
|
-- Emit equalities from interaction between two equalities
|
|
552
|
|
-improveLocalFunEqs fam_tc args eq_ct@(EqCt { eq_ev = work_ev, eq_rhs = rhs })
|
|
|
537
|
+tryLocalFamEqFDs fam_tc args eq_ct@(EqCt { eq_ev = work_ev, eq_rhs = rhs })
|
|
553
|
538
|
= Stage $
|
|
554
|
539
|
do { inerts <- getInertCans
|
|
555
|
540
|
; let my_funeqs = get_my_funeqs inerts
|
|
556
|
541
|
; imp <- if isGiven work_ev
|
|
557
|
|
- then improveGivenLocalFunEqs my_funeqs fam_tc args work_ev rhs
|
|
558
|
|
- else improveWantedLocalFunEqs my_funeqs fam_tc args work_ev rhs
|
|
|
542
|
+ then tryGivenLocalFamEqFDs my_funeqs fam_tc args work_ev rhs
|
|
|
543
|
+ else tryWantedLocalFamEqFDs my_funeqs fam_tc args work_ev rhs
|
|
559
|
544
|
; if imp then startAgainWith (CEqCan eq_ct)
|
|
560
|
545
|
else continueWith () }
|
|
561
|
546
|
where
|
| ... |
... |
@@ -567,12 +552,12 @@ improveLocalFunEqs fam_tc args eq_ct@(EqCt { eq_ev = work_ev, eq_rhs = rhs }) |
|
567
|
552
|
-- Representational equalities don't interact
|
|
568
|
553
|
-- with type family dependencies
|
|
569
|
554
|
|
|
570
|
|
-improveGivenLocalFunEqs :: [EqCt] -- Inert items, mixture of Given and Wanted
|
|
|
555
|
+tryGivenLocalFamEqFDs :: [EqCt] -- Inert items, mixture of Given and Wanted
|
|
571
|
556
|
-> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Given)
|
|
572
|
557
|
-> TcS Bool -- Always False (no unifications)
|
|
573
|
558
|
-- Emit equalities from interaction between two Given type-family equalities
|
|
574
|
559
|
-- e.g. (x+y1~z, x+y2~z) => (y1 ~ y2)
|
|
575
|
|
-improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
|
|
|
560
|
+tryGivenLocalFamEqFDs funeqs_for_tc fam_tc work_args work_ev work_rhs
|
|
576
|
561
|
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
|
|
577
|
562
|
= do { mapM_ (do_one ops) funeqs_for_tc
|
|
578
|
563
|
; return False } -- False: no unifications
|
| ... |
... |
@@ -592,7 +577,7 @@ improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs |
|
592
|
577
|
let pairs :: [(CoAxiomRule, TypeEqn)]
|
|
593
|
578
|
pairs = tryInteractInertFam ops fam_tc work_args inert_args
|
|
594
|
579
|
, not (null pairs)
|
|
595
|
|
- = do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args
|
|
|
580
|
+ = do { traceTcS "tryGivenLocalFamEqFDs" (vcat[ ppr fam_tc <+> ppr work_args
|
|
596
|
581
|
, text "work_ev" <+> ppr work_ev
|
|
597
|
582
|
, text "inert_ev" <+> ppr inert_ev
|
|
598
|
583
|
, ppr work_rhs
|
| ... |
... |
@@ -612,7 +597,7 @@ improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs |
|
612
|
597
|
|
|
613
|
598
|
do_one _ _ = return ()
|
|
614
|
599
|
|
|
615
|
|
-improveWantedLocalFunEqs
|
|
|
600
|
+tryWantedLocalFamEqFDs
|
|
616
|
601
|
:: [EqCt] -- Inert items (Given and Wanted)
|
|
617
|
602
|
-> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Wanted)
|
|
618
|
603
|
-> TcS Bool -- True <=> some unifications
|
| ... |
... |
@@ -621,7 +606,7 @@ improveWantedLocalFunEqs |
|
621
|
606
|
-- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y'
|
|
622
|
607
|
--
|
|
623
|
608
|
-- See Note [FunDep and implicit parameter reactions]
|
|
624
|
|
-improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs
|
|
|
609
|
+tryWantedLocalFamEqFDs funeqs_for_tc fam_tc args work_ev rhs
|
|
625
|
610
|
= do { traceTcS "interactFunEq improvements: " $
|
|
626
|
611
|
vcat [ text "Eqns:" <+> ppr improvement_eqns
|
|
627
|
612
|
, text "Candidates:" <+> ppr funeqs_for_tc ]
|
| ... |
... |
@@ -655,7 +640,7 @@ improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs |
|
655
|
640
|
-- See Note [Type inference for type families with injectivity]
|
|
656
|
641
|
do_one_injective inj_args rhs (EqCt { eq_lhs = TyFamLHS _ inert_args, eq_rhs = irhs })
|
|
657
|
642
|
| rhs `tcEqType` irhs
|
|
658
|
|
- = [mkInjectivityFDEqn inj_args args inert_args]
|
|
|
643
|
+ = [mkInjectivityFDEqn inj_args [] args inert_args]
|
|
659
|
644
|
| otherwise
|
|
660
|
645
|
= []
|
|
661
|
646
|
|