Midstream changes to deal with spontaneous solving and flatten skolem equivalence...

[ghc-hetmet.git] / compiler / typecheck / TcSMonad.lhs

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 5c41ff1..a487fe0 100644 (file)
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -44,6 +44,10 @@ module TcSMonad (
 
     isGoodRecEv,
 
+    zonkTcTypeTcS,                              -- Zonk through the TyBinds of the Tcs Monad
+    compatKind,
+
+
     isTouchableMetaTyVar,
     isTouchableMetaTyVar_InRange, 
 
@@ -144,12 +148,16 @@ data CanonicalCt
   | CTyEqCan {  -- tv ~ xi     (recall xi means function free)
        -- Invariant: 
        --   * tv not in tvs(xi)   (occurs check)
-       --   * If constraint is given then typeKind xi ==  typeKind tv 
+       --   * If constraint is given then typeKind xi `compatKind` typeKind tv 
        --                See Note [Spontaneous solving and kind compatibility] 
+       --   * if xi is a flatten skolem then tv must be a flatten skolem
+       --     i.e. equalities prefer flatten skolems in their LHS. 
+       --                See Note [Loopy Spontaneous Solving, Example 4]
+       --                Also related to [Flatten Skolem Equivalence Classes]
       cc_id     :: EvVar, 
       cc_flavor :: CtFlavor, 
-      cc_tyvar :: TcTyVar, 
-      cc_rhs   :: Xi
+      cc_tyvar  :: TcTyVar, 
+      cc_rhs    :: Xi
     }
 
   | CFunEqCan {  -- F xis ~ xi  
@@ -157,7 +165,7 @@ data CanonicalCt
                  --            * cc_rhs is not a touchable unification variable 
                  --                   See Note [No touchables as FunEq RHS]
                  --            * If constraint is given then 
-                 --                 typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
+                 --                 typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
       cc_id     :: EvVar,
       cc_flavor :: CtFlavor, 
       cc_fun    :: TyCon,      -- A type function
@@ -167,6 +175,9 @@ data CanonicalCt
                    
     }
 
+compatKind :: Kind -> Kind -> Bool 
+compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
+
 makeGivens :: CanonicalCts -> CanonicalCts
 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
           -- The UnkSkol doesn't matter because these givens are
@@ -882,6 +893,20 @@ matchFam tycon args
        }
 
 
+zonkTcTypeTcS :: TcType -> TcS TcType
+-- Zonk through the TyBinds of the Tcs Monad
+zonkTcTypeTcS ty 
+  = do { subst <- getTcSTyBindsMap >>= return . varEnvElts 
+       ; let (dom,rng)  = unzip subst 
+             apply_once = substTyWith dom rng 
+       ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
+       ; return (substTyWith dom rng_idemp ty) }
+
+                        
+
+
+
+
 -- Functional dependencies, instantiation of equations
 -------------------------------------------------------