Tidy up RuntimeUnkSkols a bit more

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

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 5c41ff1..416ac80 100644 (file)
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -10,6 +10,8 @@ module TcSMonad (
     makeGivens, makeSolvedByInst,
 
     CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, 
+    isGivenCt, isWantedCt, 
+
     DerivedOrig (..), 
     canRewrite, canSolve,
     combineCtLoc, mkGivenFlavor,
@@ -44,6 +46,10 @@ module TcSMonad (
 
     isGoodRecEv,
 
+    zonkTcTypeTcS,                              -- Zonk through the TyBinds of the Tcs Monad
+    compatKind,
+
+
     isTouchableMetaTyVar,
     isTouchableMetaTyVar_InRange, 
 
@@ -136,7 +142,7 @@ data CanonicalCt
   | CIPCan {   -- ?x::tau
       -- See note [Canonical implicit parameter constraints].
       cc_id     :: EvVar,
-      cc_flavor :: CtFlavor, 
+      cc_flavor :: CtFlavor,
       cc_ip_nm  :: IPName Name,
       cc_ip_ty  :: TcTauType
     }
@@ -144,12 +150,17 @@ 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' can only be: 
+       --              - a flatten skolem or a unification variable
+       --     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 +168,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 +178,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
@@ -320,6 +334,11 @@ isDerivedByInst :: CtFlavor -> Bool
 isDerivedByInst (Derived _ DerInst) = True 
 isDerivedByInst _                   = False 
 
+isWantedCt :: CanonicalCt -> Bool 
+isWantedCt ct = isWanted (cc_flavor ct)
+isGivenCt :: CanonicalCt -> Bool 
+isGivenCt ct = isGiven (cc_flavor ct) 
+
 canSolve :: CtFlavor -> CtFlavor -> Bool 
 -- canSolve ctid1 ctid2 
 -- The constraint ctid1 can be used to solve ctid2 
@@ -882,6 +901,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
 -------------------------------------------------------