From c76c69c5b62f1ca4fa52d75b0dfbd37b7eddbb09 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Fri, 4 Aug 2006 22:23:51 +0000 Subject: [PATCH] Massive patch for the first months work adding System FC to GHC #35 Broken up massive patch -=chak Original log message: This is (sadly) all done in one patch to avoid Darcs bugs. It's not complete work... more FC stuff to come. A compiler using just this patch will fail dismally. --- compiler/types/Class.lhs | 12 +- compiler/types/FunDeps.lhs | 17 +- compiler/types/InstEnv.lhs | 40 +--- compiler/types/Kind.lhs | 237 ---------------------- compiler/types/TyCon.lhs | 154 +++++++++++--- compiler/types/Type.lhs | 423 +++++++++++++++++++++++++++++++-------- compiler/types/TypeRep.lhs | 149 ++++++++++++-- compiler/types/TypeRep.lhs-boot | 11 + compiler/types/Unify.lhs | 369 +--------------------------------- 9 files changed, 627 insertions(+), 785 deletions(-) delete mode 100644 compiler/types/Kind.lhs diff --git a/compiler/types/Class.lhs b/compiler/types/Class.lhs index 016ce1b..fb6b901 100644 --- a/compiler/types/Class.lhs +++ b/compiler/types/Class.lhs @@ -5,9 +5,11 @@ \begin{code} module Class ( - Class, ClassOpItem, FunDep, + Class, ClassOpItem, DefMeth (..), + FunDep, pprFundeps, + mkClass, classTyVars, classArity, classKey, className, classSelIds, classTyCon, classMethods, classBigSig, classExtraBigSig, classTvsFds, classSCTheta @@ -159,6 +161,12 @@ instance Outputable DefMeth where 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} diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs index 7000075..1534dc6 100644 --- a/compiler/types/FunDeps.lhs +++ b/compiler/types/FunDeps.lhs @@ -17,8 +17,8 @@ module FunDeps ( 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 ) @@ -485,17 +485,4 @@ trimRoughMatchTcs clas_tvs (ltvs,_) mb_tcs \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} diff --git a/compiler/types/InstEnv.lhs b/compiler/types/InstEnv.lhs index 70e6166..7aaf6dd 100644 --- a/compiler/types/InstEnv.lhs +++ b/compiler/types/InstEnv.lhs @@ -33,8 +33,10 @@ import TcType ( Type, PredType, tcEqType, 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 ) @@ -61,7 +63,8 @@ data Instance , 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 } @@ -213,39 +216,6 @@ instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool -- 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} diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs deleted file mode 100644 index 79999c2..0000000 --- a/compiler/types/Kind.lhs +++ /dev/null @@ -1,237 +0,0 @@ -% -% (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} diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 34848c8..479ea7c 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -14,12 +14,13 @@ module TyCon( 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, @@ -29,9 +30,12 @@ module TyCon( mkClassTyCon, mkFunTyCon, mkPrimTyCon, + mkVoidPrimTyCon, mkLiftedPrimTyCon, mkTupleTyCon, mkSynTyCon, + mkSuperKindTyCon, + mkCoercionTyCon, tyConName, tyConKind, @@ -54,16 +58,11 @@ module TyCon( #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(..) ) @@ -102,6 +101,10 @@ data TyCon 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) @@ -117,8 +120,33 @@ data TyCon -- 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, @@ -134,29 +162,23 @@ data TyCon 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 @@ -183,6 +205,11 @@ data AlgTyConRhs 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 @@ -211,6 +238,20 @@ visibleDataCons (DataTyCon{ data_cons = cs }) = cs 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 @@ -304,7 +345,7 @@ mkFunTyCon name kind -- 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, @@ -317,6 +358,7 @@ mkAlgTyCon name kind tyvars argvrcs stupid rhs sel_ids is_rec gen_info algTcSelIds = sel_ids, algTcClass = Nothing, algTcRec = is_rec, + algTcGadtSyntax = gadt_syn, hasGenerics = gen_info } @@ -333,6 +375,7 @@ mkClassTyCon name kind tyvars argvrcs rhs clas is_rec algTcSelIds = [], algTcClass = Just clas, algTcRec = is_rec, + algTcGadtSyntax = False, -- Doesn't really matter hasGenerics = False } @@ -370,6 +413,9 @@ mkForeignTyCon name ext_name kind arity arg_vrcs 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 @@ -396,6 +442,21 @@ mkSynTyCon name kind tyvars rhs argvrcs 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} @@ -467,6 +528,10 @@ isSynTyCon :: TyCon -> Bool 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 @@ -506,6 +571,18 @@ isForeignTyCon :: TyCon -> Bool -- 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} @@ -527,15 +604,26 @@ tcExpandTyCon_maybe (SynTyCon {tyConTyVars = tvs, synTcRhs = rhs }) tys 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 @@ -593,6 +681,10 @@ newTyConRep :: TyCon -> ([TyVar], Type) 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 diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index fdcec30..ccabfb7 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -3,21 +3,40 @@ % \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, @@ -25,9 +44,10 @@ module Type ( 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, @@ -74,7 +94,7 @@ module Type ( -- Pretty-printing pprType, pprParendType, pprTyThingCategory, - pprPred, pprTheta, pprThetaArrow, pprClassPred + pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind ) where #include "HsVersions.h" @@ -85,20 +105,27 @@ module Type ( 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 @@ -122,7 +149,7 @@ In Core, we "look through" non-recursive newtypes and PredTypes. \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. -- @@ -150,6 +177,21 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc -- 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 @@ -158,6 +200,14 @@ tcView (NoteTy _ ty) = Just ty 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} @@ -190,6 +240,7 @@ getTyVar_maybe :: Type -> Maybe TyVar getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty' getTyVar_maybe (TyVarTy tv) = Just tv getTyVar_maybe other = Nothing + \end{code} @@ -231,20 +282,28 @@ mkAppTys orig_ty1 orig_tys2 -- 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 @@ -254,6 +313,7 @@ splitAppTys ty = split ty ty [] split orig_ty (FunTy ty1 ty2) args = ASSERT( null args ) (TyConApp funTyCon [], [ty1,ty2]) split orig_ty ty args = (orig_ty, args) + \end{code} @@ -354,6 +414,20 @@ splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty' 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} @@ -396,8 +470,7 @@ repType (TyConApp tc tys) -- 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 @@ -560,6 +633,9 @@ splitRecNewType_maybe (TyConApp tc tys) Just (substTyWith tvs tys rep_ty) splitRecNewType_maybe other = Nothing + + + \end{code} @@ -574,15 +650,30 @@ splitRecNewType_maybe other = Nothing ~~~~~~~~~~~~~~~~~~~~~~~~~~ \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} @@ -699,42 +790,11 @@ tidyTopType :: Type -> Type 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} @@ -867,8 +927,8 @@ coreEqType t1 t2 -- 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 @@ -1167,6 +1227,7 @@ substTheta subst theta 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 @@ -1174,6 +1235,9 @@ 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 @@ -1196,37 +1260,218 @@ 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} diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs index 7bb863a..5625f8e 100644 --- a/compiler/types/TypeRep.lhs +++ b/compiler/types/TypeRep.lhs @@ -17,29 +17,51 @@ module TypeRep ( 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} @@ -177,6 +199,19 @@ data Type 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} @@ -204,6 +239,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) type ThetaType = [PredType] \end{code} @@ -256,13 +292,16 @@ instance NamedThing TyThing where -- Can't put this with the type %************************************************************************ %* * -\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 @@ -272,15 +311,89 @@ funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] lif -- 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} @@ -312,6 +425,7 @@ pprParendType ty = ppr_type TyConPrec ty 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) @@ -338,6 +452,9 @@ instance Outputable name => OutputableBndr (IPName name) where ------------------ -- OK, here's the main printer +pprKind = pprType +pprParendKind = pprParendType + ppr_type :: Prec -> Type -> SDoc ppr_type p (TyVarTy tv) = ppr tv ppr_type p (PredTy pred) = braces (ppr pred) @@ -382,6 +499,12 @@ ppr_tc_app p tc [] ppr_tc_app p tc [ty] | tc `hasKey` listTyConKey = brackets (pprType ty) | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]") + | tc `hasKey` liftedTypeKindTyConKey = ptext SLIT("*") + | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#") + | tc `hasKey` openTypeKindTyConKey = ptext SLIT("(?)") + | tc `hasKey` ubxTupleKindTyConKey = ptext SLIT("(#)") + | tc `hasKey` argTypeKindTyConKey = ptext SLIT("??") + ppr_tc_app p tc tys | isTupleTyCon tc && tyConArity tc == length tys = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys))) diff --git a/compiler/types/TypeRep.lhs-boot b/compiler/types/TypeRep.lhs-boot index b99fdd3..376aa68 100644 --- a/compiler/types/TypeRep.lhs-boot +++ b/compiler/types/TypeRep.lhs-boot @@ -1,8 +1,19 @@ \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} diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index b96f207..9f5b405 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -1,16 +1,9 @@ \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" @@ -18,12 +11,11 @@ module Unify ( 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 @@ -196,352 +188,3 @@ match_pred menv subst p1 p2 = Nothing \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 -- 1.7.10.4