fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
index 02eba6d..6423a83 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,18 +26,17 @@ module TcMType (
   --------------------------------
   -- Creating new evidence variables
   newEvVar, newCoVar, newEvVars,
-  newWantedCoVar, writeWantedCoVar, readWantedCoVar, 
-  newIP, newDict, newSelfDict, isSelfDict,
+  newIP, newDict, newSilentGiven, isSilentEvVar,
 
   newWantedEvVar, newWantedEvVars,
   newTcEvBinds, addTcEvBind,
 
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
-  tcInstType, tcInstSigType, instMetaTyVar,
-  tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, 
-  tcSkolSigType, tcSkolSigTyVars, 
+  tcInstTyVars, tcInstSigTyVars,
+  tcInstType, 
+  tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+  tcSkolDFunType, tcSuperSkolTyVars,
 
   --------------------------------
   -- Checking type validity
@@ -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
@@ -163,20 +162,23 @@ newName occ
        ; return (mkInternalName uniq occ loc) }
 
 -----------------
-newSelfDict :: Class -> [TcType] -> TcM DictId
--- Make a dictionary for "self". It behaves just like a normal DictId
--- except that it responds True to isSelfDict
+newSilentGiven :: PredType -> TcM EvVar
+-- Make a dictionary for a "silent" given dictionary
+-- Behaves just like any EvVar except that it responds True to isSilentDict
 -- This is used only to suppress confusing error reports
-newSelfDict cls tys 
+newSilentGiven (ClassP cls tys)
   = do { uniq <- newUnique
-       ; let name = mkSystemName uniq selfDictOcc
+       ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
        ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+newSilentGiven (EqPred ty1 ty2)
+  = do { uniq <- newUnique
+       ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
+       ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+newSilentGiven pred@(IParam {})
+  = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
 
-selfDictOcc :: OccName
-selfDictOcc = mkVarOcc "self"
-
-isSelfDict :: EvVar -> Bool
-isSelfDict v = isSystemName (Var.varName v)
+isSilentEvVar :: EvVar -> Bool
+isSilentEvVar v = isSystemName (Var.varName v)
   -- Notice that all *other* evidence variables get Internal Names
 \end{code}
 
@@ -204,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}
 
 
@@ -281,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
@@ -346,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; 
@@ -367,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)
@@ -397,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
@@ -410,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}
 
 
@@ -464,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
@@ -477,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 }
 
@@ -493,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 }
 
@@ -506,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
@@ -549,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
@@ -562,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}
@@ -586,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:
@@ -708,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
@@ -731,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}
 
 
@@ -841,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
 
@@ -1114,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 ()
@@ -1138,7 +1162,8 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
   = do {       -- Equational constraints are valid in all contexts if type
                -- families are permitted
-       ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+       ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) 
+                 (eqPredTyErr pred)
        ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
                  (eqSuperClassErr pred)
 
@@ -1236,7 +1261,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}
@@ -1303,14 +1328,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"))
+                   parens (ptext (sLit "Use -XGADTs or -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
@@ -1339,34 +1364,20 @@ compiled elsewhere). In these cases, we let them go through anyway.
 We can also have instances for functions: @instance Foo (a -> b) ...@.
 
 \begin{code}
-checkValidInstHead :: Type -> TcM (Class, [TcType])
-
-checkValidInstHead ty  -- Should be a source type
-  = case tcSplitPredTy_maybe ty of {
-       Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
-       Just pred -> 
-
-    case getClassPredTys_maybe pred of {
-       Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
-        Just (clas,tys) -> do
+checkValidInstHead :: Class -> [Type] -> TcM ()
+checkValidInstHead clas tys
+  = do { dflags <- getDOpts
 
-    dflags <- getDOpts
-    check_inst_head dflags clas tys
-    return (clas, tys)
-    }}
-
-check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
-check_inst_head dflags clas tys
-  = do { -- If GlasgowExts then check at least one isn't a type variable
+           -- If GlasgowExts then check at least one isn't a type variable
        ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
                   all tcInstHeadTyNotSynonym tys)
-                 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+                 (instTypeErr pp_pred head_type_synonym_msg)
        ; checkTc (xopt Opt_FlexibleInstances dflags ||
                   all tcInstHeadTyAppAllTyVars tys)
-                 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+                 (instTypeErr pp_pred head_type_args_tyvars_msg)
        ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
                   isSingleton tys)
-                 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+                 (instTypeErr pp_pred head_one_type_msg)
          -- May not contain type family applications
        ; mapM_ checkTyFamFreeness tys
 
@@ -1379,6 +1390,7 @@ check_inst_head dflags clas tys
        }
 
   where
+    pp_pred = pprClassPred clas tys
     head_type_synonym_msg = parens (
                 text "All instance types must be of the form (T t1 ... tn)" $$
                 text "where T is not a synonym." $$
@@ -1386,7 +1398,7 @@ check_inst_head dflags clas tys
 
     head_type_args_tyvars_msg = parens (vcat [
                 text "All instance types must be of the form (T a1 ... an)",
-                text "where a1 ... an are type *variables*,",
+                text "where a1 ... an are *distinct type variables*,",
                 text "and each type variable appears at most once in the instance head.",
                 text "Use -XFlexibleInstances if you want to disable this."])
 
@@ -1408,35 +1420,30 @@ instTypeErr pp_ty msg
 %************************************************************************
 
 \begin{code}
-checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type 
-                   -> TcM (Class, [TcType])
-checkValidInstance hs_type tyvars theta tau
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
+                   -> Class -> [TcType] -> TcM ()
+checkValidInstance hs_type tyvars theta clas inst_tys
   = setSrcSpan (getLoc hs_type) $
-    do { (clas, inst_tys) <- setSrcSpan head_loc $
-                              checkValidInstHead tau
-
-        ; undecidable_ok <- xoptM Opt_UndecidableInstances
-
-       ; checkValidTheta InstThetaCtxt theta
+    do  { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
+        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
        -- For Haskell 98 this will already have been done by checkValidTheta,
         -- but as we may be using other extensions we need to check.
-       ; unless undecidable_ok $
+       ; undecidable_ok <- xoptM Opt_UndecidableInstances
+        ; unless undecidable_ok $
          mapM_ addErrTc (checkInstTermination inst_tys theta)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
-
-        ; return (clas, inst_tys)
-       }
+        }
   where
     msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
                         undecidableMsg])
 
-       -- The location of the "head" of the instance
+        -- The location of the "head" of the instance
     head_loc = case hs_type of
                  L _ (HsForAllTy _ _ _ (L loc _)) -> loc
                  L loc _                          -> loc
@@ -1476,7 +1483,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")