Fix desugaring of unboxed tuples
[ghc-hetmet.git] / ghc / compiler / typecheck / TcHsType.lhs
index 21b9b48..968ccfb 100644 (file)
@@ -14,55 +14,51 @@ module TcHsType (
        
                -- Typechecking kinded types
        tcHsKindedContext, tcHsKindedType, tcHsBangType,
-       tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig,
+       tcTyVarBndrs, dsHsType, tcLHsConResTy,
+       tcDataKindSig,
 
-       tcHsPatSigType, tcAddLetBoundTyVars,
-       
-       TcSigInfo(..), mkTcSig, 
-       TcSigFun, lookupSig 
+               -- Pattern type signatures
+       tcHsPatSigType, tcPatSig
    ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
-                         LHsContext, HsPred(..), LHsPred, LHsBinds,
-                         getBangStrictness, collectSigTysFromHsBinds )
+import HsSyn           ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, 
+                         LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) )
 import RnHsSyn         ( extractHsTyVars )
 import TcRnMonad
-import TcEnv           ( tcExtendTyVarEnv, tcExtendKindEnv,
+import TcEnv           ( tcExtendTyVarEnv, tcExtendKindEnvTvs, 
                          tcLookup, tcLookupClass, tcLookupTyCon,
-                         TyThing(..), getInLocalScope, wrongThingErr
+                         TyThing(..), getInLocalScope, getScopedTyVarBinds,
+                         wrongThingErr
                        )
-import TcMType         ( newKindVar, tcSkolType, newMetaTyVar, 
+import TcMType         ( newKindVar, 
                          zonkTcKindToKind, 
-                         checkValidType, UserTypeCtxt(..), pprHsSigCtxt
+                         tcInstBoxyTyVar, readFilledBox,
+                         checkValidType
                        )
-import TcUnify         ( unifyFunKind, checkExpectedKind )
-import TcType          ( Type, PredType(..), ThetaType, 
-                         SkolemInfo(SigSkol), MetaDetails(Flexi),
-                         TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
-                         mkTyVarTy, mkFunTy, 
-                         mkForAllTys, mkFunTys, tcEqType, isPredTy,
-                         mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
-                         tcSplitFunTy_maybe, tcSplitForAllTys )
+import TcUnify         ( boxyUnify, unifyFunKind, checkExpectedKind )
+import TcIface         ( checkWiredInTyCon )
+import TcType          ( Type, PredType(..), ThetaType, BoxySigmaType,
+                         TcType, TcKind, isRigidTy,
+                         UserTypeCtxt(..), pprUserTypeCtxt,
+                         substTyWith, mkTyVarTys, tcEqType,
+                         tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy, 
+                         mkTyConApp, mkAppTys, typeKind )
 import Kind            ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
                          openTypeKind, argTypeKind, splitKindFunTys )
-import Id              ( idName, idType )
-import Var             ( TyVar, mkTyVar, tyVarKind )
+import Var             ( TyVar, mkTyVar, tyVarName )
 import TyCon           ( TyCon, tyConKind )
 import Class           ( Class, classTyCon )
 import Name            ( Name, mkInternalName )
 import OccName         ( mkOccName, tvName )
 import NameSet
 import PrelNames       ( genUnitTyConName )
-import Type            ( deShadowTy )
-import TysWiredIn      ( mkListTy, mkPArrTy, mkTupleTy )
-import Bag             ( bagToList )
+import TysWiredIn      ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
 import BasicTypes      ( Boxity(..) )
-import SrcLoc          ( Located(..), unLoc, noLoc, srcSpanStart )
+import SrcLoc          ( Located(..), unLoc, noLoc, getLoc, srcSpanStart )
 import UniqSupply      ( uniqsFromSupply )
 import Outputable
-import List            ( nubBy )
 \end{code}
 
 
@@ -151,12 +147,16 @@ the TyCon being defined.
 \begin{code}
 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
   -- Do kind checking, and hoist for-alls to the top
+  -- NB: it's important that the foralls that come from the top-level
+  --    HsForAllTy in hs_ty occur *first* in the returned type.
+  --     See Note [Scoped] with TcSigInfo
 tcHsSigType ctxt hs_ty 
   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
     do { kinded_ty <- kcTypeType hs_ty
        ; ty <- tcHsKindedType kinded_ty
        ; checkValidType ctxt ty        
        ; returnM ty }
+
 -- Used for the deriving(...) items
 tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
 tcHsDeriv = addLocM (tc_hs_deriv [])
@@ -196,9 +196,7 @@ tcHsKindedType :: LHsType Name -> TcM Type
   -- This is used in type and class decls, where kinding is
   -- done in advance, and validity checking is done later
   -- [Validity checking done later because of knot-tying issues.]
-tcHsKindedType hs_ty 
-  = do { ty <- dsHsType hs_ty
-       ; return (hoistForAllTys ty) }
+tcHsKindedType hs_ty = dsHsType hs_ty
 
 tcHsBangType :: LHsType Name -> TcM Type
 -- Permit a bang, but discard it
@@ -239,9 +237,20 @@ kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
 -- with OpenTypeKind, because it gives better error messages
 kcCheckHsType (L span ty) exp_kind 
   = setSrcSpan span                            $
-    kc_hs_type ty                              `thenM` \ (ty', act_kind) ->
-    checkExpectedKind ty act_kind exp_kind     `thenM_`
-    returnM (L span ty')
+    do { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
+               -- Add the context round the inner check only
+               -- because checkExpectedKind already mentions
+               -- 'ty' by name in any error message
+
+       ; checkExpectedKind ty act_kind exp_kind
+       ; return (L span ty') }
+  where
+       -- Wrap a context around only if we want to
+       -- show that contexts.  Omit invisble ones
+       -- and ones user's won't grok (HsPred p).
+    add_ctxt (HsPredTy p)                         thing = thing
+    add_ctxt (HsForAllTy Implicit tvs (L _ []) ty) thing = thing
+    add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing
 \end{code}
 
        Here comes the main function
@@ -392,7 +401,7 @@ kcTyVar name        -- Could be a tyvar or a tycon
     tcLookup name      `thenM` \ thing ->
     traceTc (text "lk2" <+> ppr name <+> ppr thing)    `thenM_`
     case thing of 
-       ATyVar tv               -> returnM (tyVarKind tv)
+       ATyVar _ ty             -> returnM (typeKind ty)
        AThing kind             -> returnM kind
        AGlobal (ATyCon tc)     -> returnM (tyConKind tc) 
        other                   -> wrongThingErr "type" thing name
@@ -419,7 +428,9 @@ The type desugarer
        * Zonks any kinds
 
 It cannot fail, and does no validity checking, except for 
-structural matters, such as spurious ! annotations.
+structural matters, such as
+       (a) spurious ! annotations.
+       (b) a class used as a type
 
 \begin{code}
 dsHsType :: LHsType Name -> TcM Type
@@ -439,16 +450,21 @@ ds_type (HsKindSig ty k)
   = dsHsType ty        -- Kind checking done already
 
 ds_type (HsListTy ty)
-  = dsHsType ty                                `thenM` \ tau_ty ->
+  = dsHsType ty                        `thenM` \ tau_ty ->
+    checkWiredInTyCon listTyCon        `thenM_`
     returnM (mkListTy tau_ty)
 
 ds_type (HsPArrTy ty)
-  = dsHsType ty                                `thenM` \ tau_ty ->
+  = dsHsType ty                        `thenM` \ tau_ty ->
+    checkWiredInTyCon parrTyCon        `thenM_`
     returnM (mkPArrTy tau_ty)
 
 ds_type (HsTupleTy boxity tys)
-  = dsHsTypes tys                      `thenM` \ tau_tys ->
-    returnM (mkTupleTy boxity (length tys) tau_tys)
+  = dsHsTypes tys              `thenM` \ tau_tys ->
+    checkWiredInTyCon tycon    `thenM_`
+    returnM (mkTyConApp tycon tau_tys)
+  where
+    tycon = tupleTyCon boxity (length tys)
 
 ds_type (HsFunTy ty1 ty2)
   = dsHsType ty1                       `thenM` \ tau_ty1 ->
@@ -500,11 +516,9 @@ ds_var_app :: Name -> [Type] -> TcM Type
 ds_var_app name arg_tys 
  = tcLookup name                       `thenM` \ thing ->
     case thing of
-       ATyVar tv            -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
-       AGlobal (ATyCon tc)  -> returnM (mkGenTyConApp tc arg_tys)
---     AThing _             -> tcLookupTyCon name      `thenM` \ tc ->
---                             returnM (mkGenTyConApp tc arg_tys)
-       other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
+       ATyVar _ ty         -> returnM (mkAppTys ty arg_tys)
+       AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
+       other               -> wrongThingErr "type" thing name
 \end{code}
 
 
@@ -528,36 +542,12 @@ dsHsPred (HsIParam name ty)
 GADT constructor signatures
 
 \begin{code}
-tcLHsConSig :: LHsType Name 
-           -> TcM ([TcTyVar], TcThetaType, 
-                   [HsBang], [TcType],
-                   TyCon, [TcType])
--- Take apart the type signature for a data constructor
--- The difference is that there can be bangs at the top of
--- the argument types, and kind-checking is the right place to check
-tcLHsConSig sig@(L span (HsForAllTy exp tv_names ctxt ty))
-  = setSrcSpan span            $
-    addErrCtxt (gadtSigCtxt sig) $
-    tcTyVarBndrs tv_names      $ \ tyvars ->
-    do { theta <- mappM dsHsLPred (unLoc ctxt)
-       ; (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
-       ; return (tyvars, theta, bangs, arg_tys, tc, res_tys) }
-tcLHsConSig ty 
-  = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
-       ; return ([], [], bangs, arg_tys, tc, res_tys) }
-
---------
-tc_con_sig_tau (L _ (HsFunTy arg ty))
-  = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
-       ; arg_ty <- tcHsBangType arg
-       ; return (getBangStrictness arg : bangs, 
-                 arg_ty : arg_tys, tc, res_tys) }
-
-tc_con_sig_tau ty
-  = do { (tc, res_tys) <- tc_con_res ty []
-       ; return ([], [], tc, res_tys) }
-
---------
+tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
+tcLHsConResTy ty@(L span _) 
+  = setSrcSpan span $ 
+    addErrCtxt (gadtResCtxt ty) $
+    tc_con_res ty []
+
 tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
   = do { res_ty' <- dsHsType res_ty
        ; tc_con_res fun (res_ty' : res_tys) }
@@ -571,12 +561,14 @@ tc_con_res ty@(L _ (HsTyVar name)) res_tys
 
 tc_con_res ty _ = failWithTc (badGadtDecl ty)
 
-gadtSigCtxt ty
-  = hang (ptext SLIT("In the signature of a data constructor:"))
+gadtResCtxt ty
+  = hang (ptext SLIT("In the result type of a data constructor:"))
        2 (ppr ty)
 badGadtDecl ty
-  = hang (ptext SLIT("Malformed constructor signature:"))
+  = hang (ptext SLIT("Malformed constructor result type:"))
        2 (ppr ty)
+
+typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 \end{code}
 
 %************************************************************************
@@ -593,8 +585,7 @@ kcHsTyVars :: [LHsTyVarBndr Name]
           -> TcM r
 kcHsTyVars tvs thing_inside 
   = mappM (wrapLocM kcHsTyVar) tvs     `thenM` \ bndrs ->
-    tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs]
-                   (thing_inside bndrs)
+    tcExtendKindEnvTvs bndrs (thing_inside bndrs)
 
 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
        -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
@@ -612,10 +603,10 @@ tcTyVarBndrs bndrs thing_inside
   = mapM (zonk . unLoc) bndrs  `thenM` \ tyvars ->
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
   where
-    zonk (KindedTyVar name kind) = zonkTcKindToKind kind       `thenM` \ kind' ->
-                                  returnM (mkTyVar name kind')
+    zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
+                                     ; return (mkTyVar name kind') }
     zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
-                           returnM (mkTyVar name liftedTypeKind)
+                           return (mkTyVar name liftedTypeKind)
 
 -----------------------------------
 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
@@ -689,186 +680,137 @@ Historical note:
           it with expected_ty afterwards
 
 \begin{code}
-tcPatSigBndrs :: LHsType Name
-             -> TcM ([TcTyVar],        -- Brought into scope
-                     LHsType Name)     -- Kinded, but not yet desugared
+tcHsPatSigType :: UserTypeCtxt
+              -> LHsType Name          -- The type signature
+              -> TcM ([TyVar],         -- Newly in-scope type variables
+                       Type)           -- The signature
+-- Used for type-checking type signatures in
+-- (a) patterns          e.g  f (x::Int) = e
+-- (b) result signatures  e.g. g x :: Int = e
+-- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
 
-tcPatSigBndrs hs_ty
-  = do { in_scope <- getInLocalScope
-       ; span <- getSrcSpanM
-       ; let sig_tvs = [ L span (UserTyVar n) 
+tcHsPatSigType ctxt hs_ty 
+  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
+    do {       -- Find the type variables that are mentioned in the type
+               -- but not already in scope.  These are the ones that
+               -- should be bound by the pattern signature
+         in_scope <- getInLocalScope
+       ; let span = getLoc hs_ty
+             sig_tvs = [ L span (UserTyVar n) 
                        | n <- nameSetToList (extractHsTyVars hs_ty),
                          not (in_scope n) ]
-               -- The tyvars we want are the free type variables of 
-               -- the type that are not already in scope
 
-       -- Behave like kcHsType on a ForAll type
-       -- i.e. make kinded tyvars with mutable kinds, 
-       --      and kind-check the enclosed types
+       -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
+       -- except that we want to keep the tvs separate
        ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
                                    { kinded_ty <- kcTypeType hs_ty
                                    ; return (kinded_tvs, kinded_ty) }
-
-       -- Zonk the mutable kinds and bring the tyvars into scope
-       -- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case), 
-       -- except that it brings *meta* tyvars into scope, not regular ones
-       --
-       --      [Out of date, but perhaps should be resurrected]
-       -- Furthermore, the tyvars are PatSigTvs, which means that we get better
-       -- error messages when type variables escape:
-       --      Inferred type is less polymorphic than expected
-       --      Quantified type variable `t' escapes
-       --      It is mentioned in the environment:
-       --      t is bound by the pattern type signature at tcfail103.hs:6
-       ; tyvars <- mapM (zonk . unLoc) kinded_tvs
-       ; return (tyvars, kinded_ty) }
-  where
-    zonk (KindedTyVar name kind) = zonkTcKindToKind kind       `thenM` \ kind' ->
-                                  newMetaTyVar name kind' Flexi
-       -- Scoped type variables are bound to a *type*, hence Flexi
-    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
-                           returnM (mkTyVar name liftedTypeKind)
-
-tcHsPatSigType :: UserTypeCtxt
-              -> LHsType Name          -- The type signature
-              -> TcM ([TcTyVar],       -- Newly in-scope type variables
-                       TcType)         -- The signature
-
-tcHsPatSigType ctxt hs_ty 
-  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
-    do { (tyvars, kinded_ty) <- tcPatSigBndrs hs_ty
-
-        -- Complete processing of the type, and check its validity
-       ; tcExtendTyVarEnv tyvars $ do
-               { sig_ty <- tcHsKindedType kinded_ty    
-               ; checkValidType ctxt sig_ty 
-               ; return (tyvars, sig_ty) }
-       }
-
-tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
--- Turgid funciton, used for type variables bound by the patterns of a let binding
-
-tcAddLetBoundTyVars binds thing_inside
-  = go (collectSigTysFromHsBinds (bagToList binds)) thing_inside
+       ; tcTyVarBndrs kinded_tvs $ \ tyvars -> do
+       { sig_ty <- dsHsType kinded_ty
+       ; checkValidType ctxt sig_ty 
+       ; return (tyvars, sig_ty)
+      } }
+
+tcPatSig :: UserTypeCtxt
+        -> LHsType Name
+        -> BoxySigmaType
+        -> TcM (TcType,           -- The type to use for "inside" the signature
+                [(Name,TcType)])  -- The new bit of type environment, binding
+                                  -- the scoped type variables
+tcPatSig ctxt sig res_ty
+  = do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
+
+       ; if null sig_tvs then do {
+               -- The type signature binds no type variables, 
+               -- and hence is rigid, so use it to zap the res_ty
+                 boxyUnify sig_ty res_ty
+               ; return (sig_ty, [])
+
+       } else do {
+               -- Type signature binds at least one scoped type variable
+       
+               -- A pattern binding cannot bind scoped type variables
+               -- The renamer fails with a name-out-of-scope error 
+               -- if a pattern binding tries to bind a type variable,
+               -- So we just have an ASSERT here
+       ; let in_pat_bind = case ctxt of
+                               BindPatSigCtxt -> True
+                               other          -> False
+       ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
+
+               -- Check that pat_ty is rigid
+       ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
+
+               -- Now match the pattern signature against res_ty
+               -- For convenience, and uniform-looking error messages
+               -- we do the matching by allocating meta type variables, 
+               -- unifying, and reading out the results.
+               -- This is a strictly local operation.
+       ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
+       ; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
+       ; sig_tv_tys <- mapM readFilledBox box_tvs
+
+               -- Check that each is bound to a distinct type variable,
+               -- and one that is not already in scope
+       ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
+       ; binds_in_scope <- getScopedTyVarBinds
+       ; check binds_in_scope tv_binds
+       
+               -- Phew!
+       ; return (res_ty, tv_binds)
+       } }
   where
-    go [] thing_inside = thing_inside
-    go (hs_ty:hs_tys) thing_inside
-       = do { (tyvars, _kinded_ty) <- tcPatSigBndrs hs_ty
-            ; tcExtendTyVarEnv tyvars (go hs_tys thing_inside) }
-\end{code}
+    check in_scope []           = return ()
+    check in_scope ((n,ty):rest) = do { check_one in_scope n ty
+                                     ; check ((n,ty):in_scope) rest }
 
+    check_one in_scope n ty
+       = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
+               -- Must bind to a type variable
 
-%************************************************************************
-%*                                                                     *
-\subsection{Signatures}
-%*                                                                     *
-%************************************************************************
-
-@tcSigs@ checks the signatures for validity, and returns a list of
-{\em freshly-instantiated} signatures.  That is, the types are already
-split up, and have fresh type variables installed.  All non-type-signature
-"RenamedSigs" are ignored.
-
-The @TcSigInfo@ contains @TcTypes@ because they are unified with
-the variable's type, and after that checked to see whether they've
-been instantiated.
+            ; checkTc (null dups) (dupInScope n (head dups) ty)
+               -- Must not bind to the same type variable
+               -- as some other in-scope type variable
 
-\begin{code}
-data TcSigInfo
-  = TcSigInfo {
-       sig_id :: TcId,             -- *Polymorphic* binder for this value...
-       sig_tvs   :: [TcTyVar],     -- tyvars
-       sig_theta :: TcThetaType,   -- theta
-       sig_tau   :: TcTauType,     -- tau
-       sig_loc :: InstLoc          -- The location of the signature
-    }
-
-type TcSigFun = Name -> Maybe TcSigInfo
-
-instance Outputable TcSigInfo where
-    ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
-       = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
-
-lookupSig :: [TcSigInfo] -> TcSigFun   -- Search for a particular signature
-lookupSig [] name = Nothing
-lookupSig (sig : sigs) name
-  | name == idName (sig_id sig) = Just sig
-  | otherwise                  = lookupSig sigs name
-
-mkTcSig :: TcId -> TcM TcSigInfo
-mkTcSig poly_id
-  =    -- Instantiate this type
-       -- It's important to do this even though in the error-free case
-       -- we could just split the sigma_tc_ty (since the tyvars don't
-       -- unified with anything).  But in the case of an error, when
-       -- the tyvars *do* get unified with something, we want to carry on
-       -- typechecking the rest of the program with the function bound
-       -- to a pristine type, namely sigma_tc_ty
-    do { let rigid_info = SigSkol (idName poly_id)
-       ; (tyvars', theta', tau') <- tcSkolType rigid_info (idType poly_id)
-       ; loc <- getInstLoc (SigOrigin rigid_info)
-       ; return (TcSigInfo { sig_id = poly_id, sig_tvs = tyvars', 
-                             sig_theta = theta', sig_tau = tau', sig_loc = loc }) }
+            ; return () }
+       where
+         dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Errors and contexts}
+               Scoped type variables
 %*                                                                     *
 %************************************************************************
 
-
 \begin{code}
-hoistForAllTys :: Type -> Type
--- Used for user-written type signatures only
--- Move all the foralls and constraints to the top
--- e.g.  T -> forall a. a        ==>   forall a. T -> a
---      T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
---
--- Also: eliminate duplicate constraints.  These can show up
--- when hoisting constraints, notably implicit parameters.
---
--- We want to 'look through' type synonyms when doing this
--- so it's better done on the Type than the HsType
-
-hoistForAllTys ty
-  = let
-       no_shadow_ty = deShadowTy ty
-       -- Running over ty with an empty substitution gives it the
-       -- no-shadowing property.  This is important.  For example:
-       --      type Foo r = forall a. a -> r
-       --      foo :: Foo (Foo ())
-       -- Here the hoisting should give
-       --      foo :: forall a a1. a -> a1 -> ()
-       --
-       -- What about type vars that are lexically in scope in the envt?
-       -- We simply rely on them having a different unique to any
-       -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
-       -- out of the envt, which is boring and (I think) not necessary.
-    in
-    case hoist no_shadow_ty of 
-       (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
-               -- The 'nubBy' eliminates duplicate constraints,
-               -- notably implicit parameters
+pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
+pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon, 
+                                nest 2 (pp_sig ctxt) ]
   where
-    hoist ty
-       | (tvs1, body_ty) <- tcSplitForAllTys ty,
-         not (null tvs1)
-       = case hoist body_ty of
-               (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
-
-       | Just (arg, res) <- tcSplitFunTy_maybe ty
-       = let
-             arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
-         in                            -- to the argument type
-         if (isPredTy arg') then
-           case hoist res of
-               (tvs,theta,tau) -> (tvs, arg':theta, tau)
-         else
-            case hoist res of
-               (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
-
-       | otherwise = ([], [], ty)
+    pp_sig (FunSigCtxt n)  = pp_n_colon n
+    pp_sig (ConArgCtxt n)  = pp_n_colon n
+    pp_sig (ForSigCtxt n)  = pp_n_colon n
+    pp_sig (RuleSigCtxt n) = pp_n_colon n
+    pp_sig other          = ppr (unLoc hs_ty)
+
+    pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
+
+
+wobblyPatSig sig_tvs
+  = hang (ptext SLIT("A pattern type signature cannot bind scoped type variables") 
+               <+> pprQuotedList sig_tvs)
+       2 (ptext SLIT("unless the pattern has a rigid type context"))
+               
+scopedNonVar n ty
+  = vcat [sep [ptext SLIT("The scoped type variable") <+> quotes (ppr n),
+              nest 2 (ptext SLIT("is bound to the type") <+> quotes (ppr ty))],
+         nest 2 (ptext SLIT("You can only bind scoped type variables to type variables"))]
+
+dupInScope n n' ty
+  = hang (ptext SLIT("The scoped type variables") <+> quotes (ppr n) <+> ptext SLIT("and") <+> quotes (ppr n'))
+       2 (vcat [ptext SLIT("are bound to the same type (variable)"),
+               ptext SLIT("Distinct scoped type variables must be distinct")])
 \end{code}