%
% (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(..),
	PredType(..),	 		-- to friends
	
 	Kind, ThetaType,		-- Synonyms

	funTyCon, funTyConName,

	-- Pretty-printing
	pprType, pprParendType, pprTypeApp,
	pprTyThing, pprTyThingCategory, 
	pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,

	-- Kinds
	liftedTypeKind, unliftedTypeKind, openTypeKind,
        argTypeKind, ubxTupleKind,
	isLiftedTypeKindCon, isLiftedTypeKind,
	mkArrowKind, mkArrowKinds, isCoercionKind,
  	coVarPred,

        -- 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
    ) where

#include "HsVersions.h"

import {-# SOURCE #-} DataCon( DataCon, dataConName )

-- friends:
import Var
import Name
import BasicTypes
import TyCon
import Class

-- others
import PrelNames
import Outputable
import FastString

-- libraries
import Data.Data hiding ( TyCon )
\end{code}

	----------------------
	A note about newtypes
	----------------------

Consider
	newtype N = MkN Int

Then we want N to be represented as an Int, and that's what we arrange.
The front end of the compiler [TcType.lhs] treats N as opaque, 
the back end treats it as transparent [Type.lhs].

There's a bit of a problem with recursive newtypes
	newtype P = MkP P
	newtype Q = MkQ (Q->Q)

Here the 'implicit expansion' we get from treating P and Q as transparent
would give rise to infinite types, which in turn makes eqType diverge.
Similarly splitForAllTys and splitFunTys can get into a loop.  

Solution: 

* Newtypes are always represented using TyConApp.

* For non-recursive newtypes, P, treat P just like a type synonym after 
  type-checking is done; i.e. it's opaque during type checking (functions
  from TcType) but transparent afterwards (functions from Type).  
  "Treat P as a type synonym" means "all functions expand NewTcApps 
  on the fly".

  Applications of the data constructor P simply vanish:
	P x = x
  

* For recursive newtypes Q, treat the Q and its representation as 
  distinct right through the compiler.  Applications of the data consructor
  use a coerce:
	Q = \(x::Q->Q). coerce Q x
  They are rare, so who cares if they are a tiny bit less efficient.

The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
to cut all loops.  The other members of the loop may be marked 'non-recursive'.


%************************************************************************
%*									*
\subsection{The data type}
%*									*
%************************************************************************


\begin{code}
-- | The key representation of types within the compiler
data Type
  = TyVarTy TyVar	-- ^ Vanilla type variable

  | AppTy
	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
	TyVar
	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}

-------------------------------------
 		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 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}

(We don't support TREX records yet, but the setup is designed
to expand to allow them.)

A Haskell qualified type, such as that for f,g,h above, is
represented using 
	* a FunTy for the double arrow
	* with a PredTy as the function argument

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.


%************************************************************************
%*									*
			TyThing
%*									*
%************************************************************************

Despite the fact that DataCon has to be imported via a hi-boot route, 
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 = 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")

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 (AClass cl)   = getName cl
  getName (ADataCon dc) = dataConName dc
\end{code}


%************************************************************************
%*									*
		Wired-in type constructors
%*									*
%************************************************************************

We define a few wired-in type constructors here to avoid module knots

\begin{code}
--------------------------
-- 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
	--	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   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

mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS 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

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

tySuperKind, coSuperKind :: SuperKind
tySuperKind = kindTyConType tySuperKindTyCon 
coSuperKind = kindTyConType coSuperKindTyCon 

isTySuperKind :: SuperKind -> Bool
isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
isTySuperKind _                = False

isCoSuperKind :: SuperKind -> Bool
isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
isCoSuperKind _                = False

-------------------
-- 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 _                = 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}



%************************************************************************
%*									*
\subsection{The external interface}
%*									*
%************************************************************************

@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
defined to use this.  @pprParendType@ is the same, except it puts
parens around the type, except for the atomic cases.  @pprParendType@
works just by setting the initial context precedence very high.

\begin{code}
data Prec = TopPrec 	-- No parens
	  | FunPrec 	-- Function args; no parens for tycon apps
	  | TyConPrec 	-- Tycon args; no parens for atomic
	  deriving( Eq, Ord )

maybeParen :: Prec -> Prec -> SDoc -> SDoc
maybeParen ctxt_prec inner_prec pretty
  | ctxt_prec < inner_prec = pretty
  | otherwise		   = parens pretty

------------------
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) = 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 = ppr_type_app TopPrec (getName clas) tys

pprTheta :: ThetaType -> SDoc
-- pprTheta [pred] = pprPred pred	 -- I'm in two minds about this
pprTheta theta  = parens (sep (punctuate comma (map pprPred theta)))

pprThetaArrow :: ThetaType -> SDoc
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
    ppr ty = pprType ty

instance Outputable PredType where
    ppr = pprPred

instance Outputable name => OutputableBndr (IPName name) where
    pprBndr _ n = ppr n	-- Simple for now

------------------
	-- OK, here's the main printer

pprKind, pprParendKind :: Kind -> SDoc
pprKind = pprType
pprParendKind = pprParendType

ppr_type :: Prec -> Type -> SDoc
ppr_type _ (TyVarTy tv)		-- Note [Infix type variables]
  | isSymOcc (getOccName tv)  = parens (ppr tv)
  | otherwise		      = ppr 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 $
			   pprType t1 <+> ppr_type TyConPrec t2

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)
  where
    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
  = maybeParen p FunPrec $
    sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
  where
    (tvs,  rho) = split1 [] ty
    (ctxt, 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 (ForAllTy tv ty) 
      | not (isCoVar tv)     = split1 (tv:tvs) ty
    split1 tvs ty	     = (reverse tvs, 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 _ tc []
  = ppr_tc tc
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 "??")

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) 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	-- 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>"))
	       | 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
	       kind = tyVarKind tv
\end{code}

Note [Infix type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Haskell 98 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.