Basic set up for global family instance environment

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

diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 727d0ab..94ea3f9 100644 (file)
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -169,8 +169,8 @@ import Type         (       -- Re-exports
                          pprType, pprParendType, pprTyThingCategory,
                          pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
-import Coercion         ( splitForAllCo_maybe )
+import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, isOpenTyCon,
+                         synTyConDefn, tyConUnique )    
 import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
 import Class           ( Class )
 import Var             ( TyVar, Id, isCoVar, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
@@ -344,6 +344,7 @@ data SkolemInfo
        -- The rest are for non-scoped skolems
   | ClsSkol Class      -- Bound at a class decl
   | InstSkol Id                -- Bound at an instance decl
+  | FamInstSkol TyCon  -- Bound at a family instance decl
   | PatSkol DataCon    -- An existential type variable bound by a pattern for
            SrcSpan     -- a data constructor with an existential type. E.g.
                        --      data T = forall a. Eq a => MkT a
@@ -486,8 +487,13 @@ pprSkolTvBinding tv
 pprSkolInfo :: SkolemInfo -> SDoc
 pprSkolInfo (SigSkol ctxt)   = ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt
 pprSkolInfo (ClsSkol cls)    = ptext SLIT("is bound by the class declaration for") <+> quotes (ppr cls)
-pprSkolInfo (InstSkol df)    = ptext SLIT("is bound by the instance declaration at") <+> ppr (getSrcLoc df)
-pprSkolInfo (ArrowSkol loc)  = ptext SLIT("is bound by the arrow form at") <+> ppr loc
+pprSkolInfo (InstSkol df)    = 
+  ptext SLIT("is bound by the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (FamInstSkol tc) = 
+  ptext SLIT("is bound by the family instance declaration at") <+> 
+  ppr (getSrcLoc tc)
+pprSkolInfo (ArrowSkol loc)  = 
+  ptext SLIT("is bound by the arrow form at") <+> ppr loc
 pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("is bound by the pattern for") <+> quotes (ppr dc),
                                    nest 2 (ptext SLIT("at") <+> ppr loc)]
 pprSkolInfo (GenSkol tvs ty loc) = sep [sep [ptext SLIT("is bound by the polymorphic type"), 
@@ -592,8 +598,9 @@ isTauTy other                 = False
 
 isTauTyCon :: TyCon -> Bool
 -- Returns False for type synonyms whose expansion is a polytype
-isTauTyCon tc | isSynTyCon tc = isTauTy (snd (synTyConDefn tc))
-             | otherwise     = True
+isTauTyCon tc 
+  | isSynTyCon tc && not (isOpenTyCon tc) = isTauTy (snd (synTyConDefn tc))
+  | otherwise                             = True
 
 ---------------
 isBoxyTy :: TcType -> Bool
@@ -645,20 +652,23 @@ tcSplitForAllTys ty = split ty ty []
      split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
      split orig_ty (ForAllTy tv ty) tvs 
        | not (isCoVar tv) = split ty ty (tv:tvs)
-     split orig_ty t               tvs = (reverse tvs, orig_ty)
+     split orig_ty t tvs = (reverse tvs, orig_ty)
 
 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
-tcIsForAllTy (ForAllTy tv ty) = True
+tcIsForAllTy (ForAllTy tv ty) = not (isCoVar tv)
 tcIsForAllTy t               = False
 
 tcSplitPhiTy :: Type -> (ThetaType, Type)
 tcSplitPhiTy ty = split ty ty []
  where
   split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
+
+  split orig_ty (ForAllTy tv ty) ts
+        | isCoVar tv = split ty ty (eq_pred:ts)
+        where
+           PredTy eq_pred = tyVarKind tv
   split orig_ty (FunTy arg res) ts 
        | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)
-  split orig_ty ty ts
-        | Just (p, ty') <- splitForAllCo_maybe ty = split ty' ty' (p:ts) 
   split orig_ty ty             ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
@@ -985,9 +995,14 @@ tcTyVarsOfType (NoteTy _ ty)           = tcTyVarsOfType ty
 tcTyVarsOfType (PredTy sty)        = tcTyVarsOfPred sty
 tcTyVarsOfType (FunTy arg res)     = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
 tcTyVarsOfType (AppTy fun arg)     = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
-tcTyVarsOfType (ForAllTy tyvar ty)  = tcTyVarsOfType ty `delVarSet` tyvar
+tcTyVarsOfType (ForAllTy tyvar ty)  = (tcTyVarsOfType ty `delVarSet` tyvar)
+                                      `unionVarSet` tcTyVarsOfTyVar tyvar
        -- We do sometimes quantify over skolem TcTyVars
 
+tcTyVarsOfTyVar :: TcTyVar -> TyVarSet
+tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv)
+                   | otherwise  = emptyVarSet
+
 tcTyVarsOfTypes :: [Type] -> TyVarSet
 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
 
@@ -1030,11 +1045,15 @@ exactTyVarsOfType ty
     go (FunTy arg res)           = go arg `unionVarSet` go res
     go (AppTy fun arg)           = go fun `unionVarSet` go arg
     go (ForAllTy tyvar ty)       = delVarSet (go ty) tyvar
+                                    `unionVarSet` go_tv tyvar
 
     go_pred (IParam _ ty)    = go ty
     go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
     go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
 
+    go_tv tyvar | isCoVar tyvar = go (tyVarKind tyvar)
+                | otherwise     = emptyVarSet
+
 exactTyVarsOfTypes :: [TcType] -> TyVarSet
 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
 \end{code}