merge upstream HEAD
[ghc-hetmet.git] / compiler / types / TypeRep.lhs
index b0b5c63..1be55d7 100644 (file)
@@ -1,27 +1,34 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1998
 %
 \section[TypeRep]{Type - friends' interface}
 
 \begin{code}
+-- We expose the relevant stuff from this module via the Type module
+{-# OPTIONS_HADDOCK hide #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
 module TypeRep (
        TyThing(..), 
-       Type(..), TyNote(..),           -- Representation visible 
+       Type(..),
        PredType(..),                   -- to friends
        
        Kind, ThetaType,                -- Synonyms
 
-       funTyCon,
+       funTyCon, funTyConName,
 
        -- Pretty-printing
-       pprType, pprParendType, pprTyThingCategory,
-       pprPred, pprTheta, pprThetaArrow, pprClassPred,
+       pprType, pprParendType, pprTypeApp,
+       pprTyThing, pprTyThingCategory, 
+       pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
 
        -- Kinds
        liftedTypeKind, unliftedTypeKind, openTypeKind,
         argTypeKind, ubxTupleKind,
        isLiftedTypeKindCon, isLiftedTypeKind,
-       mkArrowKind, mkArrowKinds,
+       mkArrowKind, mkArrowKinds, isCoercionKind,
+       coVarPred,
 
         -- Kind constructors...
         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
@@ -37,83 +44,28 @@ module TypeRep (
         isTySuperKind, isCoSuperKind,
        tySuperKindTyCon, coSuperKindTyCon,
         
-        isCoercionKindTyCon,
-
        pprKind, pprParendKind
     ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-} DataCon( DataCon, dataConName )
-import Monad     ( guard )
--- friends:
 
-import Var       ( Var, Id, TyVar, tyVarKind )
-import VarSet     ( TyVarSet )
-import Name      ( Name, NamedThing(..), BuiltInSyntax(..), mkWiredInName )
-import OccName   ( mkOccNameFS, tcName, parenSymOcc )
-import BasicTypes ( IPName, tupleParens )
-import TyCon     ( TyCon, mkFunTyCon, tyConArity, tupleTyConBoxity, isTupleTyCon, isRecursiveTyCon, isNewTyCon, mkVoidPrimTyCon, mkSuperKindTyCon, isSuperKindTyCon, mkCoercionTyCon )
-import Class     ( Class )
+-- friends:
+import Var
+import Name
+import BasicTypes
+import TyCon
+import Class
 
 -- others
-import PrelNames  ( gHC_PRIM, funTyConKey, tySuperKindTyConKey, 
-                    coSuperKindTyConKey, liftedTypeKindTyConKey,
-                    openTypeKindTyConKey, unliftedTypeKindTyConKey,
-                    ubxTupleKindTyConKey, argTypeKindTyConKey, listTyConKey, 
-                    parrTyConKey, hasKey, eqCoercionKindTyConKey )
+import PrelNames
 import Outputable
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-\subsection{Type Classifications}
-%*                                                                     *
-%************************************************************************
-
-A type is
-
-       *unboxed*       iff its representation is other than a pointer
-                       Unboxed types are also unlifted.
-
-       *lifted*        A type is lifted iff it has bottom as an element.
-                       Closures always have lifted types:  i.e. any
-                       let-bound identifier in Core must have a lifted
-                       type.  Operationally, a lifted object is one that
-                       can be entered.
-
-                       Only lifted types may be unified with a type variable.
-
-       *algebraic*     A type with one or more constructors, whether declared
-                       with "data" or "newtype".   
-                       An algebraic type is one that can be deconstructed
-                       with a case expression.  
-                       *NOT* the same as lifted types,  because we also 
-                       include unboxed tuples in this classification.
-
-       *data*          A type declared with "data".  Also boxed tuples.
-
-       *primitive*     iff it is a built-in type that can't be expressed
-                       in Haskell.
-
-Currently, all primitive types are unlifted, but that's not necessarily
-the case.  (E.g. Int could be primitive.)
-
-Some primitive types are unboxed, such as Int#, whereas some are boxed
-but unlifted (such as ByteArray#).  The only primitive types that we
-classify as algebraic are the unboxed tuples.
-
-examples of type classifications:
-
-Type           primitive       boxed           lifted          algebraic    
------------------------------------------------------------------------------
-Int#,          Yes             No              No              No
-ByteArray#     Yes             Yes             No              No
-(# a, b #)     Yes             No              No              Yes
-(  a, b  )     No              Yes             Yes             Yes
-[a]            No              Yes             Yes             Yes
-
+import FastString
 
+-- libraries
+import Data.Data hiding ( TyCon )
+\end{code}
 
        ----------------------
        A note about newtypes
@@ -166,84 +118,92 @@ to cut all loops.  The other members of the loop may be marked 'non-recursive'.
 
 
 \begin{code}
+-- | The key representation of types within the compiler
 data Type
-  = TyVarTy TyVar      
+  = TyVarTy TyVar      -- ^ Vanilla type variable
 
   | AppTy
-       Type            -- Function is *not* a TyConApp
-       Type            -- It must be another AppTy, or TyVarTy
-                       -- (or NoteTy of these)
-
-  | TyConApp           -- Application of a TyCon, including newtypes *and* synonyms
-       TyCon           --  *Invariant* saturated appliations of FunTyCon and
-                       --      synonyms have their own constructors, below.
-                       -- However, *unsaturated* FunTyCons do appear as TyConApps.  
-                       -- 
-       [Type]          -- Might not be saturated.
-                       -- Even type synonyms are not necessarily saturated;
-                       -- for example unsaturated type synonyms can appear as the 
-                       -- RHS of a type synonym.
-
-  | FunTy              -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
        Type
+       Type            -- ^ Type application to something other than a 'TyCon'. Parameters:
+                       --
+                       --  1) Function: must /not/ be a 'TyConApp', must be another 'AppTy', or 'TyVarTy'
+                       --
+                       --  2) Argument type
+
+  | TyConApp
+       TyCon
+       [Type]          -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
+                       -- Invariant: saturated appliations of 'FunTyCon' must
+                       -- use 'FunTy' and saturated synonyms must use their own
+                       -- constructors. However, /unsaturated/ 'FunTyCon's do appear as 'TyConApp's.
+                       -- Parameters:
+                       --
+                       -- 1) Type constructor being applied to.
+                       --
+                       -- 2) Type arguments. Might not have enough type arguments here to saturate the constructor.
+                       -- Even type synonyms are not necessarily saturated; for example unsaturated type synonyms
+                       -- can appear as the right hand side of a type synonym.
+
+  | FunTy
        Type
+       Type            -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
 
-  | ForAllTy           -- A polymorphic type
+  | ForAllTy
        TyVar
-       Type    
-
-  | PredTy             -- The type of evidence for a type predictate
-       PredType        -- Can be expanded to a representation type.
-       -- NB: A PredTy (EqPred _ _) can appear only as the kind
-       --     of a coercion variable; never as the argument or result
-       --     of a FunTy (unlike ClassP, IParam)
-
-  | NoteTy             -- A type with a note attached
-       TyNote
-       Type            -- The expanded version
-
-type Kind = Type       -- Invariant: a kind is always
-                       --      FunTy k1 k2
-                       -- or   TyConApp PrimTyCon [...]
-                       -- or   TyVar kv (during inference only)
-                       -- or   ForAll ... (for top-level coercions)
-
-type SuperKind = Type   -- Invariant: a super kind is always 
-                        --   TyConApp SuperKindTyCon ...
-
-type Coercion = Type
-
-type CoercionKind = Kind
-
-data TyNote = FTVNote TyVarSet -- The free type variables of the noted expression
+       Type            -- ^ A polymorphic type
+
+  | PredTy
+       PredType        -- ^ The type of evidence for a type predictate.
+                        -- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
+                       -- of a coercion variable; never as the argument or result
+                       -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
+                       
+                       -- See Note [PredTy], and Note [Equality predicates]
+  deriving (Data, Typeable)
+
+-- | The key type representing kinds in the compiler.
+-- Invariant: a kind is always in one of these forms:
+--
+-- > FunTy k1 k2
+-- > TyConApp PrimTyCon [...]
+-- > TyVar kv   -- (during inference only)
+-- > ForAll ... -- (for top-level coercions)
+type Kind = Type
+
+-- | "Super kinds", used to help encode 'Kind's as types.
+-- Invariant: a super kind is always of this form:
+--
+-- > TyConApp SuperKindTyCon ...
+type SuperKind = Type
 \end{code}
 
 -------------------------------------
-               Source types
-
-A type of the form
-       PredTy p
-represents a value whose type is the Haskell predicate p, 
-where a predicate is what occurs before the '=>' in a Haskell type.
-It can be expanded into its representation, but: 
-
-       * The type checker must treat it as opaque
-       * The rest of the compiler treats it as transparent
-
-Consider these examples:
-       f :: (Eq a) => a -> Int
-       g :: (?x :: Int -> Int) => a -> Int
-       h :: (r\l) => {r} => {l::Int | r}
-
-Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
-Predicates are represented inside GHC by PredType:
+               Note [PredTy]
 
 \begin{code}
+-- | A type of the form @PredTy p@ represents a value whose type is
+-- the Haskell predicate @p@, where a predicate is what occurs before 
+-- the @=>@ in a Haskell type.
+-- It can be expanded into its representation, but: 
+--
+-- * The type checker must treat it as opaque
+--
+-- * The rest of the compiler treats it as transparent
+--
+-- Consider these examples:
+--
+-- > f :: (Eq a) => a -> Int
+-- > g :: (?x :: Int -> Int) => a -> Int
+-- > h :: (r\l) => {r} => {l::Int | r}
+--
+-- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
 data PredType 
-  = ClassP Class [Type]                -- Class predicate
-  | IParam (IPName Name) Type  -- Implicit parameter
-  | EqPred Type Type           -- Equality predicate (ty1 :=: ty2)
+  = ClassP Class [Type]                -- ^ Class predicate e.g. @Eq a@
+  | IParam (IPName Name) Type  -- ^ Implicit parameter e.g. @?x :: Int@
+  | EqPred Type Type           -- ^ Equality predicate e.g @ty1 ~ ty2@
+  deriving (Data, Typeable)
 
+-- | A collection of 'PredType's
 type ThetaType = [PredType]
 \end{code}
 
@@ -259,6 +219,24 @@ The predicate really does turn into a real extra argument to the
 function.  If the argument has type (PredTy p) then the predicate p is
 represented by evidence (a dictionary, for example, of type (predRepTy p).
 
+Note [Equality predicates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+       forall a b. (a ~ S b) => a -> b
+could be represented by
+       ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
+OR
+       ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
+
+The latter is what we do.  (Unlike for class and implicit parameter
+constraints, which do use FunTy.)
+
+Reason:
+       * FunTy is always a *value* function
+       * ForAllTy is discarded at runtime
+
+We often need to make a "wildcard" (c::PredTy..).  We always use the same
+name (wildCoVarName), since it's not mentioned.
+
 
 %************************************************************************
 %*                                                                     *
@@ -271,19 +249,23 @@ this module seems the right place for TyThing, because it's needed for
 funTyCon and all the types in TysPrim.
 
 \begin{code}
+-- | A typecheckable-thing, essentially anything that has a name
 data TyThing = AnId     Id
             | ADataCon DataCon
             | ATyCon   TyCon
             | AClass   Class
 
-instance Outputable TyThing where
-  ppr thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
+instance Outputable TyThing where 
+  ppr = pprTyThing
+
+pprTyThing :: TyThing -> SDoc
+pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
 
 pprTyThingCategory :: TyThing -> SDoc
-pprTyThingCategory (ATyCon _)  = ptext SLIT("Type constructor")
-pprTyThingCategory (AClass _)   = ptext SLIT("Class")
-pprTyThingCategory (AnId   _)   = ptext SLIT("Identifier")
-pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
+pprTyThingCategory (ATyCon _)  = ptext (sLit "Type constructor")
+pprTyThingCategory (AClass _)   = ptext (sLit "Class")
+pprTyThingCategory (AnId   _)   = ptext (sLit "Identifier")
+pprTyThingCategory (ADataCon _) = ptext (sLit "Data constructor")
 
 instance NamedThing TyThing where      -- Can't put this with the type
   getName (AnId id)     = getName id   -- decl, because the DataCon instance
@@ -305,6 +287,16 @@ We define a few wired-in type constructors here to avoid module knots
 --------------------------
 -- First the TyCons...
 
+-- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
+funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
+      openTypeKindTyCon, unliftedTypeKindTyCon,
+      ubxTupleKindTyCon, argTypeKindTyCon
+   :: TyCon
+funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
+      openTypeKindTyConName, unliftedTypeKindTyConName,
+      ubxTupleKindTyConName, argTypeKindTyConName
+   :: Name
+
 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
        -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
        -- But if we do that we get kind errors when saying
@@ -318,36 +310,27 @@ funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] lif
 tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
 coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
 
-liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
-openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
-unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
-ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName
-argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName
-eqCoercionKindTyCon = 
-  mkCoercionTyCon eqCoercionKindTyConName 2 (\ _ -> coSuperKind)
-
-mkKindTyCon :: Name -> TyCon
-mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
+liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName   tySuperKind
+openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName     tySuperKind
+unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
+ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName     tySuperKind
+argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName      tySuperKind
 
 --------------------------
 -- ... and now their names
 
-tySuperKindTyConName      = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
-coSuperKindTyConName      = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
-liftedTypeKindTyConName   = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
-openTypeKindTyConName     = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
-unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
-ubxTupleKindTyConName     = mkPrimTyConName FSLIT("(##)") ubxTupleKindTyConKey ubxTupleKindTyCon
-argTypeKindTyConName      = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
-funTyConName              = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
-
-eqCoercionKindTyConName   = mkWiredInName gHC_PRIM (mkOccNameFS tcName (FSLIT(":=:"))) 
-                                       eqCoercionKindTyConKey Nothing (ATyCon eqCoercionKindTyCon) 
-                                       BuiltInSyntax
-mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ) 
+tySuperKindTyConName      = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
+coSuperKindTyConName      = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
+liftedTypeKindTyConName   = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
+openTypeKindTyConName     = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
+unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
+ubxTupleKindTyConName     = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
+argTypeKindTyConName      = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
+funTyConName              = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
+
+mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
+mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ) 
                                              key 
