| ... |
... |
@@ -1792,12 +1792,12 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM () |
|
1792
|
1792
|
-- Why saturated? See (ATF4) in Note [Apartness and type families]
|
|
1793
|
1793
|
uVarOrFam env ty1 ty2 kco
|
|
1794
|
1794
|
= do { substs <- getSubstEnvs
|
|
1795
|
|
- ; pprTrace "uVarOrFam" (vcat
|
|
1796
|
|
- [ text "ty1" <+> ppr ty1
|
|
1797
|
|
- , text "ty2" <+> ppr ty2
|
|
1798
|
|
- , text "tv_env" <+> ppr (um_tv_env substs)
|
|
1799
|
|
- , text "fam_env" <+> ppr (um_fam_env substs) ]) $
|
|
1800
|
|
- go NotSwapped substs ty1 ty2 kco }
|
|
|
1795
|
+-- ; pprTrace "uVarOrFam" (vcat
|
|
|
1796
|
+-- [ text "ty1" <+> ppr ty1
|
|
|
1797
|
+-- , text "ty2" <+> ppr ty2
|
|
|
1798
|
+-- , text "tv_env" <+> ppr (um_tv_env substs)
|
|
|
1799
|
+-- , text "fam_env" <+> ppr (um_fam_env substs) ]) $
|
|
|
1800
|
+ ; go NotSwapped substs ty1 ty2 kco }
|
|
1801
|
1801
|
where
|
|
1802
|
1802
|
-- `go` takes two bites at the cherry; if the first one fails
|
|
1803
|
1803
|
-- it swaps the arguments and tries again; and then it fails.
|
| ... |
... |
@@ -1901,15 +1901,14 @@ uVarOrFam env ty1 ty2 kco |
|
1901
|
1901
|
-- Check for equality F tys1 ~ F tys2
|
|
1902
|
1902
|
| Just (tc2, tys2) <- isSatFamApp ty2
|
|
1903
|
1903
|
, tc1 == tc2
|
|
1904
|
|
- = go_fam_fam tc1 tys1 tys2 kco
|
|
|
1904
|
+ = go_fam_fam substs tc1 tys1 tys2 kco
|
|
1905
|
1905
|
|
|
1906
|
1906
|
-- Now check if we can bind the (F tys) to the RHS
|
|
1907
|
1907
|
-- This can happen even when matching: see (ATF7)
|
|
1908
|
1908
|
| BindMe <- um_bind_fam_fun env tc1 tys1 rhs
|
|
1909
|
1909
|
= if uOccursCheck substs lhs rhs
|
|
1910
|
1910
|
then maybeApart MARInfinite
|
|
1911
|
|
- else do { pprTrace "extend1" (ppr tc1 <+> ppr tys1 $$ ppr rhs) $
|
|
1912
|
|
- extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13)
|
|
|
1911
|
+ else do { extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13)
|
|
1913
|
1912
|
; maybeApart MARTypeFamily }
|
|
1914
|
1913
|
|
|
1915
|
1914
|
-- Swap in case of (F a b) ~ (G c d e)
|
| ... |
... |
@@ -1930,7 +1929,7 @@ uVarOrFam env ty1 ty2 kco |
|
1930
|
1929
|
-----------------------------
|
|
1931
|
1930
|
-- go_fam_fam: LHS and RHS are both saturated type-family applications,
|
|
1932
|
1931
|
-- for the same type-family F
|
|
1933
|
|
- go_fam_fam tc tys1 tys2 kco
|
|
|
1932
|
+ go_fam_fam substs tc tys1 tys2 kco
|
|
1934
|
1933
|
-- Decompose (F tys1 ~ F tys2): (ATF9)
|
|
1935
|
1934
|
-- Use injectivity information of F: (ATF10)
|
|
1936
|
1935
|
-- But first bind the type-fam if poss: (ATF11)
|
| ... |
... |
@@ -1950,14 +1949,12 @@ uVarOrFam env ty1 ty2 kco |
|
1950
|
1949
|
bind_fam_if_poss
|
|
1951
|
1950
|
| not (um_unif env) -- Not when matching (ATF11-1)
|
|
1952
|
1951
|
= return ()
|
|
1953
|
|
- | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys);
|
|
1954
|
|
- = return () -- otherwise we'd build an infinite substitution
|
|
1955
|
1952
|
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
|
|
1956
|
|
- = pprTrace "extend2" (ppr tc <+> ppr tys1 $$ ppr rhs1) $
|
|
|
1953
|
+ = unless (uOccursCheck substs (TyFamLHS tc tys1) rhs1) $
|
|
1957
|
1954
|
extendFamEnv tc tys1 rhs1
|
|
1958
|
|
- | um_unif env
|
|
1959
|
|
- , BindMe <- um_bind_fam_fun env tc tys2 rhs2
|
|
1960
|
|
- = pprTrace "extend3" (ppr tc <+> ppr tys2 $$ ppr rhs2) $
|
|
|
1955
|
+ -- At this point um_unif=True, so we can unify either way
|
|
|
1956
|
+ | BindMe <- um_bind_fam_fun env tc tys2 rhs2
|
|
|
1957
|
+ = unless (uOccursCheck substs (TyFamLHS tc tys2) rhs2) $
|
|
1961
|
1958
|
extendFamEnv tc tys2 rhs2
|
|
1962
|
1959
|
| otherwise
|
|
1963
|
1960
|
= return ()
|
| ... |
... |
@@ -1967,14 +1964,13 @@ uVarOrFam env ty1 ty2 kco |
|
1967
|
1964
|
|
|
1968
|
1965
|
|
|
1969
|
1966
|
uOccursCheck :: UMState -> CanEqLHS -> Type -> Bool
|
|
1970
|
|
--- See Note [The occurs check in the Core unifier] and (ATF13)
|
|
|
1967
|
+-- See Note [The occurs check in the Core unifier] and (ATF14)
|
|
1971
|
1968
|
uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty
|
|
1972
|
1969
|
= go emptyVarSet ty
|
|
1973
|
1970
|
where
|
|
1974
|
1971
|
go :: TyCoVarSet -- Bound by enclosing foralls
|
|
1975
|
1972
|
-> Type -> Bool
|
|
1976
|
|
- go bvs ty | Just ty' <- pprTrace "uOccursCheck:go" (ppr lhs $$ ppr ty) $
|
|
1977
|
|
- coreView ty = go bvs ty'
|
|
|
1973
|
+ go bvs ty | Just ty' <- coreView ty = go bvs ty'
|
|
1978
|
1974
|
go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv
|
|
1979
|
1975
|
= go bvs ty'
|
|
1980
|
1976
|
| TyVarLHS tv' <- lhs, tv==tv'
|
| ... |
... |
@@ -1999,8 +1995,7 @@ uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty |
|
1999
|
1995
|
go_tc bvs tc tys
|
|
2000
|
1996
|
| isTypeFamilyTyCon tc
|
|
2001
|
1997
|
, Just ty' <- lookupFamEnv fam_env tc (take arity tys)
|
|
2002
|
|
- = pprTrace "lookup" (ppr tc <+> ppr tys $$ ppr ty') $
|
|
2003
|
|
- go bvs ty' || any (go bvs) (drop arity tys)
|
|
|
1998
|
+ = go bvs ty' || any (go bvs) (drop arity tys)
|
|
2004
|
1999
|
|
|
2005
|
2000
|
| TyFamLHS tc' tys' <- lhs
|
|
2006
|
2001
|
, tc == tc'
|
| ... |
... |
@@ -2168,7 +2163,6 @@ extendCvEnv cv co = UM $ \state -> |
|
2168
|
2163
|
|
|
2169
|
2164
|
extendFamEnv :: TyCon -> [Type] -> Type -> UM ()
|
|
2170
|
2165
|
extendFamEnv tc tys ty = UM $ \state ->
|
|
2171
|
|
- pprTrace "Adding fam env" (ppr tc <+> ppr tys $$ text ":->" <+> ppr ty) $
|
|
2172
|
2166
|
Unifiable (state { um_fam_env = extend (um_fam_env state) tc }, ())
|
|
2173
|
2167
|
where
|
|
2174
|
2168
|
extend :: FamSubstEnv -> TyCon -> FamSubstEnv
|