| ... |
... |
@@ -522,9 +522,6 @@ mkTopFamEqFDs fam_tc work_args work_rhs |
|
522
|
522
|
|
|
523
|
523
|
| Just ax <- isClosedFamilyTyCon_maybe fam_tc
|
|
524
|
524
|
= -- Closed type families
|
|
525
|
|
- -- Look at the top-level axioms; we effectively infer injectivity,
|
|
526
|
|
- -- so we don't need tyConInjectivtyInfo. This works fine for closed
|
|
527
|
|
- -- type families without injectivity info
|
|
528
|
525
|
mkTopClosedFamEqFDs ax work_args work_rhs
|
|
529
|
526
|
|
|
530
|
527
|
| otherwise
|
| ... |
... |
@@ -551,6 +548,10 @@ tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eq |
|
551
|
548
|
-- User-defined type families
|
|
552
|
549
|
-----------------------------------------
|
|
553
|
550
|
mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns]
|
|
|
551
|
+-- Look at the top-level axioms; we effectively infer injectivity,
|
|
|
552
|
+-- so we don't need tyConInjectivtyInfo. This works fine for closed
|
|
|
553
|
+-- type families without injectivity info
|
|
|
554
|
+-- See Note [Exploiting closed type families]
|
|
554
|
555
|
mkTopClosedFamEqFDs ax work_args work_rhs
|
|
555
|
556
|
= do { let branches = fromBranches (coAxiomBranches ax)
|
|
556
|
557
|
; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs)
|
| ... |
... |
@@ -847,6 +848,184 @@ For /built-in/ type families, it's pretty similar, except that |
|
847
|
848
|
equation would indeed be the one to fire. So we call `apartnessCheck`
|
|
848
|
849
|
on the branch to ensure this, in `mkTopUserFamEqFDs`.
|
|
849
|
850
|
|
|
|
851
|
+Definition [Relevance]
|
|
|
852
|
+~~~~~~~~~~~~~~~~~~~~~~
|
|
|
853
|
+We say that a closed-type-family equation `F lhs = rhs` is
|
|
|
854
|
+ /relevant/ for a Wanted [W] F wlhs ~ wrhs
|
|
|
855
|
+iff
|
|
|
856
|
+ (R1) (lhs,rhs) pre-unifies with (wlhs,wrhs) yielding substitution S.
|
|
|
857
|
+ See (RW1),(RW2), (RW3)
|
|
|
858
|
+
|
|
|
859
|
+ (R2) There is no earlier equation that matches S(lhs). See (RW4) below.
|
|
|
860
|
+
|
|
|
861
|
+(RW1) Pre-unification treats type-family applications as binding to anything,
|
|
|
862
|
+ rather like type variables. If two types don't even pre-unify, we say that they
|
|
|
863
|
+ are /apart/. It is done by `tcUnifyTysForInjectivity`.
|
|
|
864
|
+
|
|
|
865
|
+(RW2) lhs and wlhs are of course each a list of types. We don't really form a
|
|
|
866
|
+ tuple (lhs,rhs); we just pre-unify the list (rhs_ty : lhs_tys).
|
|
|
867
|
+
|
|
|
868
|
+(RW3) Why "pre-unifies with" rather than "unifies with"? Answer: see Section 5.2
|
|
|
869
|
+ in "Injective Type Families for Haskell". A concrete example is test T12522a:
|
|
|
870
|
+
|
|
|
871
|
+ newtype I a = I a
|
|
|
872
|
+
|
|
|
873
|
+ type family Curry (as :: [Type]) b = f | f -> as b where
|
|
|
874
|
+ Curry '[] b = I b
|
|
|
875
|
+ Curry (a:as) b = a -> Curry as b
|
|
|
876
|
+
|
|
|
877
|
+ [W] Curry alpha beta ~ (gamma -> String -> I String)
|
|
|
878
|
+
|
|
|
879
|
+
|
|
|
880
|
+ Clearly the RHS is apart from the first equation and we want to fire injectivity
|
|
|
881
|
+ on the second equation.
|
|
|
882
|
+
|
|
|
883
|
+(RW4) Why "no earlier equation matches" in conditoin (R2)? Consider the family
|
|
|
884
|
+
|
|
|
885
|
+ type family Bak a = r where
|
|
|
886
|
+ Bak Int = Char -- B1
|
|
|
887
|
+ Bak Char = Int -- B2
|
|
|
888
|
+ Bak a = a -- B3
|
|
|
889
|
+
|
|
|
890
|
+ and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted.
|
|
|
891
|
+ You might think that (B3) could be instantiated to Bak Char ~ Char; but
|
|
|
892
|
+ actually that instantiation will never fire because (B2) Bak Char ~ Int would
|
|
|
893
|
+ fire first. So the only way to return a Char is if the argment is Int; so we
|
|
|
894
|
+ can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant.
|
|
|
895
|
+
|
|
|
896
|
+ That is the reason for condition (R2) in the definition of Relevance above.
|
|
|
897
|
+ A watertight proof that this is the Right Thing is not very easy. See more
|
|
|
898
|
+ discussion in #23162.
|
|
|
899
|
+
|
|
|
900
|
+Note [Exploiting closed type families]
|
|
|
901
|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
902
|
+Suppose we have
|
|
|
903
|
+ type family F a b where
|
|
|
904
|
+ F Int Bool = Bool -- (F1)
|
|
|
905
|
+ F Int Char = Char -- (F2)
|
|
|
906
|
+ F Bool a = Char -- (F3)
|
|
|
907
|
+
|
|
|
908
|
+ [W] F Int alpha ~ Char
|
|
|
909
|
+
|
|
|
910
|
+The /only/ way to solve this Wanted is using (F2), so we can safely unify
|
|
|
911
|
+alpha:=Char without risking losing any solutions. That is what
|
|
|
912
|
+`mkTopClosedFamEqFDs` does. Ticket #23162 has lots of background detail
|
|
|
913
|
+
|
|
|
914
|
+More precisely, here is the Closed Family Fundep Algorithm (CFFA)
|
|
|
915
|
+
|
|
|
916
|
+ IF * F a is a closed type family.
|
|
|
917
|
+ * We are trying to solve [W] F wlhs ~ wrhs.
|
|
|
918
|
+ * There are no "relevant" Givens [G] F lhs ~ rhs. See (CF1) below.
|
|
|
919
|
+ * F has exactly one equation, F lhs = rhs that is "relevant" for that Wanted
|
|
|
920
|
+ THEN
|
|
|
921
|
+ we can emit and solve the fundep equalities:
|
|
|
922
|
+ [W] wlhs1 ~ lhs1
|
|
|
923
|
+ ...
|
|
|
924
|
+ [W] wlhsn ~ lhsn
|
|
|
925
|
+ [W] wrhs ~ rhs See (CF2) below.
|
|
|
926
|
+ with fresh unification vars in lhs and rhs for the quantified variables of the
|
|
|
927
|
+ equation.
|
|
|
928
|
+
|
|
|
929
|
+See Definition [Relevance] for what "relevant" means.
|
|
|
930
|
+We need to take care about non-termination; see (CF3).
|
|
|
931
|
+
|
|
|
932
|
+Key point: equations that are not relevant do not need to be considered for fundeps at all.
|
|
|
933
|
+
|
|
|
934
|
+(CF1) Why "no relevant Givens"? Consider test `CEqCanOccursCheck`:
|
|
|
935
|
+
|
|
|
936
|
+ type family F a where
|
|
|
937
|
+ F Bool = Bool
|
|
|
938
|
+ type family G a b where
|
|
|
939
|
+ G a a = a
|
|
|
940
|
+
|
|
|
941
|
+ foo :: (F a ~ a, F a ~ b) => G a b -> ()
|
|
|
942
|
+
|
|
|
943
|
+ In the ambiguity check for foo we get
|
|
|
944
|
+ [G] F a ~ a
|
|
|
945
|
+ [G] F a ~ b
|
|
|
946
|
+ [W] F alpha ~ alpha
|
|
|
947
|
+ [W] F alpha ~ beta
|
|
|
948
|
+ [W] G a b ~ G alpha beta
|
|
|
949
|
+
|
|
|
950
|
+ Now use algoritm (CFFA) on [W] F alpha ~ alpha. There is only one
|
|
|
951
|
+ equation for F, and it is relevant, so we gaily emit the fundep equality
|
|
|
952
|
+ [W] alpha ~ Bool, and we are immediately dead. We end up with
|
|
|
953
|
+ • Could not deduce ‘b ~ Bool’
|
|
|
954
|
+ from the context: (F a ~ a, F a ~ b)
|
|
|
955
|
+
|
|
|
956
|
+ It is true that the only way a caller can satisfy F a ~ a is by instantiating
|
|
|
957
|
+ a to Bool; but we don't have /evidence/ for that which we can use to satisfy
|
|
|
958
|
+ b ~ Bool.
|
|
|
959
|
+
|
|
|
960
|
+ The trouble is that (CFFA) relies on knowing /all/ the equations for F;
|
|
|
961
|
+ but in this case we have some Given constraints that locally extend F.
|
|
|
962
|
+
|
|
|
963
|
+ This relates closely to
|
|
|
964
|
+ Note [Do local fundeps before top-level instances] and
|
|
|
965
|
+ Note [Do fundeps last] (which are saying much the same thing)
|
|
|
966
|
+
|
|
|
967
|
+ These Notes are extremely delicate. Suppose a local Given doesn't give rise
|
|
|
968
|
+ to a fundep equation and we move on to the top-level fundeps; but then after
|
|
|
969
|
+ some other constraints are solved the local Given would fire. Indeed this is
|
|
|
970
|
+ exactly what happens above!
|
|
|
971
|
+
|
|
|
972
|
+ Solution: Only run (CFFA) if there are no relevant Givens. This is much more
|
|
|
973
|
+ robust than "only run (CFFA) if attempting local fundeps gives rise to
|
|
|
974
|
+ equations" because if a Given is irrelevant is is forever irrelevant. It's a
|
|
|
975
|
+ bit like `noMatchableGivenDicts` and `mightEqualLater` for dictionaries.
|
|
|
976
|
+ Indeed we should probably apply a similar check when doing fundeps on
|
|
|
977
|
+ dictionaries.
|
|
|
978
|
+
|
|
|
979
|
+(CF2) Fundeps from RHS as well as LHS. Consider this from test T6018:
|
|
|
980
|
+
|
|
|
981
|
+ type family Bak a = r where
|
|
|
982
|
+ Bak Int = Char
|
|
|
983
|
+ Bak Char = Int
|
|
|
984
|
+ Bak a = a
|
|
|
985
|
+
|
|
|
986
|
+ and [W] Bak alpha ~ (). Only the last equation is relevant, but we clearly
|
|
|
987
|
+ don't want to just produce a new fundep Wanted for the LHS: beta ~ alpha,
|
|
|
988
|
+ where beta is freshly instantiated from a. We must /also/ produce an equality
|
|
|
989
|
+ [W] beta ~ () from the RHS. Hence the [W] wrhs ~ rhs in (CFFA).
|
|
|
990
|
+
|
|
|
991
|
+(CF3) Algorithm (CFFA) can diverge, just as ordinary fundeps can, as discussed
|
|
|
992
|
+ extensively in the paper "Understanding functional dependencies via constraint
|
|
|
993
|
+ handling rules". Example (test T16512a):
|
|
|
994
|
+
|
|
|
995
|
+ type family LV as b where
|
|
|
996
|
+ LV (a : as) b = a -> LV as b
|
|
|
997
|
+
|
|
|
998
|
+ [W] LV as bsk ~ LV as (ask->bsk)
|
|
|
999
|
+
|
|
|
1000
|
+ Here `as` is a unification variable, while `ask` and `bsk` are skolems.
|
|
|
1001
|
+ There is one relevant equation, because there is only one equation in the
|
|
|
1002
|
+ family! Hence algorithm (CFFA) generates new equalities
|
|
|
1003
|
+ x:asx ~ as
|
|
|
1004
|
+ bx ~ bsk
|
|
|
1005
|
+ (ax -> LV asx bx) ~ LV as (ask->bsk)
|
|
|
1006
|
+
|
|
|
1007
|
+ where ax, asx and bx are fresh unification variables. We can solve:
|
|
|
1008
|
+ as := ax:asx
|
|
|
1009
|
+ bx := bsk
|
|
|
1010
|
+
|
|
|
1011
|
+ Leaving us with
|
|
|
1012
|
+ (ax -> LV asx bsk) ~ LV (ax:asx) (ask->bsk)
|
|
|
1013
|
+ -->{reduce RHS with the equation for LV}
|
|
|
1014
|
+ (ax -> LV asx bsk) ~ (ax -> LV asx (ask->bsk))
|
|
|
1015
|
+ -->{decompose ->)
|
|
|
1016
|
+ LV asx bsk ~ LV asx (ask->bsk)
|
|
|
1017
|
+
|
|
|
1018
|
+ And now we are back where we started -- loop.
|
|
|
1019
|
+
|
|
|
1020
|
+ We solve this by bumping the `ctLocDepth` in `solveFunDeps`, and imposing
|
|
|
1021
|
+ a depth bound. See the call to `bumpReductionDepth`.
|
|
|
1022
|
+
|
|
|
1023
|
+(CF4) If one of the fundeps generated by interacting with the local equalities is
|
|
|
1024
|
+ definitely insoluble (e.g. Int~Bool) then there is no point in continuing to
|
|
|
1025
|
+ look at the global type-family definitions. That can happen. It came up when
|
|
|
1026
|
+ I was looking at non-termination for closed type families, but it's a small
|
|
|
1027
|
+ improvement in general.
|
|
|
1028
|
+
|
|
850
|
1029
|
Note [Cache-caused loops]
|
|
851
|
1030
|
~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
852
|
1031
|
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
|
| ... |
... |
@@ -903,6 +1082,7 @@ solveFunDeps work_ev fd_eqns |
|
903
|
1082
|
| otherwise
|
|
904
|
1083
|
= do { traceTcS "bumping" (ppr work_ev)
|
|
905
|
1084
|
; loc' <- bumpReductionDepth (ctEvLoc work_ev) (ctEvPred work_ev)
|
|
|
1085
|
+ -- See (CF3) in Note [Exploiting closed type families]
|
|
906
|
1086
|
|
|
907
|
1087
|
; (unifs, residual)
|
|
908
|
1088
|
<- reportFineGrainUnifications $
|
| ... |
... |
@@ -923,6 +1103,7 @@ solveFunDeps work_ev fd_eqns |
|
923
|
1103
|
; kickOutAfterUnification unifs
|
|
924
|
1104
|
|
|
925
|
1105
|
; return (insolubleWC residual, not (isEmptyVarSet unifs)) }
|
|
|
1106
|
+ -- insolubleWC: see (CF3) in Note [Exploiting closed type families]
|
|
926
|
1107
|
where
|
|
927
|
1108
|
do_fundeps :: UnifyEnv -> TcM ()
|
|
928
|
1109
|
do_fundeps env = mapM_ (do_one env) fd_eqns
|