-                                             Nothing           -- No parent object
                                              (ATyCon tycon)
                                              BuiltInSyntax
        -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
@@ -359,15 +342,20 @@ mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 kindTyConType :: TyCon -> Type
 kindTyConType kind = TyConApp kind []
 
+-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
+liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
+
 liftedTypeKind   = kindTyConType liftedTypeKindTyCon
 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
 openTypeKind     = kindTyConType openTypeKindTyCon
 argTypeKind      = kindTyConType argTypeKindTyCon
 ubxTupleKind    = kindTyConType ubxTupleKindTyCon
 
+-- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
 mkArrowKind :: Kind -> Kind -> Kind
 mkArrowKind k1 k2 = FunTy k1 k2
 
+-- | Iterated application of 'mkArrowKind'
 mkArrowKinds :: [Kind] -> Kind -> Kind
 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 
@@ -375,26 +363,37 @@ tySuperKind, coSuperKind :: SuperKind
 tySuperKind = kindTyConType tySuperKindTyCon 
 coSuperKind = kindTyConType coSuperKindTyCon 
 
-isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
+isTySuperKind :: SuperKind -> Bool
 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
-isTySuperKind other            = False
+isTySuperKind _                = False
 
-isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
+isCoSuperKind :: SuperKind -> Bool
 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
