| ... |
... |
@@ -23,6 +23,7 @@ import GHC.Tc.Types.Constraint |
|
23
|
23
|
|
|
24
|
24
|
import GHC.Core.FamInstEnv
|
|
25
|
25
|
import GHC.Core.Coercion
|
|
|
26
|
+import GHC.Core.Type( tyConAppTyCon_maybe )
|
|
26
|
27
|
import GHC.Core.Predicate( EqRel(..) )
|
|
27
|
28
|
import GHC.Core.TyCon
|
|
28
|
29
|
import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart )
|
| ... |
... |
@@ -633,6 +634,8 @@ mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunD |
|
633
|
634
|
-- type families without injectivity info
|
|
634
|
635
|
-- See Note [Exploiting closed type families]
|
|
635
|
636
|
mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs })
|
|
|
637
|
+ | Just tc <- tyConAppTyCon_maybe work_rhs
|
|
|
638
|
+ , isGenerativeTyCon tc Nominal -- See (CF5) in Note [Exploiting closed type families]
|
|
636
|
639
|
= Stage $
|
|
637
|
640
|
do { let branches = fromBranches (coAxiomBranches ax)
|
|
638
|
641
|
; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs)
|
| ... |
... |
@@ -640,6 +643,8 @@ mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) |
|
640
|
643
|
[] -> insolubleFunDep True ev -- See (IFD0) in Note [Insoluble fundeps]
|
|
641
|
644
|
[eqn] -> continueWith [eqn] -- If there is just one relevant equation, use it
|
|
642
|
645
|
_ -> continueWith [] }
|
|
|
646
|
+ | otherwise
|
|
|
647
|
+ = Stage $ continueWith []
|
|
643
|
648
|
|
|
644
|
649
|
hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool
|
|
645
|
650
|
-- See (CF1) in Note [Exploiting closed type families]
|
| ... |
... |
@@ -1115,6 +1120,32 @@ Key point: equations that are not relevant do not need to be considered for fund |
|
1115
|
1120
|
I was looking at non-termination for closed type families, but it's a small
|
|
1116
|
1121
|
improvement in general.
|
|
1117
|
1122
|
|
|
|
1123
|
+(CF5) Consider
|
|
|
1124
|
+ type family F a where
|
|
|
1125
|
+ F (Just x) = Int
|
|
|
1126
|
+
|
|
|
1127
|
+ [W] F alpha ~ F (G beta)
|
|
|
1128
|
+ [W] alpha ~ G beta
|
|
|
1129
|
+ We can solve both Wanteds by `alpha := G beta`. But if we use fundeps on the
|
|
|
1130
|
+ first Wanted, we see that there is just one relevant equation, so we'll emit
|
|
|
1131
|
+ [W] alpha ~ Just gamma
|
|
|
1132
|
+ [W] F (G beta) ~ Int
|
|
|
1133
|
+ and try to solve them. We'll do `alpha := Just gamma`, and then it's game over;
|
|
|
1134
|
+ we end up with these constraints that we can't solve
|
|
|
1135
|
+ [W] Just gamma ~ F (G beta)
|
|
|
1136
|
+ [W] Just gamma ~ G beta
|
|
|
1137
|
+ This actually happens when compiling the libarary `type-rows`, in Data.Row.Variants.
|
|
|
1138
|
+
|
|
|
1139
|
+ Even if there is only one relevant equation, we can only use it /if/ we are sure that we
|
|
|
1140
|
+ cannot solve the current Wanted by reflexivity; that is, if we must do a type-family
|
|
|
1141
|
+ reduction to solve it. So if the Wanted is
|
|
|
1142
|
+ ```
|
|
|
1143
|
+ [W] F tys ~ rhs
|
|
|
1144
|
+ ```
|
|
|
1145
|
+ we must be sure that `rhs` can't turn into `F tys`. The only way to be sure of that
|
|
|
1146
|
+ is if `rhs` is headed by a generative type constructor. See the test for
|
|
|
1147
|
+ `isGenerativeTyCon` in `mkTopClosedFamEqFDs`.
|
|
|
1148
|
+
|
|
1118
|
1149
|
Note [Cache-caused loops]
|
|
1119
|
1150
|
~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
1120
|
1151
|
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
|