Make assignTemp_ less pessimistic
[ghc-hetmet.git] / compiler / types / TypeRep.lhs
index c694dc8..db41403 100644 (file)
@@ -5,48 +5,37 @@
 \section[TypeRep]{Type - friends' interface}
 
 \begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
+-- We expose the relevant stuff from this module via the Type module
+{-# OPTIONS_HADDOCK hide #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
 module TypeRep (
        TyThing(..), 
-       Type(..), TyNote(..),           -- Representation visible 
-       PredType(..),                   -- to friends
+       Type(..),
+        Pred(..),                       -- to friends
        
-       Kind, ThetaType,                -- Synonyms
+        Kind, SuperKind,
+        PredType, ThetaType,      -- Synonyms
 
-       funTyCon,
+        -- Functions over types
+        mkTyConApp, mkTyConTy, mkTyVarTy, mkTyVarTys,
+        isLiftedTypeKind, isCoercionKind, 
 
-       -- Pretty-printing
+        -- Pretty-printing
        pprType, pprParendType, pprTypeApp,
        pprTyThing, pprTyThingCategory, 
-       pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
-
-       -- Kinds
-       liftedTypeKind, unliftedTypeKind, openTypeKind,
-        argTypeKind, ubxTupleKind,
-       isLiftedTypeKindCon, isLiftedTypeKind,
-       mkArrowKind, mkArrowKinds, isCoercionKind,
-
-        -- Kind constructors...
-        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
-        argTypeKindTyCon, ubxTupleKindTyCon,
-
-        -- And their names
-        unliftedTypeKindTyConName, openTypeKindTyConName,
-        ubxTupleKindTyConName, argTypeKindTyConName,
-        liftedTypeKindTyConName,
-
-        -- Super Kinds
-       tySuperKind, coSuperKind,
-        isTySuperKind, isCoSuperKind,
-       tySuperKindTyCon, coSuperKindTyCon,
-        
-       pprKind, pprParendKind
+       pprPredTy, pprEqPred, pprTheta, pprForAll, pprThetaArrowTy, pprClassPred,
+        pprKind, pprParendKind,
+       Prec(..), maybeParen, pprTcApp, pprTypeNameApp, 
+        pprPrefixApp, pprPred, pprArrowChain, pprThetaArrow,
+
+        -- Free variables
+        tyVarsOfType, tyVarsOfTypes,
+        tyVarsOfPred, tyVarsOfTheta,
+       varsOfPred, varsOfTheta,
+       predSize,
+
+        -- Substitutions
+        TvSubst(..), TvSubstEnv
     ) where
 
 #include "HsVersions.h"
@@ -55,9 +44,9 @@ import {-# SOURCE #-} DataCon( DataCon, dataConName )
 
 -- friends:
 import Var
+import VarEnv
 import VarSet
 import Name
-import OccName
 import BasicTypes
 import TyCon
 import Class
@@ -65,57 +54,14 @@ import Class
 -- others
 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
+import Pair
 
+-- libraries
+import qualified Data.Data        as Data hiding ( TyCon )
+import qualified Data.Foldable    as Data
+import qualified Data.Traversable as Data
+\end{code}
 
        ----------------------
        A note about newtypes
@@ -168,80 +114,108 @@ 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 (*never* a coercion 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            -- ^ 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]@
+                       -- See Note [Equality-constrained types]
+
+  | ForAllTy
+       TyCoVar         -- Type variable
+       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.Data, 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}
 
-  | ForAllTy           -- A polymorphic type
-       TyVar
-       Type    
-
-  | PredTy             -- The type of evidence for a type predictate
-       PredType        -- See Note [PredTy], and Note [Equality predicates]
-       -- 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 ...
+Note [Equality-constrained types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type   forall ab. (a ~ [b]) => blah
+is encoded like this:
 
-data TyNote = FTVNote TyVarSet -- The free type variables of the noted expression
-\end{code}
+   ForAllTy (a:*) $ ForAllTy (b:*) $
+   FunTy (PredTy (EqPred a [b]) $
+   blah
 
 -------------------------------------
                Note [PredTy]
 
-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:
-
 \begin{code}
-data PredType 
-  = ClassP Class [Type]                -- Class predicate
-  | IParam (IPName Name) Type  -- Implicit parameter
-  | EqPred Type Type           -- Equality predicate (ty1 ~ ty2)
-
+-- | 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\"
+type PredType = Pred Type
+
+data Pred a   -- Typically 'a' is instantiated with Type or Coercion
+  = ClassP Class [a]            -- ^ Class predicate e.g. @Eq a@
+  | IParam (IPName Name) a      -- ^ Implicit parameter e.g. @?x :: Int@
+  | EqPred a a                  -- ^ Equality predicate e.g @ty1 ~ ty2@
+  deriving (Data.Data, Data.Typeable, Data.Foldable, Data.Traversable, Functor)
+
+-- | A collection of 'PredType's
 type ThetaType = [PredType]
 \end{code}
 
@@ -278,6 +252,89 @@ name (wildCoVarName), since it's not mentioned.
 
 %************************************************************************
 %*                                                                     *
+            Simple constructors
+%*                                                                     *
+%************************************************************************
+
+These functions are here so that they can be used by TysPrim,
+which in turn is imported by Type
+
+\begin{code}
+mkTyVarTy  :: TyVar   -> Type
+mkTyVarTy  = TyVarTy
+
+mkTyVarTys :: [TyVar] -> [Type]
+mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
+
+-- | A key function: builds a 'TyConApp' or 'FunTy' as apppropriate to its arguments.
+-- Applies its arguments to the constructor from left to right
+mkTyConApp :: TyCon -> [Type] -> Type
+mkTyConApp tycon tys
+  | isFunTyCon tycon, [ty1,ty2] <- tys
+  = FunTy ty1 ty2
+
+  | otherwise
+  = TyConApp tycon tys
+
+-- | Create the plain type constructor type which has been applied to no type arguments at all.
+mkTyConTy :: TyCon -> Type
+mkTyConTy tycon = mkTyConApp tycon []
+
+isLiftedTypeKind :: Kind -> Bool
+-- This function is here because it's used in the pretty printer
+isLiftedTypeKind (TyConApp tc []) = tc `hasKey` liftedTypeKindTyConKey
+isLiftedTypeKind _                = False
+
+isCoercionKind :: Kind -> Bool
+-- All coercions are of form (ty1 ~ ty2)
+-- This function is here rather than in Coercion, because it
+-- is used in a knot-tied way to enforce invariants in Var
+isCoercionKind (PredTy (EqPred {})) = True
+isCoercionKind _                    = False
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+                       Free variables of types and coercions
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+tyVarsOfPred :: PredType -> TyCoVarSet
+tyVarsOfPred = varsOfPred tyVarsOfType
+
+tyVarsOfTheta :: ThetaType -> TyCoVarSet
+tyVarsOfTheta = varsOfTheta tyVarsOfType
+
+tyVarsOfType :: Type -> VarSet
+-- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
+tyVarsOfType (TyVarTy v)         = unitVarSet v
+tyVarsOfType (TyConApp _ tys)    = tyVarsOfTypes tys
+tyVarsOfType (PredTy sty)        = varsOfPred tyVarsOfType sty
+tyVarsOfType (FunTy arg res)     = tyVarsOfType arg `unionVarSet` tyVarsOfType res
+tyVarsOfType (AppTy fun arg)     = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
+tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
+
+tyVarsOfTypes :: [Type] -> TyVarSet
+tyVarsOfTypes tys = foldr (unionVarSet . tyVarsOfType) emptyVarSet tys
+
+varsOfPred :: (a -> VarSet) -> Pred a -> VarSet
+varsOfPred f (IParam _ ty)    = f ty
+varsOfPred f (ClassP _ tys)   = foldr (unionVarSet . f) emptyVarSet tys
+varsOfPred f (EqPred ty1 ty2) = f ty1 `unionVarSet` f ty2
+
+varsOfTheta :: (a -> VarSet) -> [Pred a] -> VarSet
+varsOfTheta f = foldr (unionVarSet . varsOfPred f) emptyVarSet
+
+predSize :: (a -> Int) -> Pred a -> Int
+predSize size (IParam _ t)   = 1 + size t
+predSize size (ClassP _ ts)  = 1 + sum (map size ts)
+predSize size (EqPred t1 t2) = size t1 + size t2
+\end{code}
+
+%************************************************************************
+%*                                                                     *
                        TyThing
 %*                                                                     *
 %************************************************************************
@@ -287,9 +344,11 @@ 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
+             | ACoAxiom CoAxiom
             | AClass   Class
 
 instance Outputable TyThing where 
@@ -299,14 +358,16 @@ 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 (ACoAxiom _) = ptext (sLit "Coercion axiom")
+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
   getName (ATyCon tc)   = getName tc   -- isn't visible there
+  getName (ACoAxiom cc) = getName cc
   getName (AClass cl)   = getName cl
   getName (ADataCon dc) = dataConName dc
 \end{code}
@@ -314,112 +375,92 @@ instance NamedThing TyThing where        -- Can't put this with the type
 
 %************************************************************************
 %*                                                                     *
-               Wired-in type constructors
+                       Substitutions
+      Data type defined here to avoid unnecessary mutual recursion
 %*                                                                     *
 %************************************************************************
 
-We define a few wired-in type constructors here to avoid module knots
-
 \begin{code}
---------------------------
--- First the TyCons...
-
-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
-       --      instance Control.Arrow (->)
-       -- becuase the expected kind is (*->*->*).  The trouble is that the
-       -- expected/actual stuff in the unifier does not go contra-variant, whereas
-       -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
-       -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
-
-
-tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
-coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
-
-liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
-openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
-unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
-ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName
-argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName
-
-mkKindTyCon :: Name -> TyCon
-mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
-
---------------------------
--- ... 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
-
-mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ) 
-                                             key 
-                                             (ATyCon tycon)
-                                             BuiltInSyntax
-       -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
-       -- because they are never in scope in the source
-
-------------------
--- We also need Kinds and SuperKinds, locally and in TyCon
+-- | Type substitution
+--
+-- #tvsubst_invariant#
+-- The following invariants must hold of a 'TvSubst':
+-- 
+-- 1. The in-scope set is needed /only/ to
+-- guide the generation of fresh uniques
+--
+-- 2. In particular, the /kind/ of the type variables in 
+-- the in-scope set is not relevant
+--
+-- 3. The substition is only applied ONCE! This is because
+-- in general such application will not reached a fixed point.
+data TvSubst           
+  = TvSubst InScopeSet         -- The in-scope type variables
+           TvSubstEnv  -- Substitution of types
+       -- See Note [Apply Once]
+       -- and Note [Extending the TvSubstEnv]
+
+-- | A substitition of 'Type's for 'TyVar's
+type TvSubstEnv = TyVarEnv Type
+       -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
+       -- invariant discussed in Note [Apply Once]), and also independently
+       -- in the middle of matching, and unification (see Types.Unify)
+       -- So you have to look at the context to know if it's idempotent or
+       -- apply-once or whatever
+\end{code}
 
-kindTyConType :: TyCon -> Type
-kindTyConType kind = TyConApp kind []
+Note [Apply Once]
+~~~~~~~~~~~~~~~~~
+We use TvSubsts to instantiate things, and we might instantiate
+       forall a b. ty
+\with the types
+       [a, b], or [b, a].
+So the substition might go [a->b, b->a].  A similar situation arises in Core
+when we find a beta redex like
+       (/\ a /\ b -> e) b a
+Then we also end up with a substition that permutes type variables. Other
+variations happen to; for example [a -> (a, b)].  
 
-liftedTypeKind   = kindTyConType liftedTypeKindTyCon
-unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
-openTypeKind     = kindTyConType openTypeKindTyCon
-argTypeKind      = kindTyConType argTypeKindTyCon
-ubxTupleKind    = kindTyConType ubxTupleKindTyCon
+       ***************************************************
+       *** So a TvSubst must be applied precisely once ***
+       ***************************************************
 
-mkArrowKind :: Kind -> Kind -> Kind
-mkArrowKind k1 k2 = FunTy k1 k2
+A TvSubst is not idempotent, but, unlike the non-idempotent substitution
+we use during unifications, it must not be repeatedly applied.
 
-mkArrowKinds :: [Kind] -> Kind -> Kind
-mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
+Note [Extending the TvSubst]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See #tvsubst_invariant# for the invariants that must hold.
 
-tySuperKind, coSuperKind :: SuperKind
-tySuperKind = kindTyConType tySuperKindTyCon 
-coSuperKind = kindTyConType coSuperKindTyCon 
+This invariant allows a short-cut when the TvSubstEnv is empty:
+if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
+then (substTy subst ty) does nothing.
 
-isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
-isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
-isTySuperKind other            = False
+For example, consider:
+       (/\a. /\b:(a~Int). ...b..) Int
+We substitute Int for 'a'.  The Unique of 'b' does not change, but
+nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
 
-isCoSuperKind :: SuperKind -> Bool
-isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
-isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
-isCoSuperKind other            = False
+This invariant has several crucial consequences:
 
--------------------
--- Lastly we need a few functions on Kinds
+* In substTyVarBndr, we need extend the TvSubstEnv 
+       - if the unique has changed
+       - or if the kind has changed
 
-isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
+* In substTyVar, we do not need to consult the in-scope set;
+  the TvSubstEnv is enough
 
-isLiftedTypeKind :: Kind -> Bool
-isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
-isLiftedTypeKind other            = 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 (NoteTy _ k)         = isCoercionKind k
-isCoercionKind (PredTy (EqPred {})) = True
-isCoercionKind other               = False
+* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
 \end{code}
 
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{The external interface}
-%*                                                                     *
+                   Pretty-printing types
+
+       Defined very early because of debug printing in assertions
+%*                                                                      *
 %************************************************************************
 
 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
@@ -440,37 +481,73 @@ maybeParen ctxt_prec inner_prec pretty
 
 ------------------
 pprType, pprParendType :: Type -> SDoc
-pprType       ty = ppr_type TopPrec   ty
+pprType       ty = ppr_type TopPrec ty
 pprParendType ty = ppr_type TyConPrec ty
 
-pprTypeApp :: NamedThing a => a -> SDoc -> [Type] -> SDoc
--- The first arg is the tycon; it's used to arrange printing infix 
--- if it looks like an operator
--- Second arg is the pretty-printed tycon
-pprTypeApp tc pp_tc tys = ppr_type_app TopPrec (getName tc) pp_tc tys
+pprKind, pprParendKind :: Kind -> SDoc
+pprKind       = pprType
+pprParendKind = pprParendType
 
 ------------------
-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]
+pprPredTy :: PredType -> SDoc
+pprPredTy = pprPred ppr_type
+
+pprPred :: (Prec -> a -> SDoc) -> Pred a -> SDoc
+pprPred pp (ClassP cls tys) = ppr_class_pred pp cls tys
+pprPred pp (IParam ip ty)   = ppr ip <> dcolon <> pp TopPrec ty
+pprPred pp (EqPred ty1 ty2) = ppr_eq_pred pp (Pair ty1 ty2)
+
+------------
+pprEqPred :: Pair Type -> SDoc
+pprEqPred = ppr_eq_pred ppr_type
+
+ppr_eq_pred :: (Prec -> a -> SDoc) -> Pair a -> SDoc
+ppr_eq_pred pp (Pair ty1 ty2) = sep [ pp FunPrec ty1
+                                    , nest 2 (ptext (sLit "~"))
+                                    , pp 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 = ppr_type_app TopPrec (getName clas) (ppr clas) tys
+pprClassPred = ppr_class_pred ppr_type
 
-pprTheta :: ThetaType -> SDoc
-pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
+ppr_class_pred :: (Prec -> a -> SDoc) -> Class -> [a] -> SDoc
+ppr_class_pred pp clas tys = pprTypeNameApp TopPrec pp (getName clas) tys
 
-pprThetaArrow :: ThetaType -> SDoc
-pprThetaArrow theta 
-  | null theta = empty
-  | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
+------------
+pprTheta :: ThetaType -> SDoc
+-- pprTheta [pred] = pprPred pred       -- I'm in two minds about this
+pprTheta theta  = parens (sep (punctuate comma (map pprPredTy theta)))
+
+pprThetaArrowTy :: ThetaType -> SDoc
+pprThetaArrowTy = pprThetaArrow ppr_type
+
+pprThetaArrow :: (Prec -> a -> SDoc) -> [Pred a] -> SDoc
+pprThetaArrow _ []      = empty
+pprThetaArrow pp [pred]
+      | noParenPred pred = pprPred pp pred <+> darrow
+pprThetaArrow pp preds   = parens (sep (punctuate comma (map (pprPred pp) preds)))
+                            <+> darrow
+
+noParenPred :: Pred a -> 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
     ppr ty = pprType ty
 
-instance Outputable PredType where
-    ppr = pprPred
+instance Outputable (Pred Type) where
+    ppr = pprPredTy   -- Not for arbitrary (Pred a), because the
+                     -- (Outputable a) doesn't give precedence
 
 instance Outputable name => OutputableBndr (IPName name) where
     pprBndr _ n = ppr n        -- Simple for now
@@ -478,105 +555,132 @@ instance Outputable name => OutputableBndr (IPName name) where
 ------------------
        -- OK, here's the main printer
 
-pprKind = pprType
-pprParendKind = pprParendType
-
 ppr_type :: Prec -> Type -> SDoc
-ppr_type p (TyVarTy tv)       = ppr tv
-ppr_type p (PredTy pred)      = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
-ppr_type p (NoteTy other ty2) = ppr_type p ty2
-ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
+ppr_type _ (TyVarTy tv)              = ppr_tvar tv
+ppr_type p (PredTy pred)      = maybeParen p TyConPrec $
+                                ifPprDebug (ptext (sLit "<pred>")) <> (pprPredTy pred)
+ppr_type p (TyConApp tc tys)  = pprTcApp p ppr_type tc tys
 
 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
                           pprType t1 <+> ppr_type TyConPrec t2
 
-ppr_type p ty@(ForAllTy _ _)       = ppr_forall_type p ty
+ppr_type p ty@(ForAllTy {})        = ppr_forall_type p ty
 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
 
 ppr_type p (FunTy ty1 ty2)
-  = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
-    maybeParen p FunPrec $
-    sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
+  = pprArrowChain p (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]
+    -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
+    ppr_fun_tail (FunTy ty1 ty2)
+      | not (is_pred ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2
+    ppr_fun_tail other_ty = [ppr_type TopPrec other_ty]
+
+    is_pred (PredTy {}) = True
+    is_pred _           = False
 
 ppr_forall_type :: Prec -> Type -> SDoc
 ppr_forall_type p ty
   = maybeParen p FunPrec $
-    sep [pprForAll tvs, pprThetaArrow (ctxt1 ++ ctxt2), pprType tau]
+    sep [pprForAll tvs, pprThetaArrowTy ctxt, pprType tau]
   where
-    (tvs, ctxt1, rho) = split1 [] [] ty
-    (ctxt2, tau)      = split2 [] rho
-
-    -- 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 eqs (ForAllTy tv ty) 
-      | isCoVar tv               = split1 tvs (eq:eqs) ty
-      | otherwise                = split1 (tv:tvs) eqs ty
-      where
-        PredTy eq = tyVarKind tv
-    split1 tvs eqs (NoteTy _ ty) = split1 tvs eqs ty
-    split1 tvs eqs ty           = (reverse tvs, reverse eqs, ty)
+    (tvs,  rho) = split1 [] ty
+    (ctxt, tau) = split2 [] rho
+
+    split1 tvs (ForAllTy tv ty) = 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)
-
-ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
-ppr_tc_app p tc [] 
-  = ppr_tc tc
-ppr_tc_app p 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("??")
-
-ppr_tc_app p tc tys
-  | isTupleTyCon tc && tyConArity tc == length tys
-  = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
-  | otherwise
-  = ppr_type_app p (getName tc) (ppr_naked_tc tc) tys
-
-ppr_type_app :: Prec -> Name -> SDoc -> [Type] -> SDoc
-ppr_type_app p tc pp_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, 
-                              pp_tc <+> ppr_type FunPrec ty2])
-  | otherwise
-  = maybeParen p TyConPrec (hang paren_tc 2 (sep (map pprParendType tys)))
-  where
-    is_sym_occ = isSymOcc (getOccName tc)
-    paren_tc | is_sym_occ = parens pp_tc
-            | otherwise  = pp_tc
+    split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
+    split2 ps ty                   = (reverse ps, ty)
+
+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
+
+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
 