-isCoSuperKind other            = False
-
-isCoercionKindTyCon kc = kc `hasKey` eqCoercionKindTyConKey
-
+isCoSuperKind _                = False
 
 -------------------
--- lastly we need a few functions on Kinds
+-- Lastly we need a few functions on Kinds
 
+isLiftedTypeKindCon :: TyCon -> Bool
 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
 
+isLiftedTypeKind :: Kind -> Bool
 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
-isLiftedTypeKind other            = False
-
-
+isLiftedTypeKind _                = False
+
+isCoercionKind :: Kind -> Bool
+-- All coercions are of form (ty1 ~ ty2)
+-- This function is here rather than in Coercion, 
+-- because it's used in a knot-tied way to enforce invariants in Var
+isCoercionKind (PredTy (EqPred {})) = True
+isCoercionKind _                    = False
+
+coVarPred :: CoVar -> PredType
+coVarPred tv
+  = ASSERT( isCoVar tv )
+    case tyVarKind tv of
+       PredTy eq -> eq
+       other     -> pprPanic "coVarPred" (ppr tv $$ ppr other)
 \end{code}
 
 
@@ -426,23 +425,47 @@ pprType, pprParendType :: Type -> SDoc
 pprType       ty = ppr_type TopPrec   ty
 pprParendType ty = ppr_type TyConPrec ty
 
+pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
+-- The first arg is the tycon, or sometimes class
+-- Print infix if the tycon/class looks like an operator
+pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
+
 ------------------
 pprPred :: PredType -> SDoc
 pprPred (ClassP cls tys) = pprClassPred cls tys
 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
-pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
+pprPred (EqPred ty1 ty2) = pprEqPred (ty1,ty2)
+
+pprEqPred :: (Type,Type) -> SDoc
+pprEqPred (ty1,ty2) = sep [ ppr_type FunPrec ty1
+                          , nest 2 (ptext (sLit "~"))
+                          , ppr_type FunPrec ty2]
+                              -- Precedence looks like (->) so that we get
+                              --    Maybe a ~ Bool
+                              --    (a->a) ~ Bool
+                              -- Note parens on the latter!
 
 pprClassPred :: Class -> [Type] -> SDoc
-pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas) 
-                       <+> sep (map pprParendType tys)
+pprClassPred clas tys = ppr_type_app TopPrec (getName clas) tys
 
 pprTheta :: ThetaType -> SDoc
-pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
+-- pprTheta [pred] = pprPred pred       -- I'm in two minds about this
+pprTheta theta  = parens (sep (punctuate comma (map pprPred theta)))
 
 pprThetaArrow :: ThetaType -> SDoc
