| ... |
... |
@@ -1792,7 +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
|
|
- ; 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 }
|
|
1796
|
1801
|
where
|
|
1797
|
1802
|
-- `go` takes two bites at the cherry; if the first one fails
|
|
1798
|
1803
|
-- it swaps the arguments and tries again; and then it fails.
|
| ... |
... |
@@ -1903,7 +1908,8 @@ uVarOrFam env ty1 ty2 kco |
|
1903
|
1908
|
| BindMe <- um_bind_fam_fun env tc1 tys1 rhs
|
|
1904
|
1909
|
= if uOccursCheck substs lhs rhs
|
|
1905
|
1910
|
then maybeApart MARInfinite
|
|
1906
|
|
- else do { extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13)
|
|
|
1911
|
+ else do { pprTrace "extend1" (ppr tc1 <+> ppr tys1 $$ ppr rhs) $
|
|
|
1912
|
+ extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13)
|
|
1907
|
1913
|
; maybeApart MARTypeFamily }
|
|
1908
|
1914
|
|
|
1909
|
1915
|
-- Swap in case of (F a b) ~ (G c d e)
|
| ... |
... |
@@ -1947,10 +1953,12 @@ uVarOrFam env ty1 ty2 kco |
|
1947
|
1953
|
| tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys);
|
|
1948
|
1954
|
= return () -- otherwise we'd build an infinite substitution
|
|
1949
|
1955
|
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
|
|
1950
|
|
- = extendFamEnv tc tys1 rhs1
|
|
|
1956
|
+ = pprTrace "extend2" (ppr tc <+> ppr tys1 $$ ppr rhs1) $
|
|
|
1957
|
+ extendFamEnv tc tys1 rhs1
|
|
1951
|
1958
|
| um_unif env
|
|
1952
|
1959
|
, BindMe <- um_bind_fam_fun env tc tys2 rhs2
|
|
1953
|
|
- = extendFamEnv tc tys2 rhs2
|
|
|
1960
|
+ = pprTrace "extend3" (ppr tc <+> ppr tys2 $$ ppr rhs2) $
|
|
|
1961
|
+ extendFamEnv tc tys2 rhs2
|
|
1954
|
1962
|
| otherwise
|
|
1955
|
1963
|
= return ()
|
|
1956
|
1964
|
|
| ... |
... |
@@ -1965,7 +1973,8 @@ uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty |
|
1965
|
1973
|
where
|
|
1966
|
1974
|
go :: TyCoVarSet -- Bound by enclosing foralls
|
|
1967
|
1975
|
-> Type -> Bool
|
|
1968
|
|
- go bvs ty | Just ty' <- coreView ty = go bvs ty'
|
|
|
1976
|
+ go bvs ty | Just ty' <- pprTrace "uOccursCheck:go" (ppr lhs $$ ppr ty) $
|
|
|
1977
|
+ coreView ty = go bvs ty'
|
|
1969
|
1978
|
go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv
|
|
1970
|
1979
|
= go bvs ty'
|
|
1971
|
1980
|
| TyVarLHS tv' <- lhs, tv==tv'
|
| ... |
... |
@@ -1990,12 +1999,13 @@ uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty |
|
1990
|
1999
|
go_tc bvs tc tys
|
|
1991
|
2000
|
| isTypeFamilyTyCon tc
|
|
1992
|
2001
|
, Just ty' <- lookupFamEnv fam_env tc (take arity tys)
|
|
1993
|
|
- = go bvs ty' || any (go bvs) (drop arity tys)
|
|
|
2002
|
+ = pprTrace "lookup" (ppr tc <+> ppr tys $$ ppr ty') $
|
|
|
2003
|
+ go bvs ty' || any (go bvs) (drop arity tys)
|
|
1994
|
2004
|
|
|
1995
|
2005
|
| TyFamLHS tc' tys' <- lhs
|
|
1996
|
2006
|
, tc == tc'
|
|
1997
|
2007
|
, tys `lengthAtLeast` arity -- Saturated, or over-saturated
|
|
1998
|
|
- , and (zipWith tcEqType tys tys')
|
|
|
2008
|
+ , tcEqTyConAppArgs tys tys'
|
|
1999
|
2009
|
= True
|
|
2000
|
2010
|
|
|
2001
|
2011
|
| otherwise
|
| ... |
... |
@@ -2158,6 +2168,7 @@ extendCvEnv cv co = UM $ \state -> |
|
2158
|
2168
|
|
|
2159
|
2169
|
extendFamEnv :: TyCon -> [Type] -> Type -> UM ()
|
|
2160
|
2170
|
extendFamEnv tc tys ty = UM $ \state ->
|
|
|
2171
|
+ pprTrace "Adding fam env" (ppr tc <+> ppr tys $$ text ":->" <+> ppr ty) $
|
|
2161
|
2172
|
Unifiable (state { um_fam_env = extend (um_fam_env state) tc }, ())
|
|
2162
|
2173
|
where
|
|
2163
|
2174
|
extend :: FamSubstEnv -> TyCon -> FamSubstEnv
|