\begin{code}
module Class (
- Class, ClassOpItem, FunDep,
+ Class, ClassOpItem,
DefMeth (..),
+ FunDep, pprFundeps,
+
mkClass, classTyVars, classArity,
classKey, className, classSelIds, classTyCon, classMethods,
classBigSig, classExtraBigSig, classTvsFds, classSCTheta
ppr DefMeth = text "{- has default method -}"
ppr GenDefMeth = text "{- has generic method -}"
ppr NoDefMeth = empty -- No default method
-\end{code}
+pprFundeps :: Outputable a => [FunDep a] -> SDoc
+pprFundeps [] = empty
+pprFundeps fds = hsep (ptext SLIT("|") : punctuate comma (map ppr_fd fds))
+ where
+ ppr_fd (us, vs) = hsep [interppSP us, ptext SLIT("->"),
+ interppSP vs]
+\end{code}
import Name ( Name, getSrcLoc )
import Var ( TyVar )
-import Class ( Class, FunDep, classTvsFds )
-import Unify ( tcUnifyTys, BindFlag(..) )
+import Class ( Class, FunDep, pprFundeps, classTvsFds )
+import TcGadt ( tcUnifyTys, BindFlag(..) )
import Type ( substTys, notElemTvSubst )
import TcType ( Type, PredType(..), tcEqType,
predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
\end{code}
-%************************************************************************
-%* *
-\subsection{Miscellaneous}
-%* *
-%************************************************************************
-
-\begin{code}
-pprFundeps :: Outputable a => [FunDep a] -> SDoc
-pprFundeps [] = empty
-pprFundeps fds = hsep (ptext SLIT("|") : punctuate comma (map ppr_fd fds))
-
-ppr_fd (us, vs) = hsep [interppSP us, ptext SLIT("->"), interppSP vs]
-\end{code}
tyClsNamesOfType, tcSplitTyConApp_maybe
)
import TyCon ( tyConName )
-import Unify ( tcMatchTys, tcUnifyTys, BindFlag(..) )
+import TcGadt ( tcUnifyTys, BindFlag(..) )
+import Unify ( tcMatchTys )
import Outputable
+import BasicTypes ( OverlapFlag(..) )
import UniqFM ( UniqFM, lookupUFM, emptyUFM, addToUFM_C, eltsUFM )
import Id ( idType, idName )
import SrcLoc ( pprDefnLoc )
, is_tys :: [Type] -- Full arg types
, is_dfun :: DFunId
- , is_flag :: OverlapFlag
+ , is_flag :: OverlapFlag -- See detailed comments with
+ -- the decl of BasicTypes.OverlapFlag
, is_orph :: Maybe OccName }
-- False is non-committal
instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
instanceCantMatch ts as = False -- Safe
-
----------------------------------------------------
-data OverlapFlag
- = NoOverlap -- This instance must not overlap another
-
- | OverlapOk -- Silently ignore this instance if you find a
- -- more specific one that matches the constraint
- -- you are trying to resolve
- --
- -- Example: constraint (Foo [Int])
- -- instances (Foo [Int])
- -- (Foo [a]) OverlapOk
- -- Since the second instance has the OverlapOk flag,
- -- the first instance will be chosen (otherwise
- -- its ambiguous which to choose)
-
- | Incoherent -- Like OverlapOk, but also ignore this instance
- -- if it doesn't match the constraint you are
- -- trying to resolve, but could match if the type variables
- -- in the constraint were instantiated
- --
- -- Example: constraint (Foo [b])
- -- instances (Foo [Int]) Incoherent
- -- (Foo [a])
- -- Without the Incoherent flag, we'd complain that
- -- instantiating 'b' would change which instance
- -- was chosen
- deriving( Eq )
-
-instance Outputable OverlapFlag where
- ppr NoOverlap = empty
- ppr OverlapOk = ptext SLIT("[overlap ok]")
- ppr Incoherent = ptext SLIT("[incoherent]")
\end{code}
+++ /dev/null
-%
-% (c) The GRASP/AQUA Project, Glasgow University, 1998
-%
-
-\begin{code}
-module Kind (
- Kind(..), SimpleKind,
- openTypeKind, liftedTypeKind, unliftedTypeKind, unboxedTypeKind,
- argTypeKind, ubxTupleKind,
-
- isLiftedTypeKind, isUnliftedTypeKind, isUnliftedBoxedTypeKind,
- isArgTypeKind, isOpenTypeKind,
- mkArrowKind, mkArrowKinds,
-
- isSubKind, defaultKind,
- kindFunResult, splitKindFunTys,
-
- KindVar, mkKindVar, kindVarRef, kindVarUniq,
- kindVarOcc, setKindVarOcc,
-
- pprKind, pprParendKind
- ) where
-
-#include "HsVersions.h"
-
-import Unique ( Unique )
-import OccName ( OccName, mkOccName, tvName )
-import Outputable
-import DATA_IOREF
-\end{code}
-
-Kinds
-~~~~~
-There's a little subtyping at the kind level:
-
- ?
- / \
- / \
- ?? (#)
- / | \
- * ! #
-
-where * [LiftedTypeKind] means boxed type
- # [UnboxedTypeKind] means unboxed type
- (#) [UbxTupleKind] means unboxed tuple
- ?? [ArgTypeKind] is the lub of *,#
- ? [OpenTypeKind] means any type at all
-
-In particular:
-
- error :: forall a:?. String -> a
- (->) :: ?? -> ? -> *
- (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
-
-\begin{code}
-data Kind
- = LiftedTypeKind -- *
- | OpenTypeKind -- ?
- | UnboxedTypeKind -- #
- | UnliftedTypeKind -- !
- | UbxTupleKind -- (##)
- | ArgTypeKind -- ??
- | FunKind Kind Kind -- k1 -> k2
- | KindVar KindVar
- deriving( Eq )
-
-data KindVar = KVar Unique OccName (IORef (Maybe SimpleKind))
- -- INVARIANT: a KindVar can only be instantiated by a SimpleKind
-
-type SimpleKind = Kind
- -- A SimpleKind has no ? or # kinds in it:
- -- sk ::= * | sk1 -> sk2 | kvar
-
-instance Eq KindVar where
- (KVar u1 _ _) == (KVar u2 _ _) = u1 == u2
-
-mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar
-mkKindVar u r = KVar u kind_var_occ r
-
-kindVarRef :: KindVar -> IORef (Maybe Kind)
-kindVarRef (KVar _ _ ref) = ref
-
-kindVarUniq :: KindVar -> Unique
-kindVarUniq (KVar uniq _ _) = uniq
-
-kindVarOcc :: KindVar -> OccName
-kindVarOcc (KVar _ occ _) = occ
-
-setKindVarOcc :: KindVar -> OccName -> KindVar
-setKindVarOcc (KVar u _ r) occ = KVar u occ r
-
-kind_var_occ :: OccName -- Just one for all KindVars
- -- They may be jiggled by tidying
-kind_var_occ = mkOccName tvName "k"
-\end{code}
-
-Kind inference
-~~~~~~~~~~~~~~
-During kind inference, a kind variable unifies only with
-a "simple kind", sk
- sk ::= * | sk1 -> sk2
-For example
- data T a = MkT a (T Int#)
-fails. We give T the kind (k -> *), and the kind variable k won't unify
-with # (the kind of Int#).
-
-Type inference
-~~~~~~~~~~~~~~
-When creating a fresh internal type variable, we give it a kind to express
-constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
-with kind ??.
-
-During unification we only bind an internal type variable to a type
-whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
-
-When unifying two internal type variables, we collect their kind constraints by
-finding the GLB of the two. Since the partial order is a tree, they only
-have a glb if one is a sub-kind of the other. In that case, we bind the
-less-informative one to the more informative one. Neat, eh?
-
-
-\begin{code}
-liftedTypeKind = LiftedTypeKind
-unboxedTypeKind = UnboxedTypeKind
-unliftedTypeKind = UnliftedTypeKind
-openTypeKind = OpenTypeKind
-argTypeKind = ArgTypeKind
-ubxTupleKind = UbxTupleKind
-
-mkArrowKind :: Kind -> Kind -> Kind
-mkArrowKind k1 k2 = k1 `FunKind` k2
-
-mkArrowKinds :: [Kind] -> Kind -> Kind
-mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
-\end{code}
-
-%************************************************************************
-%* *
- Functions over Kinds
-%* *
-%************************************************************************
-
-\begin{code}
-kindFunResult :: Kind -> Kind
-kindFunResult (FunKind _ k) = k
-kindFunResult k = pprPanic "kindFunResult" (ppr k)
-
-splitKindFunTys :: Kind -> ([Kind],Kind)
-splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of
- (as, r) -> (k1:as, r)
-splitKindFunTys k = ([], k)
-
-isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool
-isLiftedTypeKind LiftedTypeKind = True
-isLiftedTypeKind other = False
-
-isUnliftedBoxedTypeKind UnliftedTypeKind = True
-isUnliftedBoxedTypeKind other = False
-
-isUnliftedTypeKind UnliftedTypeKind = True
-isUnliftedTypeKind UnboxedTypeKind = True
-isUnliftedTypeKind other = False
-
-isArgTypeKind :: Kind -> Bool
--- True of any sub-kind of ArgTypeKind
-isArgTypeKind LiftedTypeKind = True
-isArgTypeKind UnliftedTypeKind = True
-isArgTypeKind UnboxedTypeKind = True
-isArgTypeKind ArgTypeKind = True
-isArgTypeKind other = False
-
-isOpenTypeKind :: Kind -> Bool
--- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
-isOpenTypeKind (FunKind _ _) = False
-isOpenTypeKind (KindVar _) = False -- This is a conservative answer
- -- It matters in the call to isSubKind in
- -- checkExpectedKind.
-isOpenTypeKind other = True
-
-isSubKind :: Kind -> Kind -> Bool
--- (k1 `isSubKind` k2) checks that k1 <: k2
-isSubKind LiftedTypeKind LiftedTypeKind = True
-isSubKind UnliftedTypeKind UnliftedTypeKind = True
-isSubKind UnboxedTypeKind UnboxedTypeKind = True
-isSubKind UbxTupleKind UbxTupleKind = True
-isSubKind k1 OpenTypeKind = isOpenTypeKind k1
-isSubKind k1 ArgTypeKind = isArgTypeKind k1
-isSubKind (FunKind a1 r1) (FunKind a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
-isSubKind k1 k2 = False
-
-defaultKind :: Kind -> Kind
--- Used when generalising: default kind '?' and '??' to '*'
---
--- When we generalise, we make generic type variables whose kind is
--- simple (* or *->* etc). So generic type variables (other than
--- built-in constants like 'error') always have simple kinds. This is important;
--- consider
--- f x = True
--- We want f to get type
--- f :: forall (a::*). a -> Bool
--- Not
--- f :: forall (a::??). a -> Bool
--- because that would allow a call like (f 3#) as well as (f True),
---and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
-defaultKind OpenTypeKind = LiftedTypeKind
-defaultKind ArgTypeKind = LiftedTypeKind
-defaultKind kind = kind
-\end{code}
-
-
-%************************************************************************
-%* *
- Pretty printing
-%* *
-%************************************************************************
-
-\begin{code}
-instance Outputable KindVar where
- ppr (KVar uniq occ _) = ppr occ <> ifPprDebug (ppr uniq)
-
-instance Outputable Kind where
- ppr k = pprKind k
-
-pprParendKind :: Kind -> SDoc
-pprParendKind k@(FunKind _ _) = parens (pprKind k)
-pprParendKind k = pprKind k
-
-pprKind (KindVar v) = ppr v
-pprKind LiftedTypeKind = ptext SLIT("*")
-pprKind UnliftedTypeKind = ptext SLIT("!")
-pprKind UnboxedTypeKind = ptext SLIT("#")
-pprKind OpenTypeKind = ptext SLIT("?")
-pprKind ArgTypeKind = ptext SLIT("??")
-pprKind UbxTupleKind = ptext SLIT("(#)")
-pprKind (FunKind k1 k2) = sep [ pprParendKind k1, arrow <+> pprKind k2]
-
-\end{code}
isFunTyCon, isUnLiftedTyCon, isProductTyCon,
isAlgTyCon, isDataTyCon, isSynTyCon, isNewTyCon, isPrimTyCon,
- isEnumerationTyCon,
+ isEnumerationTyCon, isGadtSyntaxTyCon,
isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, tupleTyConBoxity,
- isRecursiveTyCon, newTyConRep, newTyConRhs,
- isHiBootTyCon,
+ isRecursiveTyCon, newTyConRep, newTyConRhs, newTyConCo,
+ isHiBootTyCon, isSuperKindTyCon,
+ isCoercionTyCon_maybe, isCoercionTyCon,
- tcExpandTyCon_maybe, coreExpandTyCon_maybe,
+ tcExpandTyCon_maybe, coreExpandTyCon_maybe, stgExpandTyCon_maybe,
makeTyConAbstract, isAbstractTyCon,
mkClassTyCon,
mkFunTyCon,
mkPrimTyCon,
+ mkVoidPrimTyCon,
mkLiftedPrimTyCon,
mkTupleTyCon,
mkSynTyCon,
+ mkSuperKindTyCon,
+ mkCoercionTyCon,
tyConName,
tyConKind,
#include "HsVersions.h"
-import {-# SOURCE #-} TypeRep ( Type, PredType )
- -- Should just be Type(Type), but this fails due to bug present up to
- -- and including 4.02 involving slurping of hi-boot files. Bug is now fixed.
-
+import {-# SOURCE #-} TypeRep ( Kind, Type, Coercion, PredType )
import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
-
import Var ( TyVar, Id )
import Class ( Class )
-import Kind ( Kind )
import BasicTypes ( Arity, RecFlag(..), Boxity(..), isBoxed )
import Name ( Name, nameUnique, NamedThing(getName) )
import PrelNames ( Unique, Uniquable(..) )
algTcSelIds :: [Id], -- Its record selectors (empty if none):
+ algTcGadtSyntax :: Bool, -- True <=> the data type was declared using GADT syntax
+ -- That doesn't mean it's a true GADT; only that the "where"
+ -- form was used. This field is used only to guide
+ -- pretty-printinng
algTcStupidTheta :: [PredType], -- The "stupid theta" for the data type
-- (always empty for GADTs)
-- Just cl if this tycon came from a class declaration
}
+ | TupleTyCon {
+ tyConUnique :: Unique,
+ tyConName :: Name,
+ tyConKind :: Kind,
+ tyConArity :: Arity,
+ tyConBoxed :: Boxity,
+ tyConTyVars :: [TyVar],
+ dataCon :: DataCon,
+ hasGenerics :: Bool
+ }
+
+ | SynTyCon {
+ tyConUnique :: Unique,
+ tyConName :: Name,
+ tyConKind :: Kind,
+ tyConArity :: Arity,
+
+ tyConTyVars :: [TyVar], -- Bound tyvars
+ synTcRhs :: Type, -- Right-hand side, mentioning these type vars.
+ -- Acts as a template for the expansion when
+ -- the tycon is applied to some types.
+ argVrcs :: ArgVrcs
+ }
+
| PrimTyCon { -- Primitive types; cannot be defined in Haskell
-- Now includes foreign-imported types
+ -- Also includes Kinds
tyConUnique :: Unique,
tyConName :: Name,
tyConKind :: Kind,
tyConExtName :: Maybe FastString -- Just xx for foreign-imported types
}
- | TupleTyCon {
+ | CoercionTyCon { -- E.g. (:=:), sym, trans, left, right
+ -- INVARIANT: coercions are always fully applied
tyConUnique :: Unique,
- tyConName :: Name,
- tyConKind :: Kind,
+ tyConName :: Name,
tyConArity :: Arity,
- tyConBoxed :: Boxity,
- tyConTyVars :: [TyVar],
- dataCon :: DataCon,
- hasGenerics :: Bool
+ coKindFun :: [Type] -> Kind
+ }
+
+ | SuperKindTyCon { -- Super Kinds, TY (box) and CO (diamond).
+ -- They have no kind; and arity zero
+ tyConUnique :: Unique,
+ tyConName :: Name
}
- | SynTyCon {
- tyConUnique :: Unique,
- tyConName :: Name,
- tyConKind :: Kind,
- tyConArity :: Arity,
+type KindCon = TyCon
- tyConTyVars :: [TyVar], -- Bound tyvars
- synTcRhs :: Type, -- Right-hand side, mentioning these type vars.
- -- Acts as a template for the expansion when
- -- the tycon is applied to some types.
- argVrcs :: ArgVrcs
- }
+type SuperKindCon = TyCon
type FieldLabel = Name
nt_rhs :: Type, -- Cached: the argument type of the constructor
-- = the representation type of the tycon
+ -- The free tyvars of this type are the tyConTyVars
+
+ nt_co :: TyCon, -- The coercion used to create the newtype
+ -- from the representation
+ -- See Note [Newtype coercions]
nt_etad_rhs :: ([TyVar], Type) ,
-- The same again, but this time eta-reduced
visibleDataCons (NewTyCon{ data_con = c }) = [c]
\end{code}
+Note [Newtype coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+The NewTyCon field nt_co is a a TyCon (a coercion constructor in fact)
+which is used for coercing from the representation type of the
+newtype, to the newtype itself. For example,
+
+ newtype T a = MkT [a]
+
+the NewTyCon for T will contain nt_co = CoT where CoT t : [t] :=: T t.
+This TyCon is a CoercionTyCon, so it does not have a kind on its own;
+it basically has its own typing rule for the fully-applied version.
+If the newtype T has k type variables then CoT has arity k.
+
Note [Newtype eta]
~~~~~~~~~~~~~~~~~~
Consider
-- This is the making of a TyCon. Just the same as the old mkAlgTyCon,
-- but now you also have to pass in the generic information about the type
-- constructor - you can get hold of it easily (see Generics module)
-mkAlgTyCon name kind tyvars argvrcs stupid rhs sel_ids is_rec gen_info
+mkAlgTyCon name kind tyvars argvrcs stupid rhs sel_ids is_rec gen_info gadt_syn
= AlgTyCon {
tyConName = name,
tyConUnique = nameUnique name,
algTcSelIds = sel_ids,
algTcClass = Nothing,
algTcRec = is_rec,
+ algTcGadtSyntax = gadt_syn,
hasGenerics = gen_info
}
algTcSelIds = [],
algTcClass = Just clas,
algTcRec = is_rec,
+ algTcGadtSyntax = False, -- Doesn't really matter
hasGenerics = False
}
mkPrimTyCon name kind arity arg_vrcs rep
= mkPrimTyCon' name kind arity arg_vrcs rep True
+mkVoidPrimTyCon name kind arity arg_vrcs
+ = mkPrimTyCon' name kind arity arg_vrcs VoidRep True
+
-- but RealWorld is lifted
mkLiftedPrimTyCon name kind arity arg_vrcs rep
= mkPrimTyCon' name kind arity arg_vrcs rep False
synTcRhs = rhs,
argVrcs = argvrcs
}
+
+mkCoercionTyCon name arity kindRule
+ = CoercionTyCon {
+ tyConName = name,
+ tyConUnique = nameUnique name,
+ tyConArity = arity,
+ coKindFun = kindRule
+ }
+
+-- Super kinds always have arity zero
+mkSuperKindTyCon name
+ = SuperKindTyCon {
+ tyConName = name,
+ tyConUnique = nameUnique name
+ }
\end{code}
\begin{code}
isSynTyCon (SynTyCon {}) = True
isSynTyCon _ = False
+isGadtSyntaxTyCon :: TyCon -> Bool
+isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res
+isGadtSyntaxTyCon other = False
+
isEnumerationTyCon :: TyCon -> Bool
isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res
isEnumerationTyCon other = False
-- isForeignTyCon identifies foreign-imported type constructors
isForeignTyCon (PrimTyCon {tyConExtName = Just _}) = True
isForeignTyCon other = False
+
+isSuperKindTyCon :: TyCon -> Bool
+isSuperKindTyCon (SuperKindTyCon {}) = True
+isSuperKindTyCon other = False
+
+isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, [Type] -> Kind)
+isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule})
+ = Just (ar, rule)
+isCoercionTyCon_maybe other = Nothing
+
+isCoercionTyCon (CoercionTyCon {}) = True
+isCoercionTyCon other = False
\end{code}
tcExpandTyCon_maybe other_tycon tys = Nothing
---------------
--- For the *Core* view, we expand synonyms *and* non-recursive newtypes
+-- For the *Core* view, we expand synonyms only as well
+{-
coreExpandTyCon_maybe (AlgTyCon {algTcRec = NonRecursive, -- Not recursive
algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs }}) tys
= case etad_rhs of -- Don't do this in the pattern match, lest we accidentally
-- match the etad_rhs of a *recursive* newtype
(tvs,rhs) -> expand tvs rhs tys
-
+-}
coreExpandTyCon_maybe tycon tys = tcExpandTyCon_maybe tycon tys
+---------------
+-- For the *STG* view, we expand synonyms *and* non-recursive newtypes
+stgExpandTyCon_maybe (AlgTyCon {algTcRec = NonRecursive, -- Not recursive
+ algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs }}) tys
+ = case etad_rhs of -- Don't do this in the pattern match, lest we accidentally
+ -- match the etad_rhs of a *recursive* newtype
+ (tvs,rhs) -> expand tvs rhs tys
+
+stgExpandTyCon_maybe tycon tys = coreExpandTyCon_maybe tycon tys
+
----------------
expand :: [TyVar] -> Type -- Template
-> [Type] -- Args
newTyConRep (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rep = rep }}) = (tvs, rep)
newTyConRep tycon = pprPanic "newTyConRep" (ppr tycon)
+newTyConCo :: TyCon -> TyCon
+newTyConCo (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_co = co }}) = co
+newTyConCo tycon = pprPanic "newTyConCo" (ppr tycon)
+
tyConPrimRep :: TyCon -> PrimRep
tyConPrimRep (PrimTyCon {primTyConRep = rep}) = rep
tyConPrimRep tc = ASSERT(not (isUnboxedTupleTyCon tc)) PtrRep
%
\section[Type]{Type - public interface}
+
\begin{code}
module Type (
-- re-exports from TypeRep
TyThing(..), Type, PredType(..), ThetaType,
funTyCon,
- -- Re-exports from Kind
- module Kind,
+ -- Kinds
+ Kind, SimpleKind, KindVar,
+ kindFunResult, splitKindFunTys,
+
+ liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
+ argTypeKindTyCon, ubxTupleKindTyCon,
+
+ liftedTypeKind, unliftedTypeKind, openTypeKind,
+ argTypeKind, ubxTupleKind,
+
+ tySuperKind, coSuperKind,
+
+ isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
+ isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
+ isCoSuperKind, isSuperKind, isCoercionKind,
+ mkArrowKind, mkArrowKinds,
+
+ isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
+ isSubKindCon,
-- Re-exports from TyCon
PrimRep(..),
mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
- mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
+ mkAppTy, mkAppTys, splitAppTy, splitAppTys,
+ splitAppTy_maybe, repSplitAppTy_maybe,
mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
splitFunTys, splitFunTysN,
mkTyConApp, mkTyConTy,
tyConAppTyCon, tyConAppArgs,
- splitTyConApp_maybe, splitTyConApp,
+ splitTyConApp_maybe, splitTyConApp,
+ splitNewTyConApp_maybe, splitNewTyConApp,
- repType, typePrimRep, coreView, tcView,
+ repType, typePrimRep, coreView, tcView, stgView, kindView,
mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
applyTy, applyTys, isForAllTy, dropForAlls,
-- Pretty-printing
pprType, pprParendType, pprTyThingCategory,
- pprPred, pprTheta, pprThetaArrow, pprClassPred
+ pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
) where
#include "HsVersions.h"
import TypeRep
-- friends:
-import Kind
-import Var ( Var, TyVar, tyVarKind, tyVarName, setTyVarName, mkTyVar )
+import Var ( Var, TyVar, tyVarKind, tyVarName,
+ setTyVarName, setTyVarKind, mkTyVar, isTyVar )
+import Name ( Name(..) )
+import Unique ( Unique )
import VarEnv
import VarSet
import OccName ( tidyOccName )
import Name ( NamedThing(..), mkInternalName, tidyNameOcc )
import Class ( Class, classTyCon )
+import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey,
+ ubxTupleKindTyConKey, argTypeKindTyConKey,
+ eqCoercionKindTyConKey )
import TyCon ( TyCon, isRecursiveTyCon, isPrimTyCon,
isUnboxedTupleTyCon, isUnLiftedTyCon,
isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
- isAlgTyCon, tyConArity,
+ isAlgTyCon, tyConArity, isSuperKindTyCon,
tcExpandTyCon_maybe, coreExpandTyCon_maybe,
- tyConKind, PrimRep(..), tyConPrimRep,
+ stgExpandTyCon_maybe,
+ tyConKind, PrimRep(..), tyConPrimRep, tyConUnique,
+ isCoercionTyCon_maybe, isCoercionTyCon
)
-- others
\begin{code}
{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
--- Srips off the *top layer only* of a type to give
+-- Strips off the *top layer only* of a type to give
-- its underlying representation type.
-- Returns Nothing if there is nothing to look through.
--
-- partially-applied type constructor; indeed, usually will!
coreView ty = Nothing
+{-# INLINE stgView #-}
+stgView :: Type -> Maybe Type
+-- When generating STG from Core it is important that we look through newtypes
+-- but for the rest of Core we are just using coercions. This does just what
+-- coreView USED to do.
+stgView (NoteTy _ ty) = Just ty
+stgView (PredTy p) = Just (predTypeRep p)
+stgView (TyConApp tc tys) | Just (tenv, rhs, tys') <- stgExpandTyCon_maybe tc tys
+ = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
+ -- Its important to use mkAppTys, rather than (foldl AppTy),
+ -- because the function part might well return a
+ -- partially-applied type constructor; indeed, usually will!
+stgView ty = Nothing
+
+
-----------------------------------------------
{-# INLINE tcView #-}
tcView :: Type -> Maybe Type
tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
tcView ty = Nothing
+
+-----------------------------------------------
+{-# INLINE kindView #-}
+kindView :: Kind -> Maybe Kind
+-- C.f. coreView, tcView
+-- For the moment, we don't even handle synonyms in kinds
+kindView (NoteTy _ k) = Just k
+kindView other = Nothing
\end{code}
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) = Just tv
getTyVar_maybe other = Nothing
+
\end{code}
-- mkTyConApp: see notes with mkAppTy
mk_app ty1 = foldl AppTy orig_ty1 orig_tys2
+-------------
splitAppTy_maybe :: Type -> Maybe (Type, Type)
-splitAppTy_maybe ty | Just ty' <- coreView ty = splitAppTy_maybe ty'
-splitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
-splitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-splitAppTy_maybe (TyConApp tc tys) = case snocView tys of
- Nothing -> Nothing
- Just (tys',ty') -> Just (TyConApp tc tys', ty')
-splitAppTy_maybe other = Nothing
+splitAppTy_maybe ty | Just ty' <- coreView ty
+ = splitAppTy_maybe ty'
+splitAppTy_maybe ty = repSplitAppTy_maybe ty
+-------------
+repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
+-- Does the AppTy split, but assumes that any view stuff is already done
+repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
+repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
+repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
+ Just (tys', ty') -> Just (TyConApp tc tys', ty')
+ Nothing -> Nothing
+repSplitAppTy_maybe other = Nothing
+-------------
splitAppTy :: Type -> (Type, Type)
splitAppTy ty = case splitAppTy_maybe ty of
Just pr -> pr
Nothing -> panic "splitAppTy"
+-------------
splitAppTys :: Type -> (Type, [Type])
splitAppTys ty = split ty ty []
where
split orig_ty (FunTy ty1 ty2) args = ASSERT( null args )
(TyConApp funTyCon [], [ty1,ty2])
split orig_ty ty args = (orig_ty, args)
+
\end{code}
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
splitTyConApp_maybe other = Nothing
+
+-- Sometimes we do NOT want to look throught a newtype. When case matching
+-- on a newtype we want a convenient way to access the arguments of a newty
+-- constructor so as to properly form a coercion.
+splitNewTyConApp :: Type -> (TyCon, [Type])
+splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
+ Just stuff -> stuff
+ Nothing -> pprPanic "splitNewTyConApp" (ppr ty)
+splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
+splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
+splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
+splitNewTyConApp_maybe other = Nothing
+
\end{code}
-- but we must expand them here. Sure to
-- be saturated because repType is only applied
-- to types of kind *
- ASSERT( isRecursiveTyCon tc &&
- tys `lengthIs` tyConArity tc )
+ ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
repType (new_type_rep tc tys)
repType ty = ty
Just (substTyWith tvs tys rep_ty)
splitRecNewType_maybe other = Nothing
+
+
+
\end{code}
~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{code}
typeKind :: Type -> Kind
-
-typeKind (TyVarTy tyvar) = tyVarKind tyvar
-typeKind (TyConApp tycon tys) = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
-typeKind (NoteTy _ ty) = typeKind ty
-typeKind (PredTy _) = liftedTypeKind -- Predicates are always
- -- represented by lifted types
-typeKind (AppTy fun arg) = kindFunResult (typeKind fun)
-typeKind (FunTy arg res) = liftedTypeKind
-typeKind (ForAllTy tv ty) = typeKind ty
+typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
+ -- We should be looking for the coercion kind,
+ -- not the type kind
+ foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
+typeKind (NoteTy _ ty) = typeKind ty
+typeKind (PredTy pred) = predKind pred
+typeKind (AppTy fun arg) = kindFunResult (typeKind fun)
+typeKind (ForAllTy tv ty) = typeKind ty
+typeKind (TyVarTy tyvar) = tyVarKind tyvar
+typeKind (FunTy arg res)
+ -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
+ -- not unliftedTypKind (#)
+ -- The only things that can be after a function arrow are
+ -- (a) types (of kind openTypeKind or its sub-kinds)
+ -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
+ | isTySuperKind k = k
+ | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
+ where
+ k = typeKind res
+
+predKind :: PredType -> Kind
+predKind (EqPred {}) = coSuperKind -- A coercion kind!
+predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
+predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
\end{code}
tidyTopType ty = tidyType emptyTidyEnv ty
\end{code}
-
-%************************************************************************
-%* *
- Tidying Kinds
-%* *
-%************************************************************************
-
-We use a grevious hack for tidying KindVars. A TidyEnv contains
-a (VarEnv Var) substitution, to express the renaming; but
-KindVars are not Vars. The Right Thing ultimately is to make them
-into Vars (and perhaps make Kinds into Types), but I just do a hack
-here: I make up a TyVar just to remember the new OccName for the
-renamed KindVar
-
\begin{code}
+
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
-tidyKind env@(tidy_env, subst) (KindVar kvar)
- | Just tv <- lookupVarEnv_Directly subst uniq
- = (env, KindVar (setKindVarOcc kvar (getOccName tv)))
- | otherwise
- = ((tidy', subst'), KindVar kvar')
- where
- uniq = kindVarUniq kvar
- (tidy', occ') = tidyOccName tidy_env (kindVarOcc kvar)
- kvar' = setKindVarOcc kvar occ'
- fake_tv = mkTyVar tv_name (panic "tidyKind:fake tv kind")
- tv_name = mkInternalName uniq occ' noSrcLoc
- subst' = extendVarEnv subst fake_tv fake_tv
-
-tidyKind env (FunKind k1 k2)
- = (env2, FunKind k1' k2')
- where
- (env1, k1') = tidyKind env k1
- (env2, k2') = tidyKind env1 k2
+tidyKind env k = tidyOpenType env k
-tidyKind env k = (env, k) -- Atomic kinds
\end{code}
-- attempt to expand one side or the other.
-- Now deal with newtypes, synonyms, pred-tys
- eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
- | Just t2' <- coreView t2 = eq env t1 t2'
+ eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
+ | Just t2' <- coreView t2 = eq env t1 t2'
-- Fall through case; not equal!
eq env t1 t2 = False
substPred :: TvSubst -> PredType -> PredType
substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
+substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs
deShadowTy tvs ty
where
in_scope = mkInScopeSet tvs
+subst_ty :: TvSubst -> Type -> Type
+-- subst_ty is the main workhorse for type substitution
+--
-- Note that the in_scope set is poked only if we hit a forall
-- so it may often never be fully computed
subst_ty subst ty
(subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
substTyVar :: TvSubst -> TyVar -> Type
-substTyVar subst tv
- = case lookupTyVar subst tv of
- Nothing -> TyVarTy tv
- Just ty' -> ty' -- See Note [Apply Once]
+substTyVar subst@(TvSubst in_scope env) tv
+ = case lookupTyVar subst tv of {
+ Nothing -> TyVarTy tv;
+ Just ty -> ty -- See Note [Apply Once]
+ }
lookupTyVar :: TvSubst -> TyVar -> Maybe Type
lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
substTyVarBndr subst@(TvSubst in_scope env) old_var
- | old_var == new_var -- No need to clone
- -- But we *must* zap any current substitution for the variable.
- -- For example:
- -- (\x.e) with id_subst = [x |-> e']
- -- Here we must simply zap the substitution for x
- --
- -- The new_id isn't cloned, but it may have a different type
- -- etc, so we must return it, not the old id
- = (TvSubst (in_scope `extendInScopeSet` new_var)
- (delVarEnv env old_var),
- new_var)
-
- | otherwise -- The new binder is in scope so
- -- we'd better rename it away from the in-scope variables
- -- Extending the substitution to do this renaming also
- -- has the (correct) effect of discarding any existing
- -- substitution for that variable
- = (TvSubst (in_scope `extendInScopeSet` new_var)
- (extendVarEnv env old_var (TyVarTy new_var)),
- new_var)
+ = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
where
- new_var = uniqAway in_scope old_var
+
+ new_env | no_change = delVarEnv env old_var
+ | otherwise = extendVarEnv env old_var (TyVarTy new_var)
+
+ no_change = new_var == old_var && not is_co_var
+ -- no_change means that the new_var is identical in
+ -- all respects to the old_var (same unique, same kind)
+ --
+ -- In that case we don't need to extend the substitution
+ -- to map old to new. But instead we must zap any
+ -- current substitution for the variable. For example:
+ -- (\x.e) with id_subst = [x |-> e']
+ -- Here we must simply zap the substitution for x
+
+ new_var = uniqAway in_scope subst_old_var
-- The uniqAway part makes sure the new variable is not already in scope
+
+ subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
+ -- It's only worth doing the substitution for coercions,
+ -- becuase only they can have free type variables
+ | is_co_var = setTyVarKind old_var (substTy subst kind)
+ | otherwise = old_var
+ kind = tyVarKind old_var
+ is_co_var = isCoercionKind kind
+\end{code}
+
+----------------------------------------------------
+-- Kind Stuff
+
+Kinds
+~~~~~
+There's a little subtyping at the kind level:
+
+ ?
+ / \
+ / \
+ ?? (#)
+ / \
+ * #
+
+where * [LiftedTypeKind] means boxed type
+ # [UnliftedTypeKind] means unboxed type
+ (#) [UbxTupleKind] means unboxed tuple
+ ?? [ArgTypeKind] is the lub of *,#
+ ? [OpenTypeKind] means any type at all
+
+In particular:
+
+ error :: forall a:?. String -> a
+ (->) :: ?? -> ? -> *
+ (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
+
+\begin{code}
+type KindVar = TyVar -- invariant: KindVar will always be a
+ -- TcTyVar with details MetaTv TauTv ...
+-- kind var constructors and functions are in TcType
+
+type SimpleKind = Kind
+\end{code}
+
+Kind inference
+~~~~~~~~~~~~~~
+During kind inference, a kind variable unifies only with
+a "simple kind", sk
+ sk ::= * | sk1 -> sk2
+For example
+ data T a = MkT a (T Int#)
+fails. We give T the kind (k -> *), and the kind variable k won't unify
+with # (the kind of Int#).
+
+Type inference
+~~~~~~~~~~~~~~
+When creating a fresh internal type variable, we give it a kind to express
+constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
+with kind ??.
+
+During unification we only bind an internal type variable to a type
+whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
+
+When unifying two internal type variables, we collect their kind constraints by
+finding the GLB of the two. Since the partial order is a tree, they only
+have a glb if one is a sub-kind of the other. In that case, we bind the
+less-informative one to the more informative one. Neat, eh?
+
+
+\begin{code}
+
+\end{code}
+
+%************************************************************************
+%* *
+ Functions over Kinds
+%* *
+%************************************************************************
+
+\begin{code}
+kindFunResult :: Kind -> Kind
+kindFunResult k = funResultTy k
+
+splitKindFunTys :: Kind -> ([Kind],Kind)
+splitKindFunTys k = splitFunTys k
+
+isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
+
+isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
+
+isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
+isOpenTypeKind other = False
+
+isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
+
+isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
+isUbxTupleKind other = False
+
+isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
+
+isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
+isArgTypeKind other = False
+
+isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
+
+isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
+isUnliftedTypeKind other = False
+
+isSubOpenTypeKind :: Kind -> Bool
+-- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
+isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
+ ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
+ False
+isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
+isSubOpenTypeKind other = ASSERT( isKind other ) False
+ -- This is a conservative answer
+ -- It matters in the call to isSubKind in
+ -- checkExpectedKind.
+
+isSubArgTypeKindCon kc
+ | isUnliftedTypeKindCon kc = True
+ | isLiftedTypeKindCon kc = True
+ | isArgTypeKindCon kc = True
+ | otherwise = False
+
+isSubArgTypeKind :: Kind -> Bool
+-- True of any sub-kind of ArgTypeKind
+isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
+isSubArgTypeKind other = False
+
+isSuperKind :: Type -> Bool
+isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
+isSuperKind other = False
+
+isKind :: Kind -> Bool
+isKind k = isSuperKind (typeKind k)
+
+
+
+isSubKind :: Kind -> Kind -> Bool
+-- (k1 `isSubKind` k2) checks that k1 <: k2
+isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc1
+isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
+isSubKind k1 k2 = False
+
+eqKind :: Kind -> Kind -> Bool
+eqKind = tcEqType
+
+isSubKindCon :: TyCon -> TyCon -> Bool
+-- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
+isSubKindCon kc1 kc2
+ | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
+ | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
+ | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
+ | isOpenTypeKindCon kc2 = True
+ -- we already know kc1 is not a fun, its a TyCon
+ | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
+ | otherwise = False
+
+defaultKind :: Kind -> Kind
+-- Used when generalising: default kind '?' and '??' to '*'
+--
+-- When we generalise, we make generic type variables whose kind is
+-- simple (* or *->* etc). So generic type variables (other than
+-- built-in constants like 'error') always have simple kinds. This is important;
+-- consider
+-- f x = True
+-- We want f to get type
+-- f :: forall (a::*). a -> Bool
+-- Not
+-- f :: forall (a::??). a -> Bool
+-- because that would allow a call like (f 3#) as well as (f True),
+--and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
+defaultKind k
+ | isSubOpenTypeKind k = liftedTypeKind
+ | isSubArgTypeKind k = liftedTypeKind
+ | otherwise = k
+
+isCoercionKind :: Kind -> Bool
+-- All coercions are of form (ty1 :=: ty2)
+-- This function is here rather than in Coercion,
+-- because it's used by substTy
+isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
+isCoercionKind (PredTy (EqPred {})) = True
+isCoercionKind other = False
\end{code}
pprType, pprParendType, pprTyThingCategory,
pprPred, pprTheta, pprThetaArrow, pprClassPred,
- -- Re-export fromKind
+ -- Kinds
liftedTypeKind, unliftedTypeKind, openTypeKind,
- isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
+ argTypeKind, ubxTupleKind,
+ isLiftedTypeKindCon, isLiftedTypeKind,
mkArrowKind, mkArrowKinds,
+
+ -- Kind constructors...
+ liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
+ argTypeKindTyCon, ubxTupleKindTyCon,
+
+ -- And their names
+ unliftedTypeKindTyConName, openTypeKindTyConName,
+ ubxTupleKindTyConName, argTypeKindTyConName,
+ liftedTypeKindTyConName,
+
+ -- Super Kinds
+ tySuperKind, coSuperKind,
+ isTySuperKind, isCoSuperKind,
+ tySuperKindTyCon, coSuperKindTyCon,
+
+ isCoercionKindTyCon,
+
pprKind, pprParendKind
) where
#include "HsVersions.h"
import {-# SOURCE #-} DataCon( DataCon, dataConName )
-
+import Monad ( guard )
-- friends:
-import Kind
+
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 )
+import TyCon ( TyCon, mkFunTyCon, tyConArity, tupleTyConBoxity, isTupleTyCon, isRecursiveTyCon, isNewTyCon, mkVoidPrimTyCon, mkSuperKindTyCon, isSuperKindTyCon, mkCoercionTyCon )
import Class ( Class )
-- others
-import PrelNames ( gHC_PRIM, funTyConKey, listTyConKey, parrTyConKey, hasKey )
+import PrelNames ( gHC_PRIM, funTyConKey, tySuperKindTyConKey,
+ coSuperKindTyConKey, liftedTypeKindTyConKey,
+ openTypeKindTyConKey, unliftedTypeKindTyConKey,
+ ubxTupleKindTyConKey, argTypeKindTyConKey, listTyConKey,
+ parrTyConKey, hasKey, eqCoercionKindTyConKey )
import Outputable
\end{code}
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
\end{code}
data PredType
= ClassP Class [Type] -- Class predicate
| IParam (IPName Name) Type -- Implicit parameter
+ | EqPred Type Type -- Equality predicate (ty1 :=: ty2)
type ThetaType = [PredType]
\end{code}
%************************************************************************
%* *
-\subsection{Wired-in type constructors
+ Wired-in type constructors
%* *
%************************************************************************
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
-- the kind sub-typing does. Sigh. It really only matters if you use (->) in
-- a prefix way, thus: (->) Int# Int#. And this is unusual.
-funTyConName = mkWiredInName gHC_PRIM
- (mkOccNameFS tcName FSLIT("(->)"))
- funTyConKey
- Nothing -- No parent object
- (ATyCon funTyCon) -- Relevant TyCon
- BuiltInSyntax
+
+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 []
+
+--------------------------
+-- ... 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)
+ key
+ Nothing -- No parent object
+ (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 []
+
+liftedTypeKind = kindTyConType liftedTypeKindTyCon
+unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
+openTypeKind = kindTyConType openTypeKindTyCon
+argTypeKind = kindTyConType argTypeKindTyCon
+ubxTupleKind = kindTyConType ubxTupleKindTyCon
+
+mkArrowKind :: Kind -> Kind -> Kind
+mkArrowKind k1 k2 = FunTy k1 k2
+
+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 (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
+isTySuperKind other = False
+
+isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
+isCoSuperKind other = False
+
+isCoercionKindTyCon kc = kc `hasKey` eqCoercionKindTyConKey
+
+
+-------------------
+-- lastly we need a few functions on Kinds
+
+isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
+
+isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
+isLiftedTypeKind other = False
+
+
\end{code}
+
%************************************************************************
%* *
\subsection{The external interface}
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]
pprClassPred :: Class -> [Type] -> SDoc
pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
------------------
-- 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) = braces (ppr pred)
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)))
\begin{code}
module TypeRep where
+import {-# SOURCE #-} TyCon ( TyCon )
+
data Type
data PredType
data TyThing
+
+type Coercion = Type
+
+type Kind = Type
+
+tySuperKind :: Kind
+coSuperKind :: Kind
+
+isCoSuperKind :: Kind -> Bool
\end{code}
\begin{code}
module Unify (
- -- Matching and unification
- tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..),
-
- tcUnifyTys,
-
- gadtRefineTys, BindFlag(..),
-
- coreRefineTys, dataConCanMatch, TypeRefinement,
-
- -- Re-export
- MaybeErr(..)
+ -- Matching of types:
+ -- the "tc" prefix indicates that matching always
+ -- respects newtypes (rather than looking through them)
+ tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..)
) where
#include "HsVersions.h"
import Var ( Var, TyVar, tyVarKind )
import VarEnv
import VarSet
-import Kind ( isSubKind )
import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX,
- mkOpenTvSubst, tcView )
+ mkOpenTvSubst, tcView, isSubKind, eqKind, repSplitAppTy_maybe )
import TypeRep ( Type(..), PredType(..), funTyCon )
-import DataCon ( DataCon, isVanillaDataCon, dataConResTys, dataConInstResTy )
+import DataCon ( DataCon, dataConResTys )
import Util ( snocView )
import ErrUtils ( Message )
import Outputable
\end{code}
-%************************************************************************
-%* *
- Unification
-%* *
-%************************************************************************
-
-\begin{code}
-tcUnifyTys :: (TyVar -> BindFlag)
- -> [Type] -> [Type]
- -> Maybe TvSubst -- A regular one-shot substitution
--- The two types may have common type variables, and indeed do so in the
--- second call to tcUnifyTys in FunDeps.checkClsFD
-tcUnifyTys bind_fn tys1 tys2
- = maybeErrToMaybe $ initUM bind_fn $
- do { subst_env <- unify_tys emptyTvSubstEnv tys1 tys2
-
- -- Find the fixed point of the resulting non-idempotent substitution
- ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
- subst = TvSubst in_scope subst_env_fixpt
- subst_env_fixpt = mapVarEnv (substTy subst) subst_env
- ; return subst }
- where
- tvs1 = tyVarsOfTypes tys1
- tvs2 = tyVarsOfTypes tys2
-
-----------------------------
-dataConCanMatch :: DataCon -> [Type] -> Bool
--- Returns True iff the data con can match a scrutinee of type (T tys)
--- where T is the type constructor for the data con
-dataConCanMatch con tys
- | isVanillaDataCon con
- = True
- | otherwise
- = isSuccess $ initUM (\tv -> BindMe) $
- unify_tys emptyTvSubstEnv (dataConResTys con) tys
-
-----------------------------
-coreRefineTys :: DataCon -> [TyVar] -- Case pattern (con tv1 .. tvn ...)
- -> Type -- Type of scrutinee
- -> Maybe TypeRefinement
-
-type TypeRefinement = (TvSubstEnv, Bool)
- -- The Bool is True iff all the bindings in the
- -- env are for the pattern type variables
- -- In this case, there is no type refinement
- -- for already-in-scope type variables
-
--- Used by Core Lint and the simplifier.
-coreRefineTys con tvs scrut_ty
- = maybeErrToMaybe $ initUM (tryToBind tv_set) $
- do { -- Run the unifier, starting with an empty env
- ; subst_env <- unify emptyTvSubstEnv pat_res_ty scrut_ty
-
- -- Find the fixed point of the resulting non-idempotent substitution
- ; let subst = mkOpenTvSubst subst_env_fixpt
- subst_env_fixpt = mapVarEnv (substTy subst) subst_env
-
- ; return (subst_env_fixpt, all_bound_here subst_env) }
- where
- pat_res_ty = dataConInstResTy con (mkTyVarTys tvs)
-
- -- 'tvs' are the tyvars bound by the pattern
- tv_set = mkVarSet tvs
- all_bound_here env = all bound_here (varEnvKeys env)
- bound_here uniq = elemVarSetByKey uniq tv_set
-
--- This version is used by the type checker
-gadtRefineTys :: TvSubst
- -> DataCon -> [TyVar]
- -> [Type] -> [Type]
- -> MaybeErr Message (TvSubst, Bool)
--- The bool is True <=> the only *new* bindings are for pat_tvs
-
-gadtRefineTys (TvSubst in_scope env1) con pat_tvs pat_tys ctxt_tys
- = initUM (tryToBind tv_set) $
- do { -- Run the unifier, starting with an empty env
- ; env2 <- unify_tys env1 pat_tys ctxt_tys
-
- -- Find the fixed point of the resulting non-idempotent substitution
- ; let subst2 = TvSubst in_scope subst_env_fixpt
- subst_env_fixpt = mapVarEnv (substTy subst2) env2
-
- ; return (subst2, all_bound_here env2) }
- where
- -- 'tvs' are the tyvars bound by the pattern
- tv_set = mkVarSet pat_tvs
- all_bound_here env = all bound_here (varEnvKeys env)
- bound_here uniq = elemVarEnvByKey uniq env1 || elemVarSetByKey uniq tv_set
- -- The bool is True <=> the only *new* bindings are for pat_tvs
-
-----------------------------
-tryToBind :: TyVarSet -> TyVar -> BindFlag
-tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
- | otherwise = AvoidMe
-\end{code}
-
-
-%************************************************************************
-%* *
- The workhorse
-%* *
-%************************************************************************
-
-\begin{code}
-unify :: TvSubstEnv -- An existing substitution to extend
- -> Type -> Type -- Types to be unified
- -> UM TvSubstEnv -- Just the extended substitution,
- -- Nothing if unification failed
--- We do not require the incoming substitution to be idempotent,
--- nor guarantee that the outgoing one is. That's fixed up by
--- the wrappers.
-
--- Respects newtypes, PredTypes
-
-unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
- unify_ subst ty1 ty2
-
--- in unify_, any NewTcApps/Preds should be taken at face value
-unify_ subst (TyVarTy tv1) ty2 = uVar False subst tv1 ty2
-unify_ subst ty1 (TyVarTy tv2) = uVar True subst tv2 ty1
-
-unify_ subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
-unify_ subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
-
-unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
-
-unify_ subst t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2)
- | tyc1 == tyc2 = unify_tys subst tys1 tys2
-
-unify_ subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
- = do { subst' <- unify subst ty1a ty2a
- ; unify subst' ty1b ty2b }
-
- -- Applications need a bit of care!
- -- They can match FunTy and TyConApp, so use splitAppTy_maybe
- -- NB: we've already dealt with type variables and Notes,
- -- so if one type is an App the other one jolly well better be too
-unify_ subst (AppTy ty1a ty1b) ty2
- | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
- = do { subst' <- unify subst ty1a ty2a
- ; unify subst' ty1b ty2b }
-
-unify_ subst ty1 (AppTy ty2a ty2b)
- | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
- = do { subst' <- unify subst ty1a ty2a
- ; unify subst' ty1b ty2b }
-
-unify_ subst ty1 ty2 = failWith (misMatch ty1 ty2)
-
-------------------------------
-unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
- | c1 == c2 = unify_tys subst tys1 tys2
-unify_pred subst (IParam n1 t1) (IParam n2 t2)
- | n1 == n2 = unify subst t1 t2
-unify_pred subst p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
-
-------------------------------
-unify_tys = unifyList unify
-
-unifyList :: Outputable a
- => (TvSubstEnv -> a -> a -> UM TvSubstEnv)
- -> TvSubstEnv -> [a] -> [a] -> UM TvSubstEnv
-unifyList unifier subst orig_xs orig_ys
- = go subst orig_xs orig_ys
- where
- go subst [] [] = return subst
- go subst (x:xs) (y:ys) = do { subst' <- unifier subst x y
- ; go subst' xs ys }
- go subst _ _ = failWith (lengthMisMatch orig_xs orig_ys)
-
-------------------------------
-uVar :: Bool -- Swapped
- -> TvSubstEnv -- An existing substitution to extend
- -> TyVar -- Type variable to be unified
- -> Type -- with this type
- -> UM TvSubstEnv
-
-uVar swap subst tv1 ty
- = -- Check to see whether tv1 is refined by the substitution
- case (lookupVarEnv subst tv1) of
- -- Yes, call back into unify'
- Just ty' | swap -> unify subst ty ty'
- | otherwise -> unify subst ty' ty
- -- No, continue
- Nothing -> uUnrefined subst tv1 ty ty
-
-
-uUnrefined :: TvSubstEnv -- An existing substitution to extend
- -> TyVar -- Type variable to be unified
- -> Type -- with this type
- -> Type -- (de-noted version)
- -> UM TvSubstEnv
-
--- We know that tv1 isn't refined
-
-uUnrefined subst tv1 ty2 ty2'
- | Just ty2'' <- tcView ty2'
- = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
- -- This is essential, in case we have
- -- type Foo a = a
- -- and then unify a :=: Foo a
-
-uUnrefined subst tv1 ty2 (TyVarTy tv2)
- | tv1 == tv2 -- Same type variable
- = return subst
-
- -- Check to see whether tv2 is refined
- | Just ty' <- lookupVarEnv subst tv2
- = uUnrefined subst tv1 ty' ty'
-
- -- So both are unrefined; next, see if the kinds force the direction
- | k1 == k2 -- Can update either; so check the bind-flags
- = do { b1 <- tvBindFlag tv1
- ; b2 <- tvBindFlag tv2
- ; case (b1,b2) of
- (BindMe, _) -> bind tv1 ty2
-
- (AvoidMe, BindMe) -> bind tv2 ty1
- (AvoidMe, _) -> bind tv1 ty2
-
- (WildCard, WildCard) -> return subst
- (WildCard, Skolem) -> return subst
- (WildCard, _) -> bind tv2 ty1
-
- (Skolem, WildCard) -> return subst
- (Skolem, Skolem) -> failWith (misMatch ty1 ty2)
- (Skolem, _) -> bind tv2 ty1
- }
-
- | k1 `isSubKind` k2 = bindTv subst tv2 ty1 -- Must update tv2
- | k2 `isSubKind` k1 = bindTv subst tv1 ty2 -- Must update tv1
-
- | otherwise = failWith (kindMisMatch tv1 ty2)
- where
- ty1 = TyVarTy tv1
- k1 = tyVarKind tv1
- k2 = tyVarKind tv2
- bind tv ty = return (extendVarEnv subst tv ty)
-
-uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
- | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
- = failWith (occursCheck tv1 ty2) -- Occurs check
- | not (k2 `isSubKind` k1)
- = failWith (kindMisMatch tv1 ty2) -- Kind check
- | otherwise
- = bindTv subst tv1 ty2 -- Bind tyvar to the synonym if poss
- where
- k1 = tyVarKind tv1
- k2 = typeKind ty2'
-
-substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
--- Apply the non-idempotent substitution to a set of type variables,
--- remembering that the substitution isn't necessarily idempotent
-substTvSet subst tvs
- = foldVarSet (unionVarSet . get) emptyVarSet tvs
- where
- get tv = case lookupVarEnv subst tv of
- Nothing -> unitVarSet tv
- Just ty -> substTvSet subst (tyVarsOfType ty)
-
-bindTv subst tv ty -- ty is not a type variable
- = do { b <- tvBindFlag tv
- ; case b of
- Skolem -> failWith (misMatch (TyVarTy tv) ty)
- WildCard -> return subst
- other -> return (extendVarEnv subst tv ty)
- }
-\end{code}
-
-%************************************************************************
-%* *
- Unification monad
-%* *
-%************************************************************************
-
-\begin{code}
-data BindFlag
- = BindMe -- A regular type variable
- | AvoidMe -- Like BindMe but, given the choice, avoid binding it
-
- | Skolem -- This type variable is a skolem constant
- -- Don't bind it; it only matches itself
-
- | WildCard -- This type variable matches anything,
- -- and does not affect the substitution
-
-newtype UM a = UM { unUM :: (TyVar -> BindFlag)
- -> MaybeErr Message a }
-
-instance Monad UM where
- return a = UM (\tvs -> Succeeded a)
- fail s = UM (\tvs -> Failed (text s))
- m >>= k = UM (\tvs -> case unUM m tvs of
- Failed err -> Failed err
- Succeeded v -> unUM (k v) tvs)
-
-initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
-initUM badtvs um = unUM um badtvs
-
-tvBindFlag :: TyVar -> UM BindFlag
-tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
-
-failWith :: Message -> UM a
-failWith msg = UM (\tv_fn -> Failed msg)
-
-maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
-maybeErrToMaybe (Succeeded a) = Just a
-maybeErrToMaybe (Failed m) = Nothing
-
-------------------------------
-repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
--- Like Type.splitAppTy_maybe, but any coreView stuff is already done
-repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
-repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
- Just (tys', ty') -> Just (TyConApp tc tys', ty')
- Nothing -> Nothing
-repSplitAppTy_maybe other = Nothing
-\end{code}
-
-
-%************************************************************************
-%* *
- Error reporting
- We go to a lot more trouble to tidy the types
- in TcUnify. Maybe we'll end up having to do that
- here too, but I'll leave it for now.
-%* *
-%************************************************************************
-
-\begin{code}
-misMatch t1 t2
- = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
- ptext SLIT("and") <+> quotes (ppr t2)
-
-lengthMisMatch tys1 tys2
- = sep [ptext SLIT("Can't match unequal length lists"),
- nest 2 (ppr tys1), nest 2 (ppr tys2) ]
-
-kindMisMatch tv1 t2
- = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
- ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
- ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
- ptext SLIT("with") <+> quotes (ppr t2)]
-
-occursCheck tv ty
- = hang (ptext SLIT("Can't construct the infinite type"))
- 2 (ppr tv <+> equals <+> ppr ty)
-\end{code}
\ No newline at end of file
projects / ghc-hetmet.git / commitdiff