-ppr_tc :: TyCon -> SDoc
-ppr_tc tc = parenSymOcc (getOccName tc) (ppr_naked_tc tc)
+   (~>) a b -> b
 
-ppr_naked_tc :: TyCon -> SDoc  -- No brackets for SymOcc
-ppr_naked_tc tc 
+See Trac #2766.
+
+\begin{code}
+pprTcApp :: Prec -> (Prec -> a -> SDoc) -> TyCon -> [a] -> SDoc
+pprTcApp _ _ tc []      -- No brackets for SymOcc
   = 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
 
--------------------
-pprForAll []  = empty
-pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
+pprTcApp _ pp tc [ty]
+  | tc `hasKey` listTyConKey = brackets (pp TopPrec ty)
+  | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pp TopPrec 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 "??")
 
-pprTvBndr tv | isLiftedTypeKind kind = ppr tv
-            | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
-            where
-              kind = tyVarKind tv
+pprTcApp p pp tc tys
+  | isTupleTyCon tc && tyConArity tc == length tys
+  = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map (pp TopPrec) tys)))
+  | otherwise
+  = pprTypeNameApp p pp (getName tc) tys
+
+----------------
+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 = pprTypeNameApp TopPrec ppr_type (getName tc) tys
+
+pprTypeNameApp :: Prec -> (Prec -> a -> SDoc) -> Name -> [a] -> SDoc
+-- Used for classes and coercions as well as types; that's why it's separate from pprTcApp
+pprTypeNameApp p pp tc tys
+  | is_sym_occ           -- Print infix if possible
+  , [ty1,ty2] <- tys  -- We know nothing of precedence though
+  = maybeParen p FunPrec $
+    sep [pp FunPrec ty1, pprInfixVar True (ppr tc) <+> pp FunPrec ty2]
+  | otherwise
+  = pprPrefixApp p (pprPrefixVar is_sym_occ (ppr tc)) (map (pp TyConPrec) tys)
+  where
+    is_sym_occ = isSymOcc (getOccName tc)
+
+----------------
+pprPrefixApp :: Prec -> SDoc -> [SDoc] -> SDoc
+pprPrefixApp p pp_fun pp_tys = maybeParen p TyConPrec $
+                               hang pp_fun 2 (sep pp_tys)
+
+----------------
+pprArrowChain :: Prec -> [SDoc] -> SDoc
+-- pprArrowChain p [a,b,c]  generates   a -> b -> c
+pprArrowChain _ []         = empty
+pprArrowChain p (arg:args) = maybeParen p FunPrec $
+                             sep [arg, sep (map (arrow <+>) args)]
 \end{code}