Remove leftover NoteTy/FTVNote bits
[ghc-hetmet.git] / compiler / types / TypeRep.lhs
index 5625f8e..4927dcc 100644 (file)
@@ -1,4 +1,5 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1998
 %
 \section[TypeRep]{Type - friends' interface}
@@ -6,7 +7,7 @@
 \begin{code}
 module TypeRep (
        TyThing(..), 
-       Type(..), TyNote(..),           -- Representation visible 
+       Type(..),
        PredType(..),                   -- to friends
        
        Kind, ThetaType,                -- Synonyms
@@ -14,14 +15,16 @@ module TypeRep (
        funTyCon,
 
        -- Pretty-printing
-       pprType, pprParendType, pprTyThingCategory,
-       pprPred, pprTheta, pprThetaArrow, pprClassPred,
+       pprType, pprParendType, pprTypeApp,
+       pprTyThing, pprTyThingCategory, 
+       pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
 
        -- Kinds
        liftedTypeKind, unliftedTypeKind, openTypeKind,
         argTypeKind, ubxTupleKind,
        isLiftedTypeKindCon, isLiftedTypeKind,
-       mkArrowKind, mkArrowKinds,
+       mkArrowKind, mkArrowKinds, isCoercionKind,
+       coVarPred,
 
         -- Kind constructors...
         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
@@ -37,32 +40,25 @@ 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 OccName
+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
+import FastString
 \end{code}
 
 %************************************************************************
@@ -172,7 +168,6 @@ data Type
   | 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
@@ -192,12 +187,11 @@ data Type
        TyVar
        Type    
 
-  | PredTy             -- A high level source type 
-       PredType        -- ...can be expanded to a representation type...
-
-  | NoteTy             -- A type with a note attached
-       TyNote
-       Type            -- The expanded version
+  | 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)
 
 type Kind = Type       -- Invariant: a kind is always
                        --      FunTy k1 k2
@@ -207,16 +201,10 @@ type Kind = Type  -- Invariant: a kind is always
 
 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
 \end{code}
 
 -------------------------------------
-               Source types
+               Note [PredTy]
 
 A type of the form
        PredTy p
@@ -239,7 +227,7 @@ Predicates are represented inside GHC by PredType:
 data PredType 
   = ClassP Class [Type]                -- Class predicate
   | IParam (IPName Name) Type  -- Implicit parameter
-  | EqPred Type Type           -- Equality predicate (ty1 :=: ty2)
+  | EqPred Type Type           -- Equality predicate (ty1 ~ ty2)
 
 type ThetaType = [PredType]
 \end{code}
@@ -256,6 +244,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.
+
 
 %************************************************************************
 %*                                                                     *
@@ -273,8 +279,11 @@ data TyThing = AnId     Id
             | 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")
@@ -302,6 +311,15 @@ We define a few wired-in type constructors here to avoid module knots
 --------------------------
 -- First the TyCons...
 
+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
@@ -313,38 +331,32 @@ funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] lif
 
 
 tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
-coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
+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 [] 
+mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
 
 --------------------------
 -- ... and now their names
 
-tySuperKindTyConName     = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
-coSuperKindTyConName = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
+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
+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 :: FastString -> Unique -> TyCon -> Name
 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ) 
                                              key 
-                                             Nothing           -- No parent object
                                              (ATyCon tycon)
                                              BuiltInSyntax
        -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
@@ -356,6 +368,8 @@ mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 kindTyConType :: TyCon -> Type
 kindTyConType kind = TyConApp kind []
 
+liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
+
 liftedTypeKind   = kindTyConType liftedTypeKindTyCon
 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
 openTypeKind     = kindTyConType openTypeKindTyCon
@@ -372,24 +386,37 @@ tySuperKind, coSuperKind :: SuperKind
 tySuperKind = kindTyConType tySuperKindTyCon 
 coSuperKind = kindTyConType coSuperKindTyCon 
 
+isTySuperKind :: SuperKind -> Bool
 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
-isTySuperKind other            = False
+isTySuperKind _                = False
 
+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}
 
 
@@ -421,15 +448,19 @@ pprType, pprParendType :: Type -> SDoc
 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
+
 ------------------
 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) = sep [ppr ty1, nest 2 (ptext SLIT("~")), ppr ty2]
 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) (ppr clas) tys
 
 pprTheta :: ThetaType -> SDoc
 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
@@ -452,13 +483,13 @@ 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 tv
+ppr_type _ (PredTy pred)      = 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 $
@@ -483,20 +514,23 @@ 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("*")
@@ -509,11 +543,27 @@ ppr_tc_app p tc tys
   | 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) (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
 
 ppr_tc :: TyCon -> SDoc
-ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
+ppr_tc tc = parenSymOcc (getOccName tc) (ppr_naked_tc tc)
+
+ppr_naked_tc :: TyCon -> SDoc  -- No brackets for SymOcc
+ppr_naked_tc tc 
+  = pp_nt_debug <> ppr tc
   where
    pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc 
                                             then ptext SLIT("<recnt>")
@@ -521,9 +571,11 @@ ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
               | otherwise     = empty
 
 -------------------
+pprForAll :: [TyVar] -> SDoc
 pprForAll []  = empty
 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
 
+pprTvBndr :: TyVar -> SDoc
 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
             | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
             where