-pprThetaArrow theta 
-  | null theta = empty
-  | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
+pprThetaArrow []     = empty
+pprThetaArrow [pred] 
+  | noParenPred pred = pprPred pred <+> darrow
+pprThetaArrow preds  = parens (sep (punctuate comma (map pprPred preds))) <+> darrow
+
+noParenPred :: PredType -> Bool
+-- A predicate that can appear without parens before a "=>"
+--       C a => a -> a
+--       a~b => a -> b
+-- But   (?x::Int) => Int -> Int
+noParenPred (ClassP {}) = True
+noParenPred (EqPred {}) = True
+noParenPred (IParam {}) = False
 
 ------------------
 instance Outputable Type where
@@ -457,13 +480,14 @@ instance Outputable name => OutputableBndr (IPName name) where
 ------------------
        -- OK, here's the main printer
 
+pprKind, pprParendKind :: Kind -> SDoc
 pprKind = pprType
 pprParendKind = pprParendType
 
 ppr_type :: Prec -> Type -> SDoc
-ppr_type p (TyVarTy tv)       = ppr tv
-ppr_type p (PredTy pred)      = braces (ppr pred)
-ppr_type p (NoteTy other ty2) = ppr_type p ty2
+ppr_type _ (TyVarTy tv)              = ppr_tvar tv
+ppr_type p (PredTy pred)      = maybeParen p TyConPrec $
+                                ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
 ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
 
 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
@@ -477,8 +501,11 @@ ppr_type p (FunTy ty1 ty2)
     maybeParen p FunPrec $
     sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
   where
-    ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
-    ppr_fun_tail other_ty        = [arrow <+> pprType other_ty]
+    ppr_fun_tail (FunTy ty1 ty2) 
+      | not (is_pred ty1) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
+    ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
+    is_pred (PredTy {}) = True
+    is_pred _           = False
 
 ppr_forall_type :: Prec -> Type -> SDoc
 ppr_forall_type p ty
@@ -488,50 +515,96 @@ ppr_forall_type p ty
     (tvs,  rho) = split1 [] ty
     (ctxt, tau) = split2 [] rho
 
-    split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
-    split1 tvs (NoteTy _ ty)    = split1 tvs ty
-    split1 tvs ty              = (reverse tvs, ty)
+    -- We need to be extra careful here as equality constraints will occur as
+    -- type variables with an equality kind.  So, while collecting quantified
+    -- variables, we separate the coercion variables out and turn them into
+    -- equality predicates.
+    split1 tvs (ForAllTy tv ty) 
+      | not (isCoVar tv)     = split1 (tv:tvs) ty
+    split1 tvs ty           = (reverse tvs, ty)
  
