Simplify the implementation of Implicit Parameters

This patch re-implements implicit parameters via a class
with a functional dependency:

    class IP (n::Symbol) a | n -> a where
      ip :: a

This definition is in the library module GHC.IP. Notice
how it use a type-literal, so we can have constraints like
   IP "x" Int
Now all the functional dependency machinery works right to make
implicit parameters behave as they should.

Much special-case processing for implicit parameters can be removed
entirely. One particularly nice thing is not having a dedicated
"original-name cache" for implicit parameters (the nsNames field of
NameCache).  But many other cases disappear:

  * BasicTypes.IPName
  * IPTyCon constructor in Tycon.TyCon
  * CIPCan constructor  in TcRnTypes.Ct
  * IPPred constructor  in Types.PredTree

Implicit parameters remain special in a few ways:

 * Special syntax.  Eg the constraint (IP "x" Int) is parsed
   and printed as (?x::Int).  And we still have local bindings
   for implicit parameters, and occurrences thereof.

 * A implicit-parameter binding  (let ?x = True in e) amounts
   to a local instance declaration, which we have not had before.
   It just generates an implication contraint (easy), but when
   going under it we must purge any existing bindings for
   ?x in the inert set.  See Note [Shadowing of Implicit Parameters]
   in TcSimplify

 * TcMType.sizePred classifies implicit parameter constraints as size-0,
   as before the change

There are accompanying patches to libraries 'base' and 'haddock'

All the work was done by Iavor Diatchki

39 files changed, 309 insertions, 480 deletions

diff --git a/compiler/basicTypes/BasicTypes.lhs b/compiler/basicTypes/BasicTypes.lhs
index 6db5788d2f..86b93ab9a2 100644
--- a/compiler/basicTypes/BasicTypes.lhs
+++ b/compiler/basicTypes/BasicTypes.lhs
@@ -39,8 +39,6 @@ module BasicTypes(
 	negateFixity, funTyFixity,
 	compareFixity,
 
-	IPName(..), ipNameName, mapIPName,
-
 	RecFlag(..), isRec, isNonRec, boolToRecFlag,
 
 	RuleName,
@@ -178,32 +176,6 @@ instance Outputable WarningTxt where
 
 %************************************************************************
 %*									*
-\subsection{Implicit parameter identity}
-%*									*
-%************************************************************************
-
-The @IPName@ type is here because it is used in TypeRep (i.e. very
-early in the hierarchy), but also in HsSyn.
-
-\begin{code}
-newtype IPName name = IPName name	-- ?x
-  deriving( Eq, Data, Typeable )
-
-instance Functor IPName where
-    fmap = mapIPName
-
-ipNameName :: IPName name -> name
-ipNameName (IPName n) = n
-
-mapIPName :: (a->b) -> IPName a -> IPName b
-mapIPName f (IPName n) = IPName (f n)
-
-instance Outputable name => Outputable (IPName name) where
-    ppr (IPName n) = char '?' <> ppr n -- Ordinary implicit parameters
-\end{code}
-
-%************************************************************************
-%*									*
 		Rules
 %*									*
 %************************************************************************
diff --git a/compiler/basicTypes/Unique.lhs b/compiler/basicTypes/Unique.lhs
index 39b30d93f7..48afc8da41 100644
--- a/compiler/basicTypes/Unique.lhs
+++ b/compiler/basicTypes/Unique.lhs
@@ -179,9 +179,6 @@ instance Uniquable FastString where
 
 instance Uniquable Int where
  getUnique i = mkUniqueGrimily i
-
-instance Uniquable n => Uniquable (IPName n) where
-  getUnique (IPName n) = getUnique n
 \end{code}
 
 
diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs
index 25dfaababa..6123e0a346 100644
--- a/compiler/coreSyn/MkCore.lhs
+++ b/compiler/coreSyn/MkCore.lhs
@@ -25,9 +25,6 @@ module MkCore (
         -- * Floats
         FloatBind(..), wrapFloat,
 
-        -- * Constructing/deconstructing implicit parameter boxes
-        mkIPUnbox, mkIPBox,
-
         -- * Constructing/deconstructing equality evidence boxes
         mkEqBox,
         
@@ -62,7 +59,7 @@ module MkCore (
 #include "HsVersions.h"
 
 import Id
-import Var      ( IpId, EvVar, setTyVarUnique )
+import Var      ( EvVar, setTyVarUnique )
 
 import CoreSyn
 import CoreUtils        ( exprType, needsCaseBinding, bindNonRec )
@@ -72,8 +69,7 @@ import HscTypes
 import TysWiredIn
 import PrelNames
 
-import IParam           ( ipCoAxiom )
-import TcType		( mkSigmaTy, evVarPred )
+import TcType		( mkSigmaTy )
 import Type
 import Coercion
 import TysPrim
@@ -303,21 +299,6 @@ mkStringExprFS str
 
 \begin{code}
 
-mkIPBox :: IPName IpId -> CoreExpr -> CoreExpr
-mkIPBox ipx e = e `Cast` mkSymCo (mkAxInstCo (ipCoAxiom ip) [ty])
-  where x = ipNameName ipx
-        Just (ip, ty) = getIPPredTy_maybe (evVarPred x)
-        -- NB: don't use the DataCon work id because we don't generate code for it
-
-mkIPUnbox :: IPName IpId -> CoreExpr
-mkIPUnbox ipx = Var x `Cast` mkAxInstCo (ipCoAxiom ip) [ty]
-  where x = ipNameName ipx
-        Just (ip, ty) = getIPPredTy_maybe (evVarPred x)
-
-\end{code}
-
-\begin{code}
-
 mkEqBox :: Coercion -> CoreExpr
 mkEqBox co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
              Var (dataConWorkId eqBoxDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
diff --git a/compiler/deSugar/DsExpr.lhs b/compiler/deSugar/DsExpr.lhs
index a60d3c4a80..11fa5d53c9 100644
--- a/compiler/deSugar/DsExpr.lhs
+++ b/compiler/deSugar/DsExpr.lhs
@@ -86,9 +86,9 @@ dsIPBinds (IPBinds ip_binds ev_binds) body
                 -- dependency order; hence Rec
         ; foldrM ds_ip_bind inner ip_binds }
   where
-    ds_ip_bind (L _ (IPBind n e)) body
+    ds_ip_bind (L _ (IPBind ~(Right n) e)) body
       = do e' <- dsLExpr e
-           return (Let (NonRec (ipNameName n) (mkIPBox n e')) body)
+           return (Let (NonRec n e') body)
 
 -------------------------
 ds_val_bind :: (RecFlag, LHsBinds Id) -> CoreExpr -> DsM CoreExpr
@@ -188,7 +188,7 @@ dsExpr :: HsExpr Id -> DsM CoreExpr
 dsExpr (HsPar e)              = dsLExpr e
 dsExpr (ExprWithTySigOut e _) = dsLExpr e
 dsExpr (HsVar var)            = return (varToCoreExpr var)   -- See Note [Desugaring vars]
-dsExpr (HsIPVar ip)           = return (mkIPUnbox ip)
+dsExpr (HsIPVar _)            = panic "dsExpr: HsIPVar"
 dsExpr (HsLit lit)            = dsLit lit
 dsExpr (HsOverLit lit)        = dsOverLit lit
 
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index bfd44384bb..4371bca95e 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -404,7 +404,6 @@ Library
         TcCanonical
         TcSMonad
         Class
-        IParam
         Coercion
         FamInstEnv
         FunDeps
diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index 3fd7efc538..7de9018dbe 100644
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -416,10 +416,12 @@ isEmptyIPBinds (IPBinds is ds) = null is && isEmptyTcEvBinds ds
 type LIPBind id = Located (IPBind id)
 
 -- | Implicit parameter bindings.
+{- These bindings start off as (Left "x") in the parser and stay
+that way until after type-checking when they are replaced with
+(Right d), where "d" is the name of the dictionary holding the
+evidene for the implicit parameter. -}
 data IPBind id
-  = IPBind
-        (IPName id)
-        (LHsExpr id)
+  = IPBind (Either HsIPName id) (LHsExpr id)
   deriving (Data, Typeable)
 
 instance (OutputableBndr id) => Outputable (HsIPBinds id) where
@@ -427,7 +429,10 @@ instance (OutputableBndr id) => Outputable (HsIPBinds id) where
                         $$ ifPprDebug (ppr ds)
 
 instance (OutputableBndr id) => Outputable (IPBind id) where
-  ppr (IPBind id rhs) = pprBndr LetBind id <+> equals <+> pprExpr (unLoc rhs)
+  ppr (IPBind lr rhs) = name <+> equals <+> pprExpr (unLoc rhs)
+    where name = case lr of
+                   Left ip  -> pprBndr LetBind ip
+                   Right id -> pprBndr LetBind id
 \end{code}
 
 
diff --git a/compiler/hsSyn/HsExpr.lhs b/compiler/hsSyn/HsExpr.lhs
index c7f4459d6e..dcfcb9f8f0 100644
--- a/compiler/hsSyn/HsExpr.lhs
+++ b/compiler/hsSyn/HsExpr.lhs
@@ -106,7 +106,7 @@ noSyntaxTable = []
 -- | A Haskell expression.
 data HsExpr id
   = HsVar     id                        -- ^ variable
-  | HsIPVar   (IPName id)               -- ^ implicit parameter
+  | HsIPVar   HsIPName                  -- ^ implicit parameter
   | HsOverLit (HsOverLit id)            -- ^ Overloaded literals
 
   | HsLit     HsLit                     -- ^ Simple (non-overloaded) literals
diff --git a/compiler/hsSyn/HsTypes.lhs b/compiler/hsSyn/HsTypes.lhs
index eec87c4ded..a57c48a1c6 100644
--- a/compiler/hsSyn/HsTypes.lhs
+++ b/compiler/hsSyn/HsTypes.lhs
@@ -18,6 +18,7 @@ module HsTypes (
         HsQuasiQuote(..),
         HsTyWrapper(..),
         HsTyLit(..),
+        HsIPName(..), hsIPNameFS,
 
         LBangType, BangType, HsBang(..), 
         getBangType, getBangStrictness, 
@@ -158,6 +159,24 @@ mkHsWithBndrs :: thing -> HsWithBndrs thing
 mkHsWithBndrs x = HsWB { hswb_cts = x, hswb_kvs = panic "mkHsTyWithBndrs:kvs"
                                      , hswb_tvs = panic "mkHsTyWithBndrs:tvs" }
 
+
+-- | These names are used eary on to store the names of implicit
+-- parameters.  They completely disappear after type-checking.
+newtype HsIPName = HsIPName FastString-- ?x
+  deriving( Eq, Data, Typeable )
+
+hsIPNameFS :: HsIPName -> FastString
+hsIPNameFS (HsIPName n) = n
+
+instance Outputable HsIPName where
+    ppr (HsIPName n) = char '?' <> ftext n -- Ordinary implicit parameters
+
+instance OutputableBndr HsIPName where
+    pprBndr _ n   = ppr n         -- Simple for now
+    pprInfixOcc  n = ppr n
+    pprPrefixOcc n = ppr n
+
+
 data HsTyVarBndr name
   = UserTyVar           -- No explicit kinding
          name           -- See Note [Printing KindedTyVars]
@@ -201,7 +220,7 @@ data HsType name
         -- Parenthesis preserved for the precedence re-arrangement in RnTypes
         -- It's important that a * (b + c) doesn't get rearranged to (a*b) + c!
 
-  | HsIParamTy          (IPName name)    -- (?x :: ty)
+  | HsIParamTy          HsIPName         -- (?x :: ty)
                         (LHsType name)   -- Implicit parameters as they occur in contexts
 
   | HsEqTy              (LHsType name)   -- ty1 ~ ty2
diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index 5d1c48f183..f03808fbd2 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -19,9 +19,8 @@ module BinIface (
 #include "HsVersions.h"
 
 import TcRnMonad
-import TyCon      (TyCon, tyConName, tupleTyConSort, tupleTyConArity, isTupleTyCon, tyConIP_maybe)
+import TyCon      (TyCon, tyConName, tupleTyConSort, tupleTyConArity, isTupleTyCon)
 import DataCon    (dataConName, dataConWorkId, dataConTyCon)
-import IParam     (ipFastString, ipTyConName)
 import PrelInfo   (wiredInThings, basicKnownKeyNames)
 import Id         (idName, isDataConWorkId_maybe)
 import TysWiredIn
@@ -316,7 +315,7 @@ knownKeyNamesMap = listToUFM_Directly [(nameUnique n, n) | n <- knownKeyNames]
 
 -- See Note [Symbol table representation of names]
 putName :: BinDictionary -> BinSymbolTable -> BinHandle -> Name -> IO ()
-putName dict BinSymbolTable{ 
+putName _dict BinSymbolTable{ 
                bin_symtab_map = symtab_map_ref,
                bin_symtab_next = symtab_next }    bh name
   | name `elemUFM` knownKeyNamesMap
@@ -327,10 +326,6 @@ putName dict BinSymbolTable{
   = case wiredInNameTyThing_maybe name of
      Just (ATyCon tc)
        | isTupleTyCon tc             -> putTupleName_ bh tc 0
-       | Just ip <- tyConIP_maybe tc -> do
-         off <- allocateFastString dict (ipFastString ip)
-         -- MASSERT(off < 2^(30 :: Int))
-         put_ bh (0xC0000000 .|. off)
      Just (ADataCon dc)
        | let tc = dataConTyCon dc, isTupleTyCon tc -> putTupleName_ bh tc 1
      Just (AnId x)
@@ -362,7 +357,7 @@ putTupleName_ bh tc thing_tag
 getSymtabName :: NameCacheUpdater
               -> Dictionary -> SymbolTable
               -> BinHandle -> IO Name
-getSymtabName ncu dict symtab bh = do
+getSymtabName _ncu _dict symtab bh = do
     i <- get bh
     case i .&. 0xC0000000 of
         0x00000000 -> return $! symtab ! fromIntegral (i ::  Word32)
@@ -385,7 +380,6 @@ getSymtabName ncu dict symtab bh = do
                      _ -> pprPanic "getSymtabName:unknown tuple sort" (ppr i)
             thing_tag = (i .&. 0x0CFFFFFF) `shiftR` 26
             arity = fromIntegral (i .&. 0x03FFFFFF)
-        0xC0000000 -> liftM ipTyConName $ updateNameCache ncu $ flip allocateIPName (dict ! fromIntegral (i .&. 0x3FFFFFFF))
         _          -> pprPanic "getSymtabName:unknown name tag" (ppr i)
 
 data BinSymbolTable = BinSymbolTable {
@@ -426,7 +420,6 @@ data BinDictionary = BinDictionary {
 -- All the binary instances
 
 -- BasicTypes
-{-! for IPName derive: Binary !-}
 {-! for Fixity derive: Binary !-}
 {-! for FixityDirection derive: Binary !-}
 {-! for Boxity derive: Binary !-}
@@ -825,11 +818,6 @@ instance Binary Fixity where
           ab <- get bh
           return (Fixity aa ab)
 
-instance (Binary name) => Binary (IPName name) where
-    put_ bh (IPName aa) = put_ bh aa
-    get bh = do aa <- get bh
-                return (IPName aa)
-
 -------------------------------------------------------------------------
 --              Types from: Demand
 -------------------------------------------------------------------------
@@ -1057,8 +1045,7 @@ instance Binary IfaceCoCon where
    put_ bh IfaceTransCo        = putByte bh 4
    put_ bh IfaceInstCo         = putByte bh 5
    put_ bh (IfaceNthCo d)      = do { putByte bh 6; put_ bh d }
-   put_ bh (IfaceIPCoAx ip)    = do { putByte bh 7; put_ bh ip }
-  
+
    get bh = do
         h <- getByte bh
         case h of
@@ -1069,7 +1056,6 @@ instance Binary IfaceCoCon where
           4 -> return IfaceTransCo
           5 -> return IfaceInstCo
           6 -> do { d <- get bh; return (IfaceNthCo d) }
-          7 -> do { ip <- get bh; return (IfaceIPCoAx ip) }
           _ -> panic ("get IfaceCoCon " ++ show h)
 
 -------------------------------------------------------------------------
diff --git a/compiler/iface/IfaceEnv.lhs b/compiler/iface/IfaceEnv.lhs
index 1e776f52a3..20a21c3733 100644
--- a/compiler/iface/IfaceEnv.lhs
+++ b/compiler/iface/IfaceEnv.lhs
@@ -12,14 +12,14 @@ module IfaceEnv (
 	newGlobalBinder, newImplicitBinder, 
 	lookupIfaceTop,
 	lookupOrig, lookupOrigNameCache, extendNameCache,
-	newIPName, newIfaceName, newIfaceNames,
+	newIfaceName, newIfaceNames,
 	extendIfaceIdEnv, extendIfaceTyVarEnv, 
 	tcIfaceLclId, tcIfaceTyVar, lookupIfaceTyVar,
 
 	ifaceExportNames,
 
 	-- Name-cache stuff
-	allocateGlobalBinder, allocateIPName, initNameCache, updNameCache,
+	allocateGlobalBinder, initNameCache, updNameCache,
         getNameCache, mkNameCacheUpdater, NameCacheUpdater(..)
    ) where
 
@@ -40,14 +40,12 @@ import UniqFM
 import FastString
 import UniqSupply
 import SrcLoc
-import BasicTypes
 import Util
 
 import Outputable
 import Exception     ( evaluate )
 
 import Data.IORef    ( atomicModifyIORef, readIORef )
-import qualified Data.Map as Map
 \end{code}
 
 
@@ -165,21 +163,6 @@ lookupOrig mod occ
                     new_cache = extendNameCache (nsNames name_cache) mod occ name
                   in (name_cache{ nsUniqs = us, nsNames = new_cache }, name)
     }}}
-
-allocateIPName :: NameCache -> FastString -> (NameCache, IPName Name)
-allocateIPName name_cache ip = case Map.lookup ip ipcache of
-    Just name_ip -> (name_cache, name_ip)
-    Nothing      -> (new_ns, name_ip)
-       where
-         (us_here, us') = splitUniqSupply (nsUniqs name_cache)
-         tycon_u:datacon_u:dc_wrk_u:co_ax_u:_ = uniqsFromSupply us_here
-         name_ip     = mkIPName ip tycon_u datacon_u dc_wrk_u co_ax_u
-         new_ipcache = Map.insert ip name_ip ipcache
-         new_ns      = name_cache {nsUniqs = us', nsIPs = new_ipcache}
-  where ipcache = nsIPs name_cache
-
-newIPName :: FastString -> TcRnIf m n (IPName Name)
-newIPName ip = updNameCache $ flip allocateIPName ip
 \end{code}
 
 %************************************************************************
@@ -249,8 +232,7 @@ mkNameCacheUpdater = do
 initNameCache :: UniqSupply -> [Name] -> NameCache
 initNameCache us names
   = NameCache { nsUniqs = us,
-		nsNames = initOrigNames names,
-                nsIPs   = Map.empty }
+		nsNames = initOrigNames names }
 
 initOrigNames :: [Name] -> OrigNameCache
 initOrigNames names = foldl extendOrigNameCache emptyModuleEnv names
diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs
index 6b7a33771f..c484b0637f 100644
--- a/compiler/iface/IfaceType.lhs
+++ b/compiler/iface/IfaceType.lhs
@@ -14,7 +14,7 @@ This module defines interface types and binders
 -- for details
 
 module IfaceType (
-	IfExtName, IfLclName, IfIPName,
+	IfExtName, IfLclName,
 
         IfaceType(..), IfacePredType, IfaceKind, IfaceTyCon(..), IfaceCoCon(..),
         IfaceTyLit(..),
@@ -37,8 +37,6 @@ module IfaceType (
 
 import Coercion
 import TypeRep hiding( maybeParen )
-import Type (tyConAppTyCon_maybe)
-import IParam (ipFastString)
 import TyCon
 import Id
 import Var
@@ -62,8 +60,6 @@ type IfLclName = FastString	-- A local name in iface syntax
 type IfExtName = Name	-- An External or WiredIn Name can appear in IfaceSyn
      	       	 	-- (However Internal or System Names never should)
 
-type IfIPName = FastString -- Represent implicit parameters simply as a string
-
 data IfaceBndr 		-- Local (non-top-level) binders
   = IfaceIdBndr {-# UNPACK #-} !IfaceIdBndr
   | IfaceTvBndr {-# UNPACK #-} !IfaceTvBndr
@@ -99,7 +95,6 @@ newtype IfaceTyCon = IfaceTc { ifaceTyConName :: IfExtName }
   -- Coercion constructors
 data IfaceCoCon
   = IfaceCoAx IfExtName
-  | IfaceIPCoAx FastString
   | IfaceReflCo    | IfaceUnsafeCo  | IfaceSymCo
   | IfaceTransCo   | IfaceInstCo
   | IfaceNthCo Int
@@ -253,10 +248,6 @@ ppr_tc_app _         (IfaceTc n) tys
   , Just sort <- tyConTuple_maybe tc
   , tyConArity tc == length tys 
   = tupleParens sort (sep (punctuate comma (map pprIfaceType tys)))
-  | Just (ATyCon tc) <- wiredInNameTyThing_maybe n
-  , Just ip <- tyConIP_maybe tc
-  , [ty] <- tys
-  = parens (ppr ip <> dcolon <> pprIfaceType ty)
 ppr_tc_app ctxt_prec tc tys
   = maybeParen ctxt_prec tYCON_PREC
                (sep [ppr_tc tc, nest 4 (sep (map pprParendIfaceType tys))])
@@ -279,7 +270,6 @@ instance Outputable IfaceTyCon where
 
 instance Outputable IfaceCoCon where
   ppr (IfaceCoAx n)    = ppr n
-  ppr (IfaceIPCoAx ip) = ppr (IPName ip)
   ppr IfaceReflCo      = ptext (sLit "Refl")
   ppr IfaceUnsafeCo    = ptext (sLit "Unsafe")
   ppr IfaceSymCo       = ptext (sLit "Sym")
@@ -386,11 +376,6 @@ coToIfaceType (InstCo co ty)        = IfaceCoConApp IfaceInstCo
                                                     , toIfaceType ty ]
 
 coAxiomToIfaceType :: CoAxiom -> IfaceCoCon
-coAxiomToIfaceType con
-  | Just tc <- tyConAppTyCon_maybe (co_ax_lhs con)
-  , Just ip <- tyConIP_maybe tc
-  = IfaceIPCoAx (ipFastString ip)
-  | otherwise
-  = IfaceCoAx (coAxiomName con)
+coAxiomToIfaceType con = IfaceCoAx (coAxiomName con)
 \end{code}
 
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 18c9a8cba9..e63bf7268f 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -37,7 +37,6 @@ import Id
 import MkId
 import IdInfo
 import Class
-import IParam
 import TyCon
 import DataCon
 import PrelNames
@@ -958,7 +957,6 @@ tcIfaceCo (IfaceForAllTy tv t)  = bindIfaceTyVar tv $ \ tv' ->
 tcIfaceCoApp :: IfaceCoCon -> [IfaceType] -> IfL Coercion
 tcIfaceCoApp IfaceReflCo      [t]     = Refl         <$> tcIfaceType t
 tcIfaceCoApp (IfaceCoAx n)    ts      = AxiomInstCo  <$> tcIfaceCoAxiom n <*> mapM tcIfaceCo ts
-tcIfaceCoApp (IfaceIPCoAx ip) ts      = AxiomInstCo  <$> liftM ipCoAxiom (newIPName ip) <*> mapM tcIfaceCo ts
 tcIfaceCoApp IfaceUnsafeCo    [t1,t2] = UnsafeCo     <$> tcIfaceType t1 <*> tcIfaceType t2
 tcIfaceCoApp IfaceSymCo       [t]     = SymCo        <$> tcIfaceCo t
 tcIfaceCoApp IfaceTransCo     [t1,t2] = TransCo      <$> tcIfaceCo t1 <*> tcIfaceCo t2
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 484744373d..f5fc45aab3 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -2174,6 +2174,11 @@ impliedFlags
     , (Opt_RecordWildCards,     turnOn, Opt_DisambiguateRecordFields)
 
     , (Opt_ParallelArrays, turnOn, Opt_ParallelListComp)
+
+    -- An implicit parameter constraint, `?x::Int`, is desugared into
+    -- `IP "x" Int`, which requires a flexible context/instance.
+    , (Opt_ImplicitParams, turnOn, Opt_FlexibleContexts)
+    , (Opt_ImplicitParams, turnOn, Opt_FlexibleInstances)
   ]
 
 optLevelFlags :: [([Int], DynFlag)]
diff --git a/compiler/main/HscTypes.lhs b/compiler/main/HscTypes.lhs
index 6d1a9c02fb..1631e8ccaf 100644
--- a/compiler/main/HscTypes.lhs
+++ b/compiler/main/HscTypes.lhs
@@ -73,7 +73,7 @@ module HscTypes (
         -- * Information on imports and exports
         WhetherHasOrphans, IsBootInterface, Usage(..),
         Dependencies(..), noDependencies,
-        NameCache(..), OrigNameCache, OrigIParamCache,
+        NameCache(..), OrigNameCache,
         IfaceExport,
 
         -- * Warnings
@@ -162,7 +162,6 @@ import Util
 import Control.Monad    ( mplus, guard, liftM, when )
 import Data.Array       ( Array, array )
 import Data.IORef
-import Data.Map         ( Map )
 import Data.Time
 import Data.Word
 import Data.Typeable    ( Typeable )
@@ -1763,17 +1762,12 @@ its binding site, we fix it up.
 data NameCache
  = NameCache {  nsUniqs :: UniqSupply,
                 -- ^ Supply of uniques
-                nsNames :: OrigNameCache,
+                nsNames :: OrigNameCache
                 -- ^ Ensures that one original name gets one unique
-                nsIPs   :: OrigIParamCache
-                -- ^ Ensures that one implicit parameter name gets one unique
    }
 
 -- | Per-module cache of original 'OccName's given 'Name's
 type OrigNameCache   = ModuleEnv (OccEnv Name)
-
--- | Module-local cache of implicit parameter 'OccName's given 'Name's
-type OrigIParamCache = Map FastString (IPName Name)
 \end{code}
 
 
diff --git a/compiler/parser/Parser.y.pp b/compiler/parser/Parser.y.pp
index 759d5449f9..21f8782f6f 100644
--- a/compiler/parser/Parser.y.pp
+++ b/compiler/parser/Parser.y.pp
@@ -1762,10 +1762,10 @@ dbinds  :: { Located [LIPBind RdrName] }
 --      | {- empty -}                   { [] }
 
 dbind   :: { LIPBind RdrName }
-dbind   : ipvar '=' exp                 { LL (IPBind (unLoc $1) $3) }
+dbind   : ipvar '=' exp                 { LL (IPBind (Left (unLoc $1)) $3) }
 
-ipvar   :: { Located (IPName RdrName) }
-        : IPDUPVARID            { L1 (IPName (mkUnqual varName (getIPDUPVARID $1))) }
+ipvar   :: { Located HsIPName }
+        : IPDUPVARID            { L1 (HsIPName (getIPDUPVARID $1)) }
 
 -----------------------------------------------------------------------------
 -- Warnings and deprecations
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index 5af98df4e8..3a39d531bb 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -285,6 +285,9 @@ basicKnownKeyNames
         typeNatMulTyFamName,
         typeNatExpTyFamName,
 
+        -- Implicit parameters
+        ipClassName,
+
         -- Annotation type checking
         toAnnotationWrapperName
 
@@ -348,7 +351,7 @@ gHC_PRIM, gHC_TYPES, gHC_GENERICS,
     gHC_FLOAT, gHC_TOP_HANDLER, sYSTEM_IO, dYNAMIC, tYPEABLE, tYPEABLE_INTERNAL, gENERICS,
     dOTNET, rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, mONAD_ZIP,
     aRROW, cONTROL_APPLICATIVE, gHC_DESUGAR, rANDOM, gHC_EXTS,
-    cONTROL_EXCEPTION_BASE, gHC_TYPELITS :: Module
+    cONTROL_EXCEPTION_BASE, gHC_TYPELITS, gHC_IP :: Module
 
 gHC_PRIM        = mkPrimModule (fsLit "GHC.Prim")   -- Primitive types and values
 gHC_TYPES       = mkPrimModule (fsLit "GHC.Types")
@@ -402,6 +405,7 @@ rANDOM          = mkBaseModule (fsLit "System.Random")
 gHC_EXTS        = mkBaseModule (fsLit "GHC.Exts")
 cONTROL_EXCEPTION_BASE = mkBaseModule (fsLit "Control.Exception.Base")
 gHC_TYPELITS    = mkBaseModule (fsLit "GHC.TypeLits")
+gHC_IP          = mkBaseModule (fsLit "GHC.IP")
 
 gHC_PARR' :: Module
 gHC_PARR' = mkBaseModule (fsLit "GHC.PArr")
@@ -1081,6 +1085,12 @@ typeNatAddTyFamName = tcQual  gHC_TYPELITS (fsLit "+")   typeNatAddTyFamNameKey
 typeNatMulTyFamName = tcQual  gHC_TYPELITS (fsLit "*")   typeNatMulTyFamNameKey
 typeNatExpTyFamName = tcQual  gHC_TYPELITS (fsLit "^")   typeNatExpTyFamNameKey
 
+-- Implicit parameters
+ipClassName :: Name
+ipClassName         = clsQual gHC_IP (fsLit "IP")      ipClassNameKey
+
+
+
 -- dotnet interop
 objectTyConName :: Name
 objectTyConName     = tcQual   dOTNET (fsLit "Object") objectTyConKey
@@ -1201,6 +1211,9 @@ typeNatLeqClassNameKey  = mkPreludeClassUnique 43
 
 ghciIoClassKey :: Unique
 ghciIoClassKey = mkPreludeClassUnique 44
+
+ipClassNameKey :: Unique
+ipClassNameKey = mkPreludeClassUnique 45
 \end{code}
 
 %************************************************************************
diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs
index 60518bfd9f..78e1f74b4d 100644
--- a/compiler/prelude/TysWiredIn.lhs
+++ b/compiler/prelude/TysWiredIn.lhs
@@ -72,8 +72,6 @@ module TysWiredIn (
         -- * Equality predicates
         eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon,
 
-        -- * Implicit parameter predicates
-        mkIPName
     ) where
 
 #include "HsVersions.h"
@@ -85,7 +83,6 @@ import PrelNames
 import TysPrim
 
 -- others:
-import Coercion
 import Constants	( mAX_TUPLE_SIZE )
 import Module		( Module )
 import Type             ( mkTyConApp )
@@ -95,7 +92,7 @@ import TyCon
 import TypeRep
 import RdrName
 import Name
-import BasicTypes       ( TupleSort(..), tupleSortBoxity, IPName(..), 
+import BasicTypes       ( TupleSort(..), tupleSortBoxity,
                           Arity, RecFlag(..), Boxity(..), HsBang(..) )
 import ForeignCall
 import Unique           ( incrUnique, mkTupleTyConUnique,
@@ -254,9 +251,6 @@ pcTyCon is_enum is_rec name cType tyvars cons
 pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
 pcDataCon = pcDataConWithFixity False
 
-pcDataCon' :: Name -> Unique -> [TyVar] -> [Type] -> TyCon -> DataCon
-pcDataCon' = pcDataConWithFixity' False
-
 pcDataConWithFixity :: Bool -> Name -> [TyVar] -> [Type] -> TyCon -> DataCon
 pcDataConWithFixity infx n = pcDataConWithFixity' infx n (incrUnique (nameUnique n))
 -- The Name's unique is the first of two free uniques;
@@ -395,39 +389,6 @@ unboxedPairDataCon :: DataCon
 unboxedPairDataCon = tupleCon   UnboxedTuple 2
 \end{code}
 
-%************************************************************************
-%*                                                                      *
-\subsection[TysWiredIn-ImplicitParams]{Special type constructors for implicit parameters}
-%*                                                                      *
-%************************************************************************
-
-\begin{code}
-mkIPName :: FastString
-         -> Unique -> Unique -> Unique -> Unique
-         -> IPName Name
-mkIPName ip tycon_u datacon_u dc_wrk_u co_ax_u = name_ip
-  where
-    name_ip = IPName tycon_name
-
-    tycon_name = mkPrimTyConName ip tycon_u tycon
-    tycon      = mkAlgTyCon tycon_name
-                   (liftedTypeKind `mkArrowKind` constraintKind)
-                   [alphaTyVar]
-                   Nothing
-                   []      -- No stupid theta
-                   (NewTyCon { data_con    = datacon, 
-                               nt_rhs      = mkTyVarTy alphaTyVar,
-                               nt_etad_rhs = ([alphaTyVar], mkTyVarTy alphaTyVar),
-                               nt_co       = mkNewTypeCo co_ax_name tycon [alphaTyVar] (mkTyVarTy alphaTyVar) })
-                   (IPTyCon name_ip)
-                   NonRecursive
-                   False
-
-    datacon_name = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "IPBox") datacon_u datacon
-    datacon      = pcDataCon' datacon_name dc_wrk_u [alphaTyVar] [mkTyVarTy alphaTyVar] tycon
-
-    co_ax_name = mkPrimTyConName ip co_ax_u tycon
-\end{code}
 
 %************************************************************************
 %*									*
diff --git a/compiler/rename/RnBinds.lhs b/compiler/rename/RnBinds.lhs
index 536d83b344..d3d16033eb 100644
--- a/compiler/rename/RnBinds.lhs
+++ b/compiler/rename/RnBinds.lhs
@@ -35,7 +35,7 @@ import {-# SOURCE #-} RnExpr( rnLExpr, rnStmts )
 import HsSyn
 import TcRnMonad
 import TcEvidence     ( emptyTcEvBinds )
-import RnTypes        ( bindSigTyVarsFV, rnIPName, rnHsSigType, rnLHsType, checkPrecMatch )
+import RnTypes        ( bindSigTyVarsFV, rnHsSigType, rnLHsType, checkPrecMatch )
 import RnPat
 import RnEnv
 import DynFlags
@@ -220,10 +220,9 @@ rnIPBinds (IPBinds ip_binds _no_dict_binds) = do
     return (IPBinds ip_binds' emptyTcEvBinds, plusFVs fvs_s)
 
 rnIPBind :: IPBind RdrName -> RnM (IPBind Name, FreeVars)
-rnIPBind (IPBind n expr) = do
-    n' <- rnIPName n
+rnIPBind (IPBind ~(Left n) expr) = do
     (expr',fvExpr) <- rnLExpr expr
-    return (IPBind n' expr', fvExpr)
+    return (IPBind (Left n) expr', fvExpr)
 \end{code}
 
 
diff --git a/compiler/rename/RnExpr.lhs b/compiler/rename/RnExpr.lhs
index 3bb56ebfda..d27ef98e80 100644
--- a/compiler/rename/RnExpr.lhs
+++ b/compiler/rename/RnExpr.lhs
@@ -111,8 +111,7 @@ rnExpr (HsVar v)
        finishHsVar name
 
 rnExpr (HsIPVar v)
-  = do v' <- rnIPName v
-       return (HsIPVar v', emptyFVs)
+  = return (HsIPVar v, emptyFVs)
 
 rnExpr (HsLit lit@(HsString s))
   = do {
diff --git a/compiler/rename/RnTypes.lhs b/compiler/rename/RnTypes.lhs
index ecdfdaf36e..ed2144084a 100644
--- a/compiler/rename/RnTypes.lhs
+++ b/compiler/rename/RnTypes.lhs
@@ -16,7 +16,7 @@ module RnTypes (
 	rnHsType, rnLHsType, rnLHsTypes, rnContext,
         rnHsKind, rnLHsKind, rnLHsMaybeKind,
 	rnHsSigType, rnLHsInstType, rnConDeclFields,
-        rnIPName, newTyVarNameRn,
+        newTyVarNameRn,
 
 	-- Precence related stuff
 	mkOpAppRn, mkNegAppRn, mkOpFormRn, mkConOpPatRn,
@@ -41,7 +41,6 @@ import HsSyn
 import RnHsDoc          ( rnLHsDoc, rnMbLHsDoc )
 import RnEnv
 import TcRnMonad
-import IfaceEnv         ( newIPName )
 import RdrName
 import PrelNames
 import TysPrim          ( funTyConName )
@@ -50,7 +49,7 @@ import SrcLoc
 import NameSet
 
 import Util
-import BasicTypes	( IPName(..), ipNameName, compareFixity, funTyFixity, negateFixity, 
+import BasicTypes	( compareFixity, funTyFixity, negateFixity, 
 			  Fixity(..), FixityDirection(..) )
 import Outputable
 import FastString
@@ -248,8 +247,7 @@ rnHsTyKi isType doc (HsAppTy ty1 ty2)
 rnHsTyKi isType doc (HsIParamTy n ty)
   = ASSERT( isType )
     do { (ty', fvs) <- rnLHsType doc ty
-       ; n' <- rnIPName n
-       ; return (HsIParamTy n' ty', fvs) }
+       ; return (HsIParamTy n ty', fvs) }
 
 rnHsTyKi isType doc (HsEqTy ty1 ty2) 
   = ASSERT( isType )
@@ -494,9 +492,6 @@ rnContext :: HsDocContext -> LHsContext RdrName -> RnM (LHsContext Name, FreeVar
 rnContext doc (L loc cxt) 
   = do { (cxt', fvs) <- rnLHsTypes doc cxt
        ; return (L loc cxt', fvs) }
-
-rnIPName :: IPName RdrName -> RnM (IPName Name)
-rnIPName n = newIPName (occNameFS (rdrNameOcc (ipNameName n)))
 \end{code}
 
 
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index 993bcebdb5..bbad59ec6e 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -519,7 +519,6 @@ hasEqualities givens = any (has_eq . evVarPred) givens
     
     -- See Note [Float Equalities out of Implications] in TcSimplify
     has_eq' (EqPred {})          = True
-    has_eq' (IPPred {})          = False 
     has_eq' (ClassPred cls _tys) = any has_eq (classSCTheta cls)
     has_eq' (TuplePred ts)       = any has_eq ts
     has_eq' (IrredPred _)        = True -- Might have equalities in it after reduction?
@@ -529,7 +528,6 @@ tyVarsOfCt :: Ct -> TcTyVarSet
 tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
 tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
 tyVarsOfCt (CDictCan { cc_tyargs = tys }) 	        = tyVarsOfTypes tys
-tyVarsOfCt (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
 tyVarsOfCt (CIrredEvCan { cc_ty = ty })                 = tyVarsOfType ty
 tyVarsOfCt (CNonCanonical { cc_ev = fl })           = tyVarsOfType (ctEvPred fl)
 
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index aa319c8b36..5eb8e150ef 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -45,6 +45,9 @@ import Util
 import BasicTypes
 import Outputable
 import FastString
+import Type(mkStrLitTy)
+import Class(classTyCon)
+import PrelNames(ipClassName)
 
 import Control.Monad
 
@@ -207,7 +210,9 @@ tcLocalBinds (HsValBinds (ValBindsOut binds sigs)) thing_inside
 tcLocalBinds (HsValBinds (ValBindsIn {})) _ = panic "tcLocalBinds"
 
 tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
-  = do  { (given_ips, ip_binds') <- mapAndUnzipM (wrapLocSndM tc_ip_bind) ip_binds
+  = do  { ipClass <- tcLookupClass ipClassName
+        ; (given_ips, ip_binds') <-
+            mapAndUnzipM (wrapLocSndM (tc_ip_bind ipClass)) ip_binds
 
         -- If the binding binds ?x = E, we  must now 
         -- discharge any ?x constraints in expr_lie
@@ -217,16 +222,28 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
 
         ; return (HsIPBinds (IPBinds ip_binds' ev_binds), result) }
   where
-    ips = [ip | L _ (IPBind ip _) <- ip_binds]
+    ips = [ip | L _ (IPBind (Left ip) _) <- ip_binds]
 
         -- I wonder if we should do these one at at time
         -- Consider     ?x = 4
         --              ?y = ?x + 1
-    tc_ip_bind (IPBind ip expr) 
+    tc_ip_bind ipClass (IPBind (Left ip) expr)
        = do { ty <- newFlexiTyVarTy openTypeKind
-            ; ip_id <- newIP ip ty
+            ; let p = mkStrLitTy $ hsIPNameFS ip
+            ; ip_id <- newDict ipClass [ p, ty ]
             ; expr' <- tcMonoExpr expr ty
-            ; return (ip_id, (IPBind (IPName ip_id) expr')) }
+            ; let d = toDict ipClass p ty `fmap` expr'
+            ; return (ip_id, (IPBind (Right ip_id) d)) }
+    tc_ip_bind _ (IPBind (Right {}) _) = panic "tc_ip_bind"
+
+    -- Coerces a `t` into a dictionry for `IP "x" t`.
+    -- co : t -> IP "x" t
+    toDict ipClass x ty =
+      case unwrapNewTyCon_maybe (classTyCon ipClass) of
+        Just (_,_,ax) -> HsWrap $ WpCast $ mkTcSymCo $ mkTcAxInstCo ax [x,ty]
+        Nothing       -> panic "The dictionary for `IP` is not a newtype?"
+
+
 \end{code}
 
 Note [Implicit parameter untouchables]
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 4beb6d2d9c..284d0218f5 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -14,7 +14,6 @@ module TcCanonical(
 
 #include "HsVersions.h"
 
-import BasicTypes ( IPName )
 import TcRnTypes
 import TcType
 import Type
@@ -23,7 +22,6 @@ import TcEvidence
 import Class
 import TyCon
 import TypeRep
-import Name ( Name )
 import Var
 import VarEnv
 import Outputable
@@ -199,11 +197,6 @@ canonicalize (CFunEqCan { cc_depth = d
   = {-# SCC "canEqLeafFunEqLeftRec" #-}
     canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
 
-canonicalize (CIPCan { cc_depth = d
-                     , cc_ev = fl
-                     , cc_ip_nm  = nm
-                     , cc_ip_ty  = xi })
-  = canIP d fl nm xi
 canonicalize (CIrredEvCan { cc_ev = fl
                           , cc_depth = d
                           , cc_ty = xi })
@@ -219,7 +212,6 @@ canEvVar d fl pred_classifier
   = case pred_classifier of
       ClassPred cls tys -> canClassNC d fl cls tys 
       EqPred ty1 ty2    -> canEqNC    d fl ty1 ty2 
-      IPPred nm ty      -> canIP      d fl nm ty
       IrredPred ev_ty   -> canIrred   d fl ev_ty
       TuplePred tys     -> canTuple   d fl tys
 \end{code}
@@ -248,43 +240,6 @@ canTuple d fl tys
 
 %************************************************************************
 %*                                                                      *
-%*                      Implicit Parameter Canonicalization
-%*                                                                      *
-%************************************************************************
-
-\begin{code}
-canIP :: SubGoalDepth -- Depth 
-      -> CtEvidence
-      -> IPName Name -> Type -> TcS StopOrContinue
--- Precondition: EvVar is implicit parameter evidence
-canIP d fl nm ty
-  =    -- Note [Canonical implicit parameter constraints] explains why it's 
-       -- possible in principle to not flatten, but since flattening applies 
-       -- the inert substitution we choose to flatten anyway.
-    do { (xi,co) <- flatten d FMFullFlatten fl (mkIPPred nm ty)
-       ; mb <- rewriteCtFlavor fl xi co 
-       ; case mb of
-            Just new_fl -> let IPPred _ xi_in = classifyPredType xi
-                           in continueWith $ CIPCan { cc_ev = new_fl
-                                                    , cc_ip_nm = nm, cc_ip_ty = xi_in
-                                                    , cc_depth = d }
-            Nothing -> return Stop }
-
-\end{code}
-
-Note [Canonical implicit parameter constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The type in a canonical implicit parameter constraint doesn't need to
-be a xi (type-function-free type) since we can defer the flattening
-until checking this type for equality with another type.  If we
-encounter two IP constraints with the same name, they MUST have the
-same type, and at that point we can generate a flattened equality
-constraint between the types.  (On the other hand, the types in two
-class constraints for the same class MAY be equal, so they need to be
-flattened in the first place to facilitate comparing them.)
-
-%************************************************************************
-%*                                                                      *
 %*                      Class Canonicalization
 %*                                                                      *
 %************************************************************************
@@ -441,7 +396,6 @@ is_improvement_pty ty = go (classifyPredType ty)
     go (EqPred {})         = True 
     go (ClassPred cls _tys) = not $ null fundeps
       where (_,fundeps) = classTvsFds cls
-    go (IPPred {})         = False
     go (TuplePred ts)      = any is_improvement_pty ts
     go (IrredPred {})      = True -- Might have equalities after reduction?
 \end{code}
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index c46d826e0a..ff774fa37b 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -255,9 +255,10 @@ tryReporters reporters deflt cts
 mkFlatErr :: ReportErrCtxt -> Ct -> TcM ErrMsg
 -- Context is already set
 mkFlatErr ctxt ct   -- The constraint is always wanted
+  | isIPPred (ctPred ct) = mkIPErr    ctxt [ct]
+  | otherwise
   = case classifyPredType (ctPred ct) of
       ClassPred {}  -> mkDictErr  ctxt [ct]
-      IPPred {}     -> mkIPErr    ctxt [ct]
       IrredPred {}  -> mkIrredErr ctxt [ct]
       EqPred {}     -> mkEqErr1 ctxt ct
       TuplePred {}  -> panic "mkFlat"
@@ -289,9 +290,10 @@ reportFlatErrs ctxt cts
     go [] dicts ips irreds
       = (dicts, ips, irreds)
     go (ct:cts) dicts ips irreds
+      | isIPPred (ctPred ct) = go cts dicts (ct:ips) irreds
+      | otherwise
       = case classifyPredType (ctPred ct) of
           ClassPred {}  -> go cts (ct:dicts) ips irreds
-          IPPred {}     -> go cts dicts (ct:ips) irreds
           IrredPred {}  -> go cts dicts ips (ct:irreds)
           _             -> panic "mkFlat"
     -- TuplePreds should have been expanded away by the constraint
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index c915b16c42..f3c238bd66 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -63,6 +63,7 @@ import ErrUtils
 import Outputable
 import FastString
 import Control.Monad
+import Class(classTyCon)
 \end{code}
 
 %************************************************************************
@@ -178,15 +179,23 @@ tcExpr (NegApp expr neg_expr) res_ty
 	; expr' <- tcMonoExpr expr res_ty
 	; return (NegApp expr' neg_expr') }
 
-tcExpr (HsIPVar ip) res_ty
-  = do	{ let origin = IPOccOrigin ip
-	 	-- Implicit parameters must have a *tau-type* not a 
-		-- type scheme.  We enforce this by creating a fresh
-		-- type variable as its type.  (Because res_ty may not
-		-- be a tau-type.)
-	; ip_ty <- newFlexiTyVarTy openTypeKind
-	; ip_var <- emitWanted origin (mkIPPred ip ip_ty)
-	; tcWrapResult (HsIPVar (IPName ip_var)) ip_ty res_ty }
+tcExpr (HsIPVar x) res_ty
+  = do { let origin = IPOccOrigin x
+       ; ipClass <- tcLookupClass ipClassName
+           {- Implicit parameters must have a *tau-type* not a.
+              type scheme.  We enforce this by creating a fresh
+              type variable as its type.  (Because res_ty may not
+              be a tau-type.) -}
+       ; ip_ty <- newFlexiTyVarTy openTypeKind
+       ; let ip_name = mkStrLitTy (hsIPNameFS x)
+       ; ip_var <- emitWanted origin (mkClassPred ipClass [ip_name, ip_ty])
+       ; tcWrapResult (fromDict ipClass ip_name ip_ty (HsVar ip_var)) ip_ty res_ty }
+  where
+  -- Coerces a dictionry for `IP "x" t` into `t`.
+  fromDict ipClass x ty =
+    case unwrapNewTyCon_maybe (classTyCon ipClass) of
+      Just (_,_,ax) -> HsWrap $ WpCast $ mkTcAxInstCo ax [x,ty]
+      Nothing       -> panic "The dictionary for `IP` is not a newtype?"
 
 tcExpr (HsLam match) res_ty
   = do	{ (co_fn, match') <- tcMatchLambda match res_ty
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index a026c4381c..aa444715b0 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -359,7 +359,7 @@ zonkLocalBinds env (HsValBinds vb@(ValBindsOut binds sigs))
 zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds))
   = mappM (wrapLocM zonk_ip_bind) binds	`thenM` \ new_binds ->
     let
-	env1 = extendIdZonkEnv env [ipNameName n | L _ (IPBind n _) <- new_binds]
+	env1 = extendIdZonkEnv env [ n | L _ (IPBind (Right n) _) <- new_binds]
     in
     zonkTcEvBinds env1 dict_binds 	`thenM` \ (env2, new_dict_binds) -> 
     returnM (env2, HsIPBinds (IPBinds new_binds new_dict_binds))
@@ -539,8 +539,8 @@ zonkLExpr  env expr  = wrapLocM (zonkExpr env) expr
 zonkExpr env (HsVar id)
   = returnM (HsVar (zonkIdOcc env id))
 
-zonkExpr env (HsIPVar id)
-  = returnM (HsIPVar (mapIPName (zonkIdOcc env) id))
+zonkExpr _ (HsIPVar id)
+  = returnM (HsIPVar id)
 
 zonkExpr env (HsLit (HsRat f ty))
   = zonkTcTypeToType env ty	   `thenM` \ new_ty  ->
@@ -862,8 +862,9 @@ zonkRecFields env (HsRecFields flds dd)
 	   ; return (fld { hsRecFieldId = new_id, hsRecFieldArg = new_expr }) }
 
 -------------------------------------------------------------------------
-mapIPNameTc :: (a -> TcM b) -> IPName a -> TcM (IPName b)
-mapIPNameTc f (IPName n) = f n  `thenM` \ r -> returnM (IPName r)
+mapIPNameTc :: (a -> TcM b) -> Either HsIPName a -> TcM (Either HsIPName b)
+mapIPNameTc _ (Left x)  = returnM (Left x)
+mapIPNameTc f (Right x) = f x  `thenM` \ r -> returnM (Right r)
 \end{code}
 
 
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 2a1f4f3540..7808c6b44c 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -76,6 +76,7 @@ import FastString
 import Util
 
 import Control.Monad ( unless, when, zipWithM )
+import PrelNames(ipClassName)
 \end{code}
 
 
@@ -422,7 +423,10 @@ tc_hs_type ipTy@(HsIParamTy n ty) exp_kind
   = do { ty' <- tc_lhs_type ty 
             (EK liftedTypeKind (ptext (sLit "The type argument of the implicit parameter had")))
        ; checkExpectedKind ipTy constraintKind exp_kind
-       ; return (mkIPPred n ty') }
+       ; ipClass <- tcLookupClass ipClassName
+       ; let n' = mkStrLitTy $ hsIPNameFS n
+       ; return (mkClassPred ipClass [n',ty'])
+       }
 
 tc_hs_type ty@(HsEqTy ty1 ty2) exp_kind 
   = do { (ty1', kind1) <- tc_infer_lhs_type ty1
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 9aa5730856..adff5ea182 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -29,7 +29,6 @@ import PrelNames (singIClassName)
 import Class
 import TyCon
 import Name
-import IParam
 
 import FunDeps
 
@@ -276,9 +275,6 @@ Case 1: In Rewriting Equalities (function rewriteEqLHS)
 Case 2: Functional Dependencies 
     Again, we should prefer, if possible, the inert variables on the RHS
 
-Case 3: IP improvement work
-    We must always rewrite so that the inert type is on the right. 
-
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem
@@ -378,14 +374,12 @@ kick_out_rewritable ct is@(IS { inert_cans =
                                    IC { inert_eqs    = eqmap
                                       , inert_eq_tvs = inscope
                                       , inert_dicts  = dictmap
-                                      , inert_ips    = ipmap
                                       , inert_funeqs = funeqmap
                                       , inert_irreds = irreds }
                               , inert_frozen = frozen })
   = ((kicked_out,eqmap), remaining)
   where
-    rest_out = fro_out `andCts` dicts_out 
-                   `andCts` ips_out `andCts` irs_out
+    rest_out = fro_out `andCts` dicts_out `andCts` irs_out
     kicked_out = WorkList { wl_eqs    = []
                           , wl_funeqs = bagToList feqs_out
                           , wl_rest   = bagToList rest_out }
@@ -394,7 +388,6 @@ kick_out_rewritable ct is@(IS { inert_cans =
                                      , inert_eq_tvs = inscope 
                                        -- keep the same, safe and cheap
                                      , inert_dicts = dicts_in
-                                     , inert_ips = ips_in
                                      , inert_funeqs = feqs_in
                                      , inert_irreds = irs_in }
                    , inert_frozen = fro_in } 
@@ -404,8 +397,6 @@ kick_out_rewritable ct is@(IS { inert_cans =
                 -- subsitution into account
     fl = cc_ev ct
     tv = cc_tyvar ct
-                               
-    (ips_out,   ips_in)     = partitionCCanMap rewritable ipmap
 
     (feqs_out,  feqs_in)    = partCtFamHeadMap rewritable funeqmap
     (dicts_out, dicts_in)   = partitionCCanMap rewritable dictmap
@@ -635,6 +626,8 @@ solveWithIdentity d wd tv xi
 *                                                                               *
 *********************************************************************************
 
+Note [
+
 Note [The Solver Invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We always add Givens first.  So you might think that the solver has
@@ -722,7 +715,7 @@ interactWithInertsStage wi
 doInteractWithInert :: Ct -> Ct -> TcS InteractResult
 -- Identical class constraints.
 doInteractWithInert
-  inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
+  inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 })
    workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 })
 
   | cls1 == cls2  
@@ -766,46 +759,6 @@ doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 })
   | ty1 `eqType` ty2
   = solveOneFromTheOther "Irred/Irred" ifl workItem
 
--- Two implicit parameter constraints.  If the names are the same,
--- but their types are not, we generate a wanted type equality 
--- that equates the type (this is "improvement").  
--- However, we don't actually need the coercion evidence,
--- so we just generate a fresh coercion variable that isn't used anywhere.
-doInteractWithInert (CIPCan { cc_ev = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) 
-           workItem@(CIPCan { cc_ev = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
-  | nm1 == nm2 && isGiven wfl && isGiven ifl
-  = 	-- See Note [Overriding implicit parameters]
-        -- Dump the inert item, override totally with the new one
-	-- Do not require type equality
-	-- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
-	--              we must *override* the outer one with the inner one
-    irInertConsumed "IP/IP (override inert)"
-
-  | nm1 == nm2 && ty1 `eqType` ty2 
-  = solveOneFromTheOther "IP/IP" ifl workItem 
-
-  | nm1 == nm2
-  =  	-- See Note [When improvement happens]
-    do { mb_eqv <- newWantedEvVar new_wloc (mkEqPred ty2 ty1)
-         -- co :: ty2 ~ ty1, see Note [Efficient orientation]
-       ; cv <- case mb_eqv of
-                 Fresh eqv  -> 
-                   do { updWorkListTcS $ extendWorkListEq $ 
-                        CNonCanonical { cc_ev = eqv
-                                      , cc_depth = cc_depth workItem }
-                      ; return (ctEvTerm eqv) }
-                 Cached eqv -> return eqv
-       ; case wfl of
-            Wanted { ctev_evar = ev_id } ->
-              let ip_co = mkTcTyConAppCo (ipTyCon nm1) [evTermCoercion cv]
-              in do { setEvBind ev_id $
-                      mkEvCast (ctEvTerm ifl) (mkTcSymCo ip_co)
-                    ; irWorkItemConsumed "IP/IP (solved by rewriting)" }
-            _ -> pprPanic "Unexpected IP constraint" (ppr workItem) }
-  where 
-    new_wloc | isGiven wfl = getWantedLoc ifl
-             | otherwise   = getWantedLoc wfl
-
 doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
                     wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
@@ -873,6 +826,65 @@ doInteractWithInert _ _ = irKeepGoing "NOP"
 
 \end{code}
 
+
+Note [Shadowing of Implicit Parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider the following example:
+
+f :: (?x :: Char) => Char
+f = let ?x = 'a' in ?x
+
+The "let ?x = ..." generates an implication constraint of the form:
+
+?x :: Char => ?x :: Char
+
+Furthermore, the signature for `f` also generates an implication
+constraint, so we end up with the following nested implication:
+
+?x :: Char => (?x :: Char => ?x :: Char)
+
+Note that the wanted (?x :: Char) constraint may be solved in
+two incompatible ways:  either by using the parameter from the
+signature, or by using the local definition.  Our intention is
+that the local definition should "shadow" the parameter of the
+signature, and we implement this as follows: when we add a new
+given implicit parameter to the inert set, it replaces any existing
+givens for the same implicit parameter.
+
+This works for the normal cases but it has an odd side effect
+in some pathological programs like this:
+
+-- This is accepted, the second parameter shadows
+f1 :: (?x :: Int, ?x :: Char) => Char
+f1 = ?x
+
+-- This is rejected, the second parameter shadows
+f2 :: (?x :: Int, ?x :: Char) => Int
+f2 = ?x
+
+Both of these are actually wrong:  when we try to use either one,
+we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
+which would lead to an error.
+
+I can think of two ways to fix this:
+
+  1. Simply disallow multiple constratits for the same implicit
+    parameter---this is never useful, and it can be detected completely
+    syntactically.
+
+  2. Move the shadowing machinery to the location where we nest
+     implications, and add some code here that will produce an
+     error if we get multiple givens for the same implicit parameter.
+
+
+
+
+
+
+
+
+
 Note [Cache-caused loops]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 7404acd58c..4e6f499db1 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -33,7 +33,7 @@ module TcMType (
   --------------------------------
   -- Creating new evidence variables
   newEvVar, newEvVars,
-  newEq, newIP, newDict,
+  newEq, newDict,
 
   newWantedEvVar, newWantedEvVars,
   newTcEvBinds, addTcEvBind,
@@ -85,7 +85,6 @@ import Var
 -- others:
 import HsSyn		-- HsType
 import TcRnMonad        -- TcType, amongst others
-import IParam
 import Id
 import FunDeps
 import Name
@@ -95,7 +94,6 @@ import DynFlags
 import Util
 import Maybes
 import ListSetOps
-import BasicTypes
 import SrcLoc
 import Outputable
 import FastString
@@ -156,11 +154,6 @@ newEq ty1 ty2
   = do { name <- newName (mkVarOccFS (fsLit "cobox"))
        ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
 
-newIP :: IPName Name -> TcType -> TcM IpId
-newIP ip ty
-  = do 	{ name <- newName (mkVarOccFS (ipFastString ip))
-        ; return (mkLocalId name (mkIPPred ip ty)) }
-
 newDict :: Class -> [TcType] -> TcM DictId
 newDict cls tys 
   = do { name <- newName (mkDictOcc (getOccName cls))
@@ -169,7 +162,6 @@ newDict cls tys
 predTypeOccName :: PredType -> OccName
 predTypeOccName ty = case classifyPredType ty of
     ClassPred cls _ -> mkDictOcc (getOccName cls)
-    IPPred ip _     -> mkVarOccFS (ipFastString ip)
     EqPred _ _      -> mkVarOccFS (fsLit "cobox")
     TuplePred _     -> mkVarOccFS (fsLit "tup")
     IrredPred _     -> mkVarOccFS (fsLit "irred")
@@ -1186,19 +1178,6 @@ check_pred_ty' dflags _ctxt (EqPred ty1 ty2)
        ; checkValidMonoType ty2
        }
 
-check_pred_ty' _ _ctxt (IPPred _ ty) = checkValidMonoType ty
-	-- Contrary to GHC 7.2 and below, we allow implicit parameters not only
-	-- in type signatures but also in instance decls, superclasses etc
-	-- The reason we didn't allow implicit params in instances is a bit
-	-- subtle:
-	-- If we allowed	instance (?x::Int, Eq a) => Foo [a] where ...
-	-- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
-	-- discharge all the potential usas of the ?x in e.   For example, a
-	-- constraint Foo [Int] might come out of e,and applying the
-	-- instance decl would show up two uses of ?x.
-        --
-        -- Happily this is not an issue in the new constraint solver.
-
 check_pred_ty' dflags ctxt t@(TuplePred ts)
   = do { checkTc (xopt Opt_ConstraintKinds dflags)
                  (predTupleErr (predTreePredType t))
@@ -1759,17 +1738,22 @@ sizeTypes xs = sum (map sizeType tys)
 
 -- Size of a predicate
 --
--- We are considering whether *class* constraints terminate
--- Once we get into an implicit parameter or equality we
--- can't get back to a class constraint, so it's safe
--- to say "size 0".  See Trac #4200.
+-- We are considering whether class constraints terminate.
+-- Equality constraints and constraints for the implicit
+-- parameter class always termiante so it is safe to say "size 0".
+-- (Implicit parameter constraints always terminate because
+-- there are no instances for them---they are only solved by
+-- "local instances" in expressions).
+-- See Trac #4200.
 sizePred :: PredType -> Int
-sizePred ty = go (classifyPredType ty)
+sizePred ty = goClass ty
   where
+    goClass p | isIPPred p = 0
+              | otherwise  = go (classifyPredType p)
+
     go (ClassPred _ tys') = sizeTypes tys'
-    go (IPPred {})        = 0
     go (EqPred {})        = 0
-    go (TuplePred ts)     = sum (map (go . classifyPredType) ts)
+    go (TuplePred ts)     = sum (map goClass ts)
     go (IrredPred ty)     = sizeType ty
 \end{code}
 
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 2c8d69e2f6..1ed3d0d198 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -53,7 +53,7 @@ module TcRnTypes(
        -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, keepWanted,
         singleCt, extendCts, isEmptyCts, isCTyEqCan, isCFunEqCan,
-        isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
+        isCDictCan_Maybe, isCFunEqCan_Maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt, 
         isGivenCt, 
         ctWantedLoc, ctEvidence,
@@ -847,19 +847,11 @@ data Ct
                        -- See Note [WorkList]
     }
 
-  | CIPCan {	-- ?x::tau
-      -- See note [Canonical implicit parameter constraints].
-      cc_ev :: CtEvidence,
-      cc_ip_nm  :: IPName Name,
-      cc_ip_ty  :: TcTauType,          -- Not a Xi! See same not as above
-      cc_depth  :: SubGoalDepth        -- See Note [WorkList]
-    }
-
   | CIrredEvCan {  -- These stand for yet-unknown predicates
       cc_ev :: CtEvidence,
       cc_ty     :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
                        -- Since, if it were a type constructor application, that'd make the
-                       -- whole constraint a CDictCan, CIPCan, or CTyEqCan. And it can't be
+                       -- whole constraint a CDictCan, or CTyEqCan. And it can't be
                        -- a type family application either because it's a Xi type.
       cc_depth :: SubGoalDepth -- See Note [WorkList]
     }
@@ -922,8 +914,6 @@ ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
   = mkTcEqPred (mkTyVarTy tv) xi
 ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 }) 
   = mkTcEqPred (mkTyConApp fn xis1) xi2
-ctPred (CIPCan { cc_ip_nm = nm, cc_ip_ty = xi }) 
-  = mkIPPred nm xi
 ctPred (CIrredEvCan { cc_ty = xi }) = xi
 -}
 \end{code}
@@ -960,10 +950,6 @@ isCDictCan_Maybe :: Ct -> Maybe Class
 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
 isCDictCan_Maybe _              = Nothing
 
-isCIPCan_Maybe :: Ct -> Maybe (IPName Name)
-isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
-isCIPCan_Maybe _                = Nothing
-
 isCIrredEvCan :: Ct -> Bool
 isCIrredEvCan (CIrredEvCan {}) = True
 isCIrredEvCan _                = False
@@ -990,7 +976,6 @@ instance Outputable Ct where
                            CFunEqCan {}     -> "CFunEqCan"
                            CNonCanonical {} -> "CNonCanonical"
                            CDictCan {}      -> "CDictCan"
-                           CIPCan {}        -> "CIPCan"
                            CIrredEvCan {}   -> "CIrredEvCan"
 \end{code}
 
@@ -1397,7 +1382,7 @@ data SkolemInfo
 
   | ArrowSkol 	  	-- An arrow form (see TcArrows)
 
-  | IPSkol [IPName Name]  -- Binding site of an implicit parameter
+  | IPSkol [HsIPName]   -- Binding site of an implicit parameter
 
   | RuleSkol RuleName	-- The LHS of a RULE
 
@@ -1465,7 +1450,7 @@ data CtOrigin
 
   | TypeEqOrigin EqOrigin
 
-  | IPOccOrigin  (IPName Name)	-- Occurrence of an implicit parameter
+  | IPOccOrigin  HsIPName 	-- Occurrence of an implicit parameter
 
   | LiteralOrigin (HsOverLit Name)	-- Occurrence of a literal
   | NegateOrigin			-- Occurrence of syntactic negation
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index c4ceaea050..f0c69c5819 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -73,7 +73,7 @@ module TcSMonad (
     CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
     PredMap, FamHeadMap,
     partCtFamHeadMap, lookupFamHead,
-
+    filterSolved,
 
     instDFunType,                              -- Instantiation
     newFlexiTcSTy, instFlexiTcS,
@@ -99,7 +99,6 @@ module TcSMonad (
 #include "HsVersions.h"
 
 import HscTypes
-import BasicTypes 
 
 import Inst
 import InstEnv 
@@ -399,6 +398,11 @@ partCtFamHeadMap f ctmap
                       = ty1 
                       | otherwise 
                       = panic "partCtFamHeadMap, encountered non equality!"
+
+filterSolved :: (CtEvidence -> Bool) -> PredMap CtEvidence -> PredMap CtEvidence
+filterSolved p (PredMap mp) = PredMap (foldTM upd mp emptyTM)
+  where upd a m = if p a then alterTM (ctEvPred a) (\_ -> Just a) m
+                         else m
 \end{code}
 
 %************************************************************************
@@ -423,10 +427,6 @@ data InertCans
               -- Dictionaries only, index is the class
               -- NB: index is /not/ the whole type because FD reactions 
               -- need to match the class but not necessarily the whole type.
-       , inert_ips :: CCanMap (IPName Name)
-              -- Implicit parameters, index is the name
-              -- NB: index is /not/ the whole type because IP reactions need 
-              -- to match the ip name but not necessarily the whole type.
        , inert_funeqs :: CtFamHeadMap
               -- Family equations, index is the whole family head type.
        , inert_irreds :: Cts       
@@ -525,7 +525,6 @@ data InertSet
 instance Outputable InertCans where 
   ppr ics = vcat [ vcat (map ppr (varEnvElts (inert_eqs ics)))
                  , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
-                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips ics))) 
                  , vcat (map ppr (Bag.bagToList $ 
                                   ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
                  , vcat (map ppr (Bag.bagToList $ inert_irreds ics))
@@ -545,7 +544,6 @@ emptyInert
   = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                          , inert_eq_tvs = emptyInScopeSet
                          , inert_dicts  = emptyCCanMap
-                         , inert_ips    = emptyCCanMap
                          , inert_funeqs = FamHeadMap emptyTM 
                          , inert_irreds = emptyCts }
        , inert_frozen        = emptyCts
@@ -592,9 +590,6 @@ updInertSet is item
                 
             in ics { inert_eqs = eqs', inert_eq_tvs = inscope' }
 
-          | Just x  <- isCIPCan_Maybe item      -- IP 
-          = ics { inert_ips   = updCCanMap (x,item) (inert_ips ics) }  
-            
           | isCIrredEvCan item                  -- Presently-irreducible evidence
           = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
 
@@ -683,7 +678,6 @@ extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
 extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
                                       , inert_eq_tvs = eq_tvs
                                       , inert_irreds = irreds
-                                      , inert_ips    = ips
                                       , inert_funeqs = funeqs
                                       , inert_dicts  = dicts
                                       }
@@ -696,7 +690,6 @@ extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
   = let is_solved  = IS { inert_cans = IC { inert_eqs    = solved_eqs
                                           , inert_eq_tvs = eq_tvs
                                           , inert_dicts  = solved_dicts
-                                          , inert_ips    = solved_ips
                                           , inert_irreds = solved_irreds
                                           , inert_funeqs = solved_funeqs }
                         , inert_frozen = emptyCts -- All out
@@ -715,12 +708,11 @@ extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
                        eqs `minusVarEnv` solved_eqs
 
         (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
-        (unsolved_ips, solved_ips)       = extractUnsolvedCMap ips
         (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap dicts
         (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
 
         unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
-                   unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
+                   unsolved_dicts `unionBags` unsolved_funeqs
 
 
 
@@ -749,9 +741,6 @@ extractRelevantInerts wi
                     Nothing -> (emptyCts, funeq_map)
                     Just ct -> (singleCt ct, new_funeq_map)
             in (cts, ics { inert_funeqs = FamHeadMap feqs_map })
-        extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics = 
-            let (cts, ips_map) = getRelevantCts nm (inert_ips ics) 
-            in (cts, ics { inert_ips = ips_map })
         extract_ics_relevants (CIrredEvCan { }) ics = 
             let cts = inert_irreds ics 
             in (cts, ics { inert_irreds = emptyCts })
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 34c40f2a63..39f7f4d72a 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -22,7 +22,7 @@ import TcSMonad
 import TcInteract 
 import Inst
 import Unify	( niFixTvSubst, niSubstTvSet )
-import Type     ( classifyPredType, PredTree(..) )
+import Type     ( classifyPredType, PredTree(..), isIPPred_maybe )
 import Var
 import Unique
 import VarSet
@@ -42,7 +42,7 @@ import Outputable
 import FastString
 import TrieMap () -- DV: for now
 import DynFlags
-
+import Data.Maybe ( mapMaybe )
 \end{code}
 
 
@@ -965,7 +965,8 @@ solveImplication tcs_untouchables
                  , ic_given  = givens
                  , ic_wanted = wanteds
                  , ic_loc    = loc })
-  = nestImplicTcS ev_binds (untch, tcs_untouchables) $
+  = shadowIPs givens $    -- See Note [Shadowing of Implicit Parameters]
+    nestImplicTcS ev_binds (untch, tcs_untouchables) $
     recoverTcS (return (emptyBag, emptyBag)) $
        -- Recover from nested failures.  Even the top level is
        -- just a bunch of implications, so failing at the first one is bad
@@ -1039,6 +1040,31 @@ floatEqualities skols can_given wantders
                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
           where
             inner_tvs = tvs_under_fsks ty
+
+shadowIPs :: [EvVar] -> TcS a -> TcS a
+shadowIPs gs m
+  | null shadowed = m
+  | otherwise     = do is <- getTcSInerts
+                       doWithInert (purgeShadowed is) m
+  where
+  shadowed  = mapMaybe isIP gs
+
+  isIP g    = do p <- evVarPred_maybe g
+                 (x,_) <- isIPPred_maybe p
+                 return x
+
+  isShadowedCt ct = isShadowedEv (ctEvidence ct)
+  isShadowedEv ev = case isIPPred_maybe (ctEvPred ev) of
+                      Just (x,_) -> x `elem` shadowed
+                      _          -> False
+
+  purgeShadowed is = is { inert_cans = purgeCans (inert_cans is)
+                        , inert_solved = purgeSolved (inert_solved is)
+                        }
+
+  purgeDicts    = snd . partitionCCanMap isShadowedCt
+  purgeCans ics = ics { inert_dicts = purgeDicts (inert_dicts ics) }
+  purgeSolved   = filterSolved (not . isShadowedEv)
 \end{code}
 
 Note [Preparing inert set for implications]
@@ -1241,6 +1267,39 @@ f (x::beta) =
         g2 z = case z of TEx y -> (h [[undefined]], op x [y])
     in (g1 '3', g2 undefined)
 
+Note [Shadowing of Implicit Parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following example:
+
+f :: (?x :: Char) => Char
+f = let ?x = 'a' in ?x
+
+The "let ?x = ..." generates an implication constraint of the form:
+
+?x :: Char => ?x :: Char
+
+
+Furthermore, the signature for `f` also generates an implication
+constraint, so we end up with the following nested implication:
+
+?x :: Char => (?x :: Char => ?x :: Char)
+
+Note that the wanted (?x :: Char) constraint may be solved in
+two incompatible ways:  either by using the parameter from the
+signature, or by using the local definition.  Our intention is
+that the local definition should "shadow" the parameter of the
+signature, and we implement this as follows: when we nest implications,
+we remove any implicit parameters in the outer implication, that
+have the same name as givens of the inner implication.
+
+Here is another variation of the example:
+
+f :: (?x :: Int) => Char
+f = let ?x = 'x' in ?x
+
+This program should also be accepted: the two constraints `?x :: Int`
+and `?x :: Char` never exist in the same context, so they don't get to
+interact to cause failure.
 \begin{code}
 
 solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs
index c02f885edf..fac61afe65 100644
--- a/compiler/typecheck/TcSplice.lhs
+++ b/compiler/typecheck/TcSplice.lhs
@@ -1424,10 +1424,14 @@ reify_tc_app tc tys
     removeKinds _ tys           = tys
 
 reifyPred :: TypeRep.PredType -> TcM TH.Pred
-reifyPred ty = case classifyPredType ty of
+reifyPred ty
+  -- We could reify the implicit paramter as a class but it seems
+  -- nicer to support them properly...
+  | isIPPred ty = noTH (sLit "implicit parameters") (ppr ty)
+  | otherwise
+   = case classifyPredType ty of
   ClassPred cls tys -> do { tys' <- reifyTypes tys 
                           ; return $ TH.ClassP (reifyName cls) tys' }
-  IPPred _ _        -> noTH (sLit "implicit parameters") (ppr ty)
   EqPred ty1 ty2    -> do { ty1' <- reifyType ty1
                           ; ty2' <- reifyType ty2
                           ; return $ TH.EqualP ty1' ty2'
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index effc30d946..5e050e5465 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -130,7 +130,7 @@ module TcType (
   mkTyVarTy, mkTyVarTys, mkTyConTy,
 
   isClassPred, isEqPred, isIPPred,
-  mkClassPred, mkIPPred,
+  mkClassPred,
   isDictLikeTy,
   tcSplitDFunTy, tcSplitDFunHead, 
   mkEqPred, 
@@ -1091,9 +1091,6 @@ shallowPredTypePredTree ev_ty
       () | tc `hasKey` eqTyConKey
          , let [_, ty1, ty2] = tys
          -> EqPred ty1 ty2
-      () | Just ip <- tyConIP_maybe tc
-         , let [ty] = tys
-         -> IPPred ip ty
       () | isTupleTyCon tc
          -> TuplePred tys
       _ -> IrredPred ev_ty
diff --git a/compiler/types/IParam.lhs b/compiler/types/IParam.lhs
deleted file mode 100644
index 67d46c3a82..0000000000
--- a/compiler/types/IParam.lhs
+++ /dev/null
@@ -1,41 +0,0 @@
-%
-% (c) The University of Glasgow 2006
-% (c) The GRASP/AQUA Project, Glasgow University, 1998
-%
-
-\begin{code}
-module IParam (
-        ipFastString, ipTyConName, ipTyCon, ipCoAxiom
-    ) where
-
-#include "HsVersions.h"
-
-import Name
-import TyCon    (CoAxiom, TyCon, newTyConCo_maybe)
-import Type
-
-import BasicTypes (IPName(..), ipNameName)
-import FastString
-import Outputable
-\end{code}
-
-\begin{code}
-ipFastString :: IPName Name -> FastString
-ipFastString = occNameFS . nameOccName . ipTyConName
-
-ipTyConName :: IPName Name -> Name
-ipTyConName = ipNameName
-
-ipTyCon :: IPName Name -> TyCon
-ipTyCon ip = case wiredInNameTyThing_maybe (ipTyConName ip) of
-    Just (ATyCon tc) -> tc
-    _                -> pprPanic "ipTyCon" (ppr ip)
-
-ipCoAxiom :: IPName Name -> CoAxiom
-ipCoAxiom ip = case newTyConCo_maybe (ipTyCon ip) of
-    Just ax -> ax
-    _       -> pprPanic "ipCoAxiom" (ppr ip)
-
--- The IParam DataCon never gets any code generated for it, so it's
--- a bit dangerous to actually make use of it, hence no ipDataCon function
-\end{code}
diff --git a/compiler/types/IParam.lhs-boot b/compiler/types/IParam.lhs-boot
deleted file mode 100644
index 34acf1a5da..0000000000
--- a/compiler/types/IParam.lhs-boot
+++ /dev/null
@@ -1,10 +0,0 @@
-\begin{code}
-module IParam where
-
-import Name
-import BasicTypes
-import {-# SOURCE #-} TyCon (TyCon)
-
-ipTyConName :: IPName Name -> Name
-ipTyCon :: IPName Name -> TyCon
-\end{code}
\ No newline at end of file
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 47db814476..c12947911b 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -64,7 +64,7 @@ module TyCon(
         tyConStupidTheta,
         tyConArity,
         tyConParent,
-        tyConTuple_maybe, tyConClass_maybe, tyConIP_maybe,
+        tyConTuple_maybe, tyConClass_maybe,
         tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
         synTyConDefn, synTyConRhs, synTyConType,
         tyConExtName,           -- External name for foreign types
@@ -89,7 +89,6 @@ module TyCon(
 
 import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
 import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
-import {-# SOURCE #-} IParam  ( ipTyConName )
 
 import Var
 import Class
@@ -514,10 +513,6 @@ data TyConParent
   | ClassTyCon
         Class           -- INVARIANT: the classTyCon of this Class is the current tycon
 
-  -- | Associated type of a implicit parameter.
-  | IPTyCon
-        (IPName Name)
-
   -- | An *associated* type of a class.
   | AssocFamilyTyCon
         Class           -- The class in whose declaration the family is declared
@@ -555,7 +550,6 @@ data TyConParent
 instance Outputable TyConParent where
     ppr NoParentTyCon           = text "No parent"
     ppr (ClassTyCon cls)        = text "Class parent" <+> ppr cls
-    ppr (IPTyCon n)             = text "IP parent" <+> ppr n
     ppr (AssocFamilyTyCon cls)  = text "Class parent (assoc. family)" <+> ppr cls
     ppr (FamInstTyCon _ tc tys) = text "Family parent (family instance)" <+> ppr tc <+> sep (map ppr tys)
 
@@ -564,7 +558,6 @@ okParent :: Name -> TyConParent -> Bool
 okParent _       NoParentTyCon               = True
 okParent tc_name (AssocFamilyTyCon cls)      = tc_name `elem` map tyConName (classATs cls)
 okParent tc_name (ClassTyCon cls)            = tc_name == tyConName (classTyCon cls)
-okParent tc_name (IPTyCon ip)                = tc_name == ipTyConName ip
 okParent _       (FamInstTyCon _ fam_tc tys) = tyConArity fam_tc == length tys
 
 isNoParent :: TyConParent -> Bool
@@ -1409,12 +1402,6 @@ tyConTuple_maybe :: TyCon -> Maybe TupleSort
 tyConTuple_maybe (TupleTyCon {tyConTupleSort = sort}) = Just sort
 tyConTuple_maybe _                                    = Nothing
 
--- | If this 'TyCon' is that for implicit parameter, return the IP it is for.
--- Otherwise returns @Nothing@
-tyConIP_maybe :: TyCon -> Maybe (IPName Name)
-tyConIP_maybe (AlgTyCon {algTcParent = IPTyCon ip}) = Just ip
-tyConIP_maybe _                                     = Nothing
-
 ----------------------------------------------------------------------------
 tyConParent :: TyCon -> TyConParent
 tyConParent (AlgTyCon {algTcParent = parent}) = parent
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 4726f26213..1099303e48 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -53,14 +53,12 @@ module Type (
 	isDictLikeTy,
         mkEqPred, mkPrimEqPred,
         mkClassPred,
-	mkIPPred,
-        noParenPred, isClassPred, isEqPred, isIPPred,
+        noParenPred, isClassPred, isEqPred, isIPPred, isIPPred_maybe,
         
         -- Deconstructing predicate types
         PredTree(..), predTreePredType, classifyPredType,
         getClassPredTys, getClassPredTys_maybe,
         getEqPredTys, getEqPredTys_maybe,
-        getIPPredTy_maybe,
 
 	-- ** Common type constructors
         funTyCon,
@@ -153,13 +151,11 @@ import Class
 import TyCon
 import TysPrim
 import {-# SOURCE #-} TysWiredIn ( eqTyCon, mkBoxedTupleTy )
-import PrelNames	         ( eqTyConKey )
+import PrelNames	         ( eqTyConKey, ipClassName )
 
 -- others
-import {-# SOURCE #-} IParam ( ipTyCon )
 import Unique		( Unique, hasKey )
-import BasicTypes	( Arity, RepArity, IPName(..) )
-import Name		( Name )
+import BasicTypes	( Arity, RepArity )
 import NameSet
 import StaticFlags
 import Util
@@ -169,6 +165,7 @@ import FastString
 import Data.List        ( partition )
 import Maybes		( orElse )
 import Data.Maybe	( isJust )
+import Control.Monad    ( guard )
 
 infixr 3 `mkFunTy`	-- Associates to the right
 \end{code}
@@ -840,7 +837,7 @@ noParenPred :: PredType -> Bool
 --       C a => a -> a
 --       a~b => a -> b
 -- But   (?x::Int) => Int -> Int
-noParenPred p = isClassPred p || isEqPred p
+noParenPred p = not (isIPPred p) && isClassPred p || isEqPred p
 
 isPredTy :: Type -> Bool
 isPredTy ty
@@ -857,9 +854,17 @@ isClassPred ty = case tyConAppTyCon_maybe ty of
 isEqPred ty = case tyConAppTyCon_maybe ty of
     Just tyCon -> tyCon `hasKey` eqTyConKey
     _          -> False
+
 isIPPred ty = case tyConAppTyCon_maybe ty of
-    Just tyCon | Just _ <- tyConIP_maybe tyCon -> True
-    _                                          -> False
+    Just tyCon -> tyConName tyCon == ipClassName
+    _          -> False
+
+isIPPred_maybe :: Type -> Maybe (FastString, Type)
+isIPPred_maybe ty =
+  do (tc,[t1,t2]) <- splitTyConApp_maybe ty
+     guard (tyConName tc == ipClassName)
+     x <- isStrLitTy t1
+     return (x,t2)
 \end{code}
 
 Make PredTypes
@@ -882,13 +887,6 @@ mkPrimEqPred ty1  ty2
     k = typeKind ty1
 \end{code}
 
---------------------- Implicit parameters ---------------------------------
-
-\begin{code}
-mkIPPred :: IPName Name -> Type -> PredType
-mkIPPred ip ty = TyConApp (ipTyCon ip) [ty]
-\end{code}
-
 --------------------- Dictionary types ---------------------------------
 \begin{code}
 mkClassPred :: Class -> [Type] -> PredType
@@ -941,14 +939,12 @@ Decomposing PredType
 \begin{code}
 data PredTree = ClassPred Class [Type]
               | EqPred Type Type
-              | IPPred (IPName Name) Type
               | TuplePred [PredType]
               | IrredPred PredType
 
 predTreePredType :: PredTree -> PredType
 predTreePredType (ClassPred clas tys) = mkClassPred clas tys
 predTreePredType (EqPred ty1 ty2)     = mkEqPred ty1 ty2
-predTreePredType (IPPred ip ty)       = mkIPPred ip ty
 predTreePredType (TuplePred tys)      = mkBoxedTupleTy tys
 predTreePredType (IrredPred ty)       = ty
 
@@ -959,9 +955,6 @@ classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
     Just (tc, tys) | tc `hasKey` eqTyConKey
                    , let [_, ty1, ty2] = tys
                    -> EqPred ty1 ty2
-    Just (tc, tys) | Just ip <- tyConIP_maybe tc
-                   , let [ty] = tys
-                   -> IPPred ip ty
     Just (tc, tys) | isTupleTyCon tc
                    -> TuplePred tys
     _ -> IrredPred ev_ty
@@ -990,11 +983,6 @@ getEqPredTys_maybe ty
   = case splitTyConApp_maybe ty of 
       Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
       _ -> Nothing
-
-getIPPredTy_maybe :: PredType -> Maybe (IPName Name, Type)
-getIPPredTy_maybe ty = case splitTyConApp_maybe ty of 
-        Just (tc, [ty1]) | Just ip <- tyConIP_maybe tc -> Just (ip, ty1)
-        _ -> Nothing
 \end{code}
 
 %************************************************************************
diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index 3605851101..327ac78d71 100644
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -551,17 +551,18 @@ instance Outputable Type where
 instance Outputable TyLit where
    ppr = pprTyLit
 
-instance Outputable name => OutputableBndr (IPName name) where
-    pprBndr _ n   = ppr n	-- Simple for now
-    pprInfixOcc  n = ppr n 
-    pprPrefixOcc n = ppr n 
-
 ------------------
 	-- OK, here's the main printer
 
 ppr_type :: Prec -> Type -> SDoc
 ppr_type _ (TyVarTy tv)	      = ppr_tvar tv
+
+ppr_type _ (TyConApp tc [LitTy (StrTyLit n),ty])
+  | tc `hasKey` ipClassNameKey
+  = char '?' <> ftext n <> ptext (sLit "::") <> ppr_type TopPrec ty
+
 ppr_type p (TyConApp tc tys)  = pprTcApp p ppr_type tc tys
+
 ppr_type p (LitTy l)          = ppr_tylit p l
 ppr_type p ty@(ForAllTy {})   = ppr_forall_type p ty
 
@@ -661,7 +662,6 @@ pprTcApp _ _ tc []      -- No brackets for SymOcc
 pprTcApp _ pp tc [ty]
   | tc `hasKey` listTyConKey   = pprPromotionQuote tc <> brackets   (pp TopPrec ty)
   | tc `hasKey` parrTyConKey   = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
-  | Just n <- tyConIP_maybe tc = ppr n <> ptext (sLit "::") <> pp TopPrec ty
 
 pprTcApp p pp tc tys
   | isTupleTyCon tc && tyConArity tc == length tys