Merge remote branch 'origin/master'
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
index ef4ad34..2c01d23 100644 (file)
@@ -18,6 +18,7 @@ module TcMType (
   newFlexiTyVarTy,             -- Kind -> TcM TcType
   newFlexiTyVarTys,            -- Int -> Kind -> TcM [TcType]
   newKindVar, newKindVars, 
+  mkTcTyVarName,
 
   newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
   isFilledMetaTyVar, isFlexiMetaTyVar,
@@ -25,7 +26,6 @@ module TcMType (
   --------------------------------
   -- Creating new evidence variables
   newEvVar, newCoVar, newEvVars,
-  newWantedCoVar, writeWantedCoVar, readWantedCoVar, 
   newIP, newDict, newSilentGiven, isSilentEvVar,
 
   newWantedEvVar, newWantedEvVars,
@@ -33,17 +33,17 @@ module TcMType (
 
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
-  tcInstType, tcInstSigType, instMetaTyVar,
-  tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, 
-  tcSkolSigType, tcSkolSigTyVars, 
+  tcInstTyVars, tcInstSigTyVars,
+  tcInstType, 
+  tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+  tcSkolDFunType, tcSuperSkolTyVars,
 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
   SourceTyCtxt(..), checkValidTheta, 
-  checkValidInstance,
-  checkValidTypeInst, checkTyFamFreeness,
+  checkValidInstHead, checkValidInstance, 
+  checkInstTermination, checkValidTypeInst, checkTyFamFreeness, 
   arityErr, 
   growPredTyVars, growThetaTyVars, validDerivPred,
 
@@ -55,10 +55,12 @@ module TcMType (
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkTcType, zonkTcTypes, zonkTcThetaType,
   zonkTcKindToKind, zonkTcKind, 
-  zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
+  zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
+  zonkWC, zonkWantedEvVars,
   zonkTcTypeAndSubst,
   tcGetGlobalTyVars, 
 
+
   readKindVar, writeKindVar
   ) where
 
@@ -68,7 +70,6 @@ module TcMType (
 import TypeRep
 import TcType
 import Type
-import Coercion
 import Class
 import TyCon
 import Var
@@ -89,10 +90,11 @@ import BasicTypes
 import SrcLoc
 import Outputable
 import FastString
+import Unique( Unique )
 import Bag
 
 import Control.Monad
-import Data.List       ( (\\) )
+import Data.List        ( (\\) )
 \end{code}
 
 
@@ -124,16 +126,13 @@ newEvVars :: TcThetaType -> TcM [EvVar]
 newEvVars theta = mapM newEvVar theta
 
 newWantedEvVar :: TcPredType -> TcM EvVar 
-newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
+newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
 newWantedEvVar (ClassP cls tys) = newDict cls tys
 newWantedEvVar (IParam ip ty)   = newIP ip ty
 
 newWantedEvVars :: TcThetaType -> TcM [EvVar] 
 newWantedEvVars theta = mapM newWantedEvVar theta 
 
-newWantedCoVar :: TcType -> TcType -> TcM CoVar 
-newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
-
 --------------
 newEvVar :: TcPredType -> TcM EvVar
 -- Creates new *rigid* variables for predicates
@@ -143,7 +142,7 @@ newEvVar (IParam ip ty)   = newIP    ip ty
 
 newCoVar :: TcType -> TcType -> TcM CoVar
 newCoVar ty1 ty2
-  = do { name <- newName (mkTyVarOccFS (fsLit "co"))
+  = do { name <- newName (mkVarOccFS (fsLit "co"))
        ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
 
 newIP :: IPName Name -> TcType -> TcM IpId
@@ -207,68 +206,66 @@ tcInstType inst_tyvars ty
 
                            ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
                                -- Either the tyvars are freshly made, by inst_tyvars,
-                               -- or (in the call from tcSkolSigType) any nested foralls
-                               -- have different binders.  Either way, zipTopTvSubst is ok
+                                -- or any nested foralls have different binders.
+                                -- Either way, zipTopTvSubst is ok
 
                            ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
                            ; return (tyvars', theta, tau) }
 
-mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
-mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
-
-tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type signature with skolem constants, but 
 -- do *not* give them fresh names, because we want the name to
 -- be in the type environment: it is lexically scoped.
-tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
 
-tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
 -- Make skolem constants, but do *not* give them new names, as above
-tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
-                             | tv <- tyvars ]
+-- Moreover, make them "super skolems"; see comments with superSkolemTv
+tcSuperSkolTyVars tyvars
+  = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
+    | tv <- tyvars ]
 
-tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
 -- Instantiate the tyvar, using 
 --     * the occ-name and kind of the supplied tyvar, 
 --     * the unique from the monad,
 --     * the location either from the tyvar (skol_info = SigSkol)
---                    or from the monad (otehrwise)
-tcInstSkolTyVar skol_info tyvar
+--                     or from the monad (otherwise)
+tcInstSkolTyVar overlappable tyvar
   = do { uniq <- newUnique
-       ; loc <- case skol_info of
-                    SigSkol {} -> return (getSrcSpan old_name)
-                    _          -> getSrcSpanM
+        ; loc <-  getSrcSpanM
        ; let new_name = mkInternalName uniq occ loc
-       ; return (mkSkolTyVar new_name kind skol_info) }
+        ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
   where
     old_name = tyVarName tyvar
     occ      = nameOccName old_name
     kind     = tyVarKind tyvar
 
-tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Get the location from the monad
-tcInstSkolTyVars info tyvars 
-  = mapM (tcInstSkolTyVar info) tyvars
+tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
 
-tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
+
+tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 -- Binding location comes from the monad
-tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
-
-tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
--- Instantiate with skolems or meta SigTvs; depending on use_skols
--- Always take location info from the supplied tyvars
-tcInstSigType use_skols name ty
-  | use_skols
-  = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
-  | otherwise
-  = tcInstType tcInstSigTyVars ty
+tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
 
 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
 -- Make meta SigTv type variables for patten-bound scoped type varaibles
 -- We use SigTvs for them, so that they can't unify with arbitrary types
-tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
-               -- ToDo: the "function binding site is bogus
+tcInstSigTyVars = mapM tcInstSigTyVar
+
+tcInstSigTyVar :: TyVar -> TcM TcTyVar
+tcInstSigTyVar tyvar
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
+        ; let name = setNameUnique (tyVarName tyvar) uniq
+               -- Use the same OccName so that the tidy-er 
+               -- doesn't rename 'a' to 'a0' etc
+             kind = tyVarKind tyvar
+       ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }
 \end{code}
 
 
@@ -284,33 +281,22 @@ newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
 newMetaTyVar meta_info kind
   = do { uniq <- newMetaUnique
        ; ref <- newMutVar Flexi
-       ; let name = mkSysTvName uniq fs 
-             fs = case meta_info of
-                       TauTv   -> fsLit "t"
-                       TcsTv   -> fsLit "u"
-                       SigTv _ -> fsLit "a"
+        ; let name = mkTcTyVarName uniq s
+              s = case meta_info of
+                        TauTv -> fsLit "t"
+                        TcsTv -> fsLit "u"
+                        SigTv -> fsLit "a"
        ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
 
-instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
--- Make a new meta tyvar whose Name and Kind 
--- come from an existing TyVar
-instMetaTyVar meta_info tyvar
-  = do { uniq <- newMetaUnique
-       ; ref <- newMutVar Flexi
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-             kind = tyVarKind tyvar
-       ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
+mkTcTyVarName :: Unique -> FastString -> Name
+-- Make sure that fresh TcTyVar names finish with a digit
+-- leaving the un-cluttered names free for user names
+mkTcTyVarName uniq str = mkSysTvName uniq str
 
 readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
                      readMutVar (metaTvRef tyvar)
 
-readWantedCoVar :: CoVar -> TcM MetaDetails
-readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
-                       readMutVar (metaTvRef covar)
-
-
-
 isFilledMetaTyVar :: TyVar -> TcM Bool
 -- True of a filled-in (Indirect) meta type variable
 isFilledMetaTyVar tv
@@ -349,9 +335,6 @@ writeMetaTyVar tyvar ty
   = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
     return ()
 
-writeWantedCoVar :: CoVar -> Coercion -> TcM () 
-writeWantedCoVar cv co = writeMetaTyVar cv co 
-
 --------------------
 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
 -- Here the tyvar is for error checking only; 
@@ -370,8 +353,8 @@ writeMetaTyVarRef tyvar ref ty
 
   | otherwise
   = do { meta_details <- readMutVar ref; 
-       ; WARN( not (isFlexi meta_details), 
-                hang (text "Double update of meta tyvar")
+       ; ASSERT2( isFlexi meta_details, 
+                  hang (text "Double update of meta tyvar")
                    2 (ppr tyvar $$ ppr meta_details) )
 
          traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
@@ -400,10 +383,6 @@ newFlexiTyVarTy kind = do
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
-tcInstTyVar :: TyVar -> TcM TcTyVar
--- Instantiate with a META type variable
-tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
-
 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 -- Instantiate with META type variables
 tcInstTyVars tyvars
@@ -413,6 +392,16 @@ tcInstTyVars tyvars
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
+
+tcInstTyVar :: TyVar -> TcM TcTyVar
+-- Make a new unification variable tyvar whose Name and Kind 
+-- come from an existing TyVar
+tcInstTyVar tyvar
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
+        ; let name = mkSystemName uniq (getOccName tyvar)
+             kind = tyVarKind tyvar
+       ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
 \end{code}
 
 
@@ -467,7 +456,6 @@ zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
 
 -----------------  Types
-
 zonkTcTypeCarefully :: TcType -> TcM TcType
 -- Do not zonk type variables free in the environment
 zonkTcTypeCarefully ty
@@ -480,10 +468,11 @@ zonkTcTypeCarefully ty
       | otherwise
       = ASSERT( isTcTyVar tv )
        case tcTyVarDetails tv of
-         SkolemTv {}  -> return (TyVarTy tv)
-         FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
-         MetaTv _ ref -> do { cts <- readMutVar ref
-                            ; case cts of    
+          SkolemTv {}   -> return (TyVarTy tv)
+          RuntimeUnk {} -> return (TyVarTy tv)
+          FlatSkol ty   -> zonkType (zonk_tv env_tvs) ty
+          MetaTv _ ref  -> do { cts <- readMutVar ref
+                              ; case cts of
                                   Flexi       -> return (TyVarTy tv)
                                   Indirect ty -> zonkType (zonk_tv env_tvs) ty }
 
@@ -496,10 +485,11 @@ zonkTcTyVar :: TcTyVar -> TcM TcType
 zonkTcTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-      SkolemTv {}  -> return (TyVarTy tv)
-      FlatSkol ty  -> zonkTcType ty
-      MetaTv _ ref -> do { cts <- readMutVar ref
-                        ; case cts of    
+      SkolemTv {}   -> return (TyVarTy tv)
+      RuntimeUnk {} -> return (TyVarTy tv)
+      FlatSkol ty   -> zonkTcType ty
+      MetaTv _ ref  -> do { cts <- readMutVar ref
+                          ; case cts of
                               Flexi       -> return (TyVarTy tv)
                               Indirect ty -> zonkTcType ty }
 
@@ -509,10 +499,11 @@ zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
   where
     zonk_tv tv 
       = case tcTyVarDetails tv of
-         SkolemTv {}    -> return (TyVarTy tv)
-         FlatSkol ty    -> zonkType zonk_tv ty
-         MetaTv _ ref   -> do { cts <- readMutVar ref
-                              ; case cts of    
+          SkolemTv {}   -> return (TyVarTy tv)
+          RuntimeUnk {} -> return (TyVarTy tv)
+          FlatSkol ty   -> zonkType zonk_tv ty
+          MetaTv _ ref  -> do { cts <- readMutVar ref
+                              ; case cts of
                                   Flexi       -> zonk_flexi tv
                                   Indirect ty -> zonkType zonk_tv ty }
     zonk_flexi tv
@@ -552,8 +543,8 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 zonkQuantifiedTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv ) 
     case tcTyVarDetails tv of
-      FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
-      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+      SkolemTv {} -> WARN( True, ppr tv )  -- Dec10: Can this really happen?
+                     do { kind <- zonkTcType (tyVarKind tv)
                         ; return $ setTyVarKind tv kind }
        -- It might be a skolem type variable, 
        -- for example from a user type signature
@@ -565,23 +556,26 @@ zonkQuantifiedTyVar tv
                       (readMutVar _ref >>= \cts -> 
                        case cts of 
                              Flexi -> return ()
-                             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
+                             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                                             return ()) >>
 #endif
-                      skolemiseUnboundMetaTyVar UnkSkol tv 
-                             
-skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
+                      skolemiseUnboundMetaTyVar tv vanillaSkolemTv
+      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
+
+skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
 -- Skolemise it, including giving it a new Name, so that
 --   we are totally out of Meta-tyvar-land
 -- We create a skolem TyVar, not a regular TyVar
 --   See Note [Zonking to Skolem]
-skolemiseUnboundMetaTyVar skol_info tv
+skolemiseUnboundMetaTyVar tv details
   = ASSERT2( isMetaTyVar tv, ppr tv ) 
-    do { uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
+    do  { span <- getSrcSpanM    -- Get the location from "here"
+                                 -- ie where we are generalising
+        ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
        ; let final_kind = defaultKind (tyVarKind tv)
-              final_name = setNameUnique (tyVarName tv) uniq
-             final_tv   = mkSkolTyVar final_name final_kind skol_info
+              final_name = mkInternalName uniq (getOccName tv) span
+              final_tv   = mkTcTyVar final_name final_kind details
        ; writeMetaTyVar tv (mkTyVarTy final_tv)
        ; return final_tv }
 \end{code}
@@ -589,24 +583,59 @@ skolemiseUnboundMetaTyVar skol_info tv
 \begin{code}
 zonkImplication :: Implication -> TcM Implication
 zonkImplication implic@(Implic { ic_given = given 
-                               , ic_wanted = wanted })
-  = do { given'   <- mapM zonkEvVar given
-       ; wanted'  <- mapBagM zonkWanted wanted
-       ; return (implic { ic_given = given', ic_wanted = wanted' }) }
+                               , ic_wanted = wanted
+                               , ic_loc = loc })
+  = do {    -- No need to zonk the skolems
+       ; given'  <- mapM zonkEvVar given
+       ; loc'    <- zonkGivenLoc loc
+       ; wanted' <- zonkWC wanted
+       ; return (implic { ic_given = given'
+                        , ic_wanted = wanted'
+                        , ic_loc = loc' }) }
 
 zonkEvVar :: EvVar -> TcM EvVar
 zonkEvVar var = do { ty' <- zonkTcType (varType var)
                    ; return (setVarType var ty') }
 
-zonkWanted :: WantedConstraint -> TcM WantedConstraint
-zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
-zonkWanted (WcEvVar ev)   = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
+zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
+zonkFlavoredEvVar (EvVarX ev fl)
+  = do { ev' <- zonkEvVar ev
+       ; fl' <- zonkFlavor fl
+       ; return (EvVarX ev' fl') }
+
+zonkWC :: WantedConstraints -> TcM WantedConstraints
+zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+  = do { flat'   <- zonkWantedEvVars flat
+       ; implic' <- mapBagM zonkImplication implic
+       ; insol'  <- mapBagM zonkFlavoredEvVar insol
+       ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
+
+zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
+zonkWantedEvVars = mapBagM zonkWantedEvVar
 
 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
-zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
+zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
+
+zonkFlavor :: CtFlavor -> TcM CtFlavor
+zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
+zonkFlavor fl             = return fl
+
+zonkGivenLoc :: GivenLoc -> TcM GivenLoc
+-- GivenLocs may have unification variables inside them!
+zonkGivenLoc (CtLoc skol_info span ctxt)
+  = do { skol_info' <- zonkSkolemInfo skol_info
+       ; return (CtLoc skol_info' span ctxt) }
+
+zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
+zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
+                                     ; return (SigSkol cx ty') }
+zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
+                                     ; return (InferSkol ntys') }
+  where
+    do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
+zonkSkolemInfo skol_info = return skol_info
 \end{code}
 
-
 Note [Silly Type Synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
@@ -711,13 +740,12 @@ zonkType zonk_tc_tyvar ty
 
        -- The two interesting cases!
     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
-                      | otherwise       = liftM TyVarTy $ 
-                                           zonkTyVar zonk_tc_tyvar tyvar
+                      | otherwise       = return (TyVarTy tyvar)
                -- Ordinary (non Tc) tyvars occur inside quantified types
 
     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
                              ty' <- go ty
-                             tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
+                             tyvar' <- return tyvar
                              return (ForAllTy tyvar' ty')
 
     go_pred (ClassP c tys)   = do tys' <- mapM go tys
@@ -734,21 +762,12 @@ mkZonkTcTyVar unbound_var_fn tyvar
   = ASSERT( isTcTyVar tyvar )
     case tcTyVarDetails tyvar of
       SkolemTv {}    -> return (TyVarTy tyvar)
+      RuntimeUnk {}  -> return (TyVarTy tyvar)
       FlatSkol ty    -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
       MetaTv _ ref   -> do { cts <- readMutVar ref
                           ; case cts of    
                               Flexi       -> unbound_var_fn tyvar  
                               Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
-
--- Zonk the kind of a non-TC tyvar in case it is a coercion variable 
--- (their kind contains types).
-zonkTyVar :: (TcTyVar -> TcM Type)      -- What to do for a TcTyVar
-         -> TyVar -> TcM TyVar
-zonkTyVar zonk_tc_tyvar tv 
-  | isCoVar tv
-  = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
-       ; return $ setTyVarKind tv kind }
-  | otherwise = return tv
 \end{code}
 
 
@@ -844,7 +863,9 @@ checkValidType ctxt ty = do
 
                 ForSigCtxt _   -> gen_rank 1
                 SpecInstCtxt   -> gen_rank 1
-                ThBrackCtxt    -> gen_rank 1
+                 ThBrackCtxt    -> gen_rank 1
+                 GenSigCtxt     -> panic "checkValidType"
+                                     -- Can't happen; GenSigCtxt not used for *user* sigs
 
        actual_kind = typeKind ty
 
@@ -1117,7 +1138,7 @@ check_valid_theta ctxt theta = do
     warnTc (notNull dups) (dupPredWarn dups)
     mapM_ (check_pred_ty dflags ctxt) theta
   where
-    (_,dups) = removeDups tcCmpPred theta
+    (_,dups) = removeDups cmpPred theta
 
 -------------------------
 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
@@ -1239,7 +1260,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars
 
 ambigErr :: PredType -> SDoc
 ambigErr pred
-  = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
+  = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred),
         nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
                 ptext (sLit "must be reachable from the type after the '=>'"))]
 \end{code}
@@ -1306,14 +1327,14 @@ eqSuperClassErr pred
        2 (ppr pred)
 
 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
-badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
-eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
+badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
+eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
                    $$
                    parens (ptext (sLit "Use -XTypeFamilies to permit this"))
 predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
-                         nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+                         nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
 dupPredWarn :: [[PredType]] -> SDoc
-dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups)
 
 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
 arityErr kind name n m
@@ -1461,7 +1482,7 @@ checkInstTermination tys theta
 
 predUndecErr :: PredType -> SDoc -> SDoc
 predUndecErr pred msg = sep [msg,
-                       nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+                       nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
 
 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")