-    split2 ps (NoteTy _ arg    -- Rather a disgusting case
-              `FunTy` res)           = split2 ps (arg `FunTy` res)
-    split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
-    split2 ps (NoteTy _ ty)          = split2 ps ty
-    split2 ps ty                     = (reverse ps, ty)
+    split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
+    split2 ps (ForAllTy tv ty) 
+       | isCoVar tv                = split2 (coVarPred tv : ps) ty
+    split2 ps ty                   = (reverse ps, ty)
 
 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
-ppr_tc_app p tc [] 
+ppr_tc_app _ tc []
   = ppr_tc tc
-ppr_tc_app p tc [ty] 
+ppr_tc_app _ tc [ty]
   | tc `hasKey` listTyConKey = brackets (pprType ty)
-  | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
-  | tc `hasKey` liftedTypeKindTyConKey   = ptext SLIT("*")
-  | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
-  | tc `hasKey` openTypeKindTyConKey     = ptext SLIT("(?)")
-  | tc `hasKey` ubxTupleKindTyConKey     = ptext SLIT("(#)")
-  | tc `hasKey` argTypeKindTyConKey      = ptext SLIT("??")
+  | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
+  | tc `hasKey` liftedTypeKindTyConKey   = ptext (sLit "*")
+  | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
+  | tc `hasKey` openTypeKindTyConKey     = ptext (sLit "(?)")
+  | tc `hasKey` ubxTupleKindTyConKey     = ptext (sLit "(#)")
+  | tc `hasKey` argTypeKindTyConKey      = ptext (sLit "??")
 
 ppr_tc_app p tc tys
+  | [ecvar,ty] <- tys, tc `hasKey` hetMetCodeTypeTyConKey
+  = ptext (sLit "<[")  <> pprType ty <> ptext (sLit "]>@") <> ppr ecvar
   | isTupleTyCon tc && tyConArity tc == length tys
   = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
   | otherwise
-  = maybeParen p TyConPrec $
-    ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
+  = ppr_type_app p (getName tc) tys
+
+ppr_type_app :: Prec -> Name -> [Type] -> SDoc
+-- Used for classes as well as types; that's why it's separate from ppr_tc_app
+ppr_type_app p tc tys
+  | is_sym_occ         -- Print infix if possible
+  , [ty1,ty2] <- tys   -- We know nothing of precedence though
+  = maybeParen p FunPrec (sep [ppr_type FunPrec ty1, 
+                              pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
+  | otherwise
+  = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
+                              2 (sep (map pprParendType tys)))
+  where
+    is_sym_occ = isSymOcc (getOccName tc)
 
-ppr_tc :: TyCon -> SDoc
-ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
+ppr_tc :: TyCon -> SDoc        -- No brackets for SymOcc
+ppr_tc tc 
+  = pp_nt_debug <> ppr tc
   where
    pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc 
-                                            then ptext SLIT("<recnt>")
-                                            else ptext SLIT("<nt>"))
+                                            then ptext (sLit "<recnt>")
+                                            else ptext (sLit "<nt>"))
               | otherwise     = empty
 
+ppr_tvar :: TyVar -> SDoc
+ppr_tvar tv  -- Note [Infix type variables]
+  | isSymOcc (getOccName tv)  = parens (ppr tv)
+  | otherwise                = ppr tv
+
 -------------------
+pprForAll :: [TyVar] -> SDoc
 pprForAll []  = empty
-pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
+pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
 
-pprTvBndr tv | isLiftedTypeKind kind = ppr tv
-            | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
+pprTvBndr :: TyVar -> SDoc
+pprTvBndr tv | isLiftedTypeKind kind = ppr_tvar tv
+            | otherwise             = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
             where
               kind = tyVarKind tv
 \end{code}
 
+Note [Infix type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With TypeOperators you can say
+
+   f :: (a ~> b) -> b
+
+and the (~>) is considered a type variable.  However, the type
+pretty-printer in this module will just see (a ~> b) as
+
+   App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
+
+So it'll print the type in prefix form.  To avoid confusion we must
+remember to parenthesise the operator, thus
+
+   (~>) a b -> b
+
+See Trac #2766.
+
+
+
+