| ... |
... |
@@ -23,7 +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
|
+import GHC.Core.TyCo.Rep( Type(..) )
|
|
27
|
27
|
import GHC.Core.Predicate( EqRel(..) )
|
|
28
|
28
|
import GHC.Core.TyCon
|
|
29
|
29
|
import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart )
|
| ... |
... |
@@ -634,8 +634,7 @@ mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunD |
|
634
|
634
|
-- type families without injectivity info
|
|
635
|
635
|
-- See Note [Exploiting closed type families]
|
|
636
|
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]
|
|
|
637
|
+ | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families]
|
|
639
|
638
|
= Stage $
|
|
640
|
639
|
do { let branches = fromBranches (coAxiomBranches ax)
|
|
641
|
640
|
; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs)
|
| ... |
... |
@@ -646,6 +645,20 @@ mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) |
|
646
|
645
|
| otherwise
|
|
647
|
646
|
= Stage $ continueWith []
|
|
648
|
647
|
|
|
|
648
|
+isGenerativeType :: Type -> Bool
|
|
|
649
|
+-- True <=> This type cannot rewrite to, or be substituted to,
|
|
|
650
|
+-- a saturated type-family application
|
|
|
651
|
+-- See (CF5) in Note [Exploiting closed type families]
|
|
|
652
|
+isGenerativeType ty | Just ty' <- coreView ty = isGenerativeType ty'
|
|
|
653
|
+isGenerativeType (FunTy {}) = True
|
|
|
654
|
+isGenerativeType (CastTy ty _) = isGenerativeType ty
|
|
|
655
|
+isGenerativeType (ForAllTy {}) = True
|
|
|
656
|
+isGenerativeType (TyConApp tc _) = isGenerativeTyCon tc Nominal
|
|
|
657
|
+isGenerativeType (AppTy {}) = True
|
|
|
658
|
+isGenerativeType (LitTy {}) = True
|
|
|
659
|
+isGenerativeType (TyVarTy {}) = False
|
|
|
660
|
+isGenerativeType (CoercionTy {}) = False
|
|
|
661
|
+
|
|
649
|
662
|
hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool
|
|
650
|
663
|
-- See (CF1) in Note [Exploiting closed type families]
|
|
651
|
664
|
-- A Given is relevant if it is not apart from the Wanted
|
| ... |
... |
@@ -1121,30 +1134,34 @@ Key point: equations that are not relevant do not need to be considered for fund |
|
1121
|
1134
|
improvement in general.
|
|
1122
|
1135
|
|
|
1123
|
1136
|
(CF5) Consider
|
|
1124
|
|
- type family F a where
|
|
1125
|
|
- F (Just x) = Int
|
|
|
1137
|
+ type family F a where
|
|
|
1138
|
+ F (Just x) = Int
|
|
1126
|
1139
|
|
|
1127
|
|
- [W] F alpha ~ F (G beta)
|
|
1128
|
|
- [W] alpha ~ G beta
|
|
|
1140
|
+ [W] F alpha ~ F (G beta)
|
|
|
1141
|
+ [W] alpha ~ G beta
|
|
1129
|
1142
|
We can solve both Wanteds by `alpha := G beta`. But if we use fundeps on the
|
|
1130
|
1143
|
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
|
|
|
1144
|
+ [W] alpha ~ Just gamma
|
|
|
1145
|
+ [W] F (G beta) ~ Int
|
|
1133
|
1146
|
and try to solve them. We'll do `alpha := Just gamma`, and then it's game over;
|
|
1134
|
1147
|
we end up with these constraints that we can't solve
|
|
1135
|
|
- [W] Just gamma ~ F (G beta)
|
|
1136
|
|
- [W] Just gamma ~ G beta
|
|
|
1148
|
+ [W] Just gamma ~ F (G beta)
|
|
|
1149
|
+ [W] Just gamma ~ G beta
|
|
1137
|
1150
|
This actually happens when compiling the libarary `type-rows`, in Data.Row.Variants.
|
|
1138
|
1151
|
|
|
1139
|
1152
|
Even if there is only one relevant equation, we can only use it /if/ we are sure that we
|
|
1140
|
1153
|
cannot solve the current Wanted by reflexivity; that is, if we must do a type-family
|
|
1141
|
1154
|
reduction to solve it. So if the Wanted is
|
|
1142
|
|
- ```
|
|
1143
|
|
- [W] F tys ~ rhs
|
|
1144
|
|
- ```
|
|
|
1155
|
+ [W] F tys ~ rhs
|
|
1145
|
1156
|
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`.
|
|
|
1157
|
+ is if `rhs` is headed by a generative type constructor. See `isGenerativeType`.
|
|
|
1158
|
+
|
|
|
1159
|
+ It's important for `isGenerativeType` to look through casts. Consider T13822
|
|
|
1160
|
+ type I :: Ty k -> IK k
|
|
|
1161
|
+ type family I t = res | res -> t where
|
|
|
1162
|
+ I TInt = Int |> g -- where g :: Type ~# IK k
|
|
|
1163
|
+ and [W] I alpha ~ Int |> g2
|
|
|
1164
|
+ Here we definiteily want to take advantage of injectivity.
|
|
1148
|
1165
|
|
|
1149
|
1166
|
Note [Cache-caused loops]
|
|
1150
|
1167
|
~~~~~~~~~~~~~~~~~~~~~~~~~
|