From: Manuel M T Chakravarty Date: Wed, 20 Sep 2006 17:38:56 +0000 (+0000) Subject: fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla X-Git-Tag: After_FC_branch_merge~79 X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=6fcf90065dc4e75b7dc6bbf238a9891a71ae5a86;ds=sidebyside fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla Mon Sep 18 14:51:33 EDT 2006 Manuel M T Chakravarty * fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla Sat Aug 5 21:48:21 EDT 2006 Manuel M T Chakravarty * fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla Wed Jul 19 08:06:28 EDT 2006 kevind@bu.edu --- diff --git a/compiler/Makefile b/compiler/Makefile index 43622c3..e81ccfb 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -411,7 +411,7 @@ endif ifeq "$(GhcWithInterpreter) $(bootstrapped)" "YES YES" # Yes, include the interepreter, readline, and Template Haskell extensions -SRC_HC_OPTS += -DGHCI -DBREAKPOINT -package template-haskell +SRC_HC_OPTS += -DGHCI -package template-haskell PKG_DEPENDS += template-haskell # Use threaded RTS with GHCi, so threads don't get blocked at the prompt. diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index 0a1902e..1c25d81 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/compiler/basicTypes/MkId.lhs @@ -48,7 +48,7 @@ import TysWiredIn ( charTy, mkListTy ) import PrelRules ( primOpRules ) import Type ( TyThing(..), mkForAllTy, tyVarsOfTypes, newTyConInstRhs, coreEqType ) import Coercion ( mkSymCoercion, mkUnsafeCoercion, - splitRecNewTypeCo_maybe ) + splitNewTypeRepCo_maybe ) import TcType ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy, mkTyConApp, mkTyVarTys, mkClassPred, mkFunTys, mkFunTy, mkSigmaTy, tcSplitSigmaTy, diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index 697f089..e4aa8c2 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -10,7 +10,7 @@ module Var ( setVarName, setVarUnique, -- TyVars - TyVar, mkTyVar, mkTcTyVar, + TyVar, mkTyVar, mkTcTyVar, mkWildTyVar, tyVarName, tyVarKind, setTyVarName, setTyVarUnique, setTyVarKind, tcTyVarDetails, @@ -40,9 +40,10 @@ import {-# SOURCE #-} TcType( TcTyVarDetails, pprTcTyVarDetails ) import {-# SOURCE #-} IdInfo( GlobalIdDetails, notGlobalId, IdInfo, seqIdInfo ) import Name ( Name, NamedThing(..), - setNameUnique, nameUnique + setNameUnique, nameUnique, mkSysTvName ) -import Unique ( Unique, Uniquable(..), mkUniqueGrimily, getKey# ) +import Unique ( Unique, Uniquable(..), mkUniqueGrimily, getKey#, + mkBuiltinUnique ) import FastTypes import Outputable \end{code} @@ -197,6 +198,14 @@ mkTcTyVar name kind details tyVarKind = kind, tcTyVarDetails = details } + +mkWildTyVar :: Kind -> TyVar +mkWildTyVar kind + = TyVar { varName = mkSysTvName wild_uniq FSLIT("co_wild"), + realUnique = _ILIT(1), + tyVarKind = kind } + where + wild_uniq = (mkBuiltinUnique 1) \end{code} %************************************************************************ diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index 9b58159..19a44dc 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -42,7 +42,7 @@ import GLAEXTS -- For `xori` import CoreSyn import CoreFVs ( exprFreeVars ) import PprCore ( pprCoreExpr ) -import Var ( Var, TyVar ) +import Var ( Var, TyVar, isCoVar, tyVarKind ) import VarSet ( unionVarSet ) import VarEnv import Name ( hashName ) @@ -53,7 +53,7 @@ import Literal ( hashLiteral, literalType, litIsDupable, litIsTrivial, isZeroLit, Literal( MachLabel ) ) import DataCon ( DataCon, dataConRepArity, isVanillaDataCon, dataConTyCon, dataConRepArgTys, - dataConUnivTyVars ) + dataConUnivTyVars, dataConExTyVars ) import PrimOp ( PrimOp(..), primOpOkForSpeculation, primOpIsCheap ) import Id ( Id, idType, globalIdDetails, idNewStrictness, mkWildId, idArity, idName, idUnfolding, idInfo, @@ -70,8 +70,9 @@ import Type ( Type, mkFunTy, mkForAllTy, splitFunTy_maybe, substTyWith ) import Coercion ( Coercion, mkTransCoercion, coercionKind, - splitRecNewTypeCo_maybe, mkSymCoercion, mkLeftCoercion, - mkRightCoercion, decomposeCo, coercionKindTyConApp ) + splitNewTypeRepCo_maybe, mkSymCoercion, mkLeftCoercion, + mkRightCoercion, decomposeCo, coercionKindTyConApp, + splitCoercionKind ) import TyCon ( tyConArity ) import TysWiredIn ( boolTy, trueDataCon, falseDataCon ) import CostCentre ( CostCentre ) @@ -687,30 +688,62 @@ exprIsConApp_maybe (Cast expr co) -- (# r, s #) -> ... -- where the memcpy is in the IO monad, but the call is in -- the (ST s) monad - let (from_ty, to_ty) = coercionKind co in case exprIsConApp_maybe expr of { Nothing -> Nothing ; Just (dc, args) -> + + let (from_ty, to_ty) = coercionKind co in case splitTyConApp_maybe to_ty of { Nothing -> Nothing ; Just (tc, tc_arg_tys) | tc /= dataConTyCon dc -> Nothing - | not (isVanillaDataCon dc) -> Nothing + -- | not (isVanillaDataCon dc) -> Nothing | otherwise -> - -- Type constructor must match - -- We knock out existentials to keep matters simple(r) + -- Type constructor must match datacon + + case splitTyConApp_maybe from_ty of { + Nothing -> Nothing ; + Just (tc', tc_arg_tys') | tc /= tc' -> Nothing + -- Both sides of coercion must have the same type constructor + | otherwise -> + let + -- here we do the PushC reduction rule as described in the FC paper arity = tyConArity tc - val_args = drop arity args + n_ex_tvs = length dc_ex_tyvars + + (univ_args, rest) = splitAt arity args + (ex_args, val_args) = splitAt n_ex_tvs rest + arg_tys = dataConRepArgTys dc dc_tyvars = dataConUnivTyVars dc + dc_ex_tyvars = dataConExTyVars dc + deep arg_ty = deepCast arg_ty dc_tyvars co + + -- first we appropriately cast the value arguments + arg_cos = map deep arg_tys new_val_args = zipWith mkCoerce (map deep arg_tys) val_args + + -- then we cast the existential coercion arguments + orig_tvs = dc_tyvars ++ dc_ex_tyvars + gammas = decomposeCo arity co + new_tys = gammas ++ (map (\ (Type t) -> t) ex_args) + theta = substTyWith orig_tvs new_tys + cast_ty tv (Type ty) + | isCoVar tv + , (ty1, ty2) <- splitCoercionKind (tyVarKind tv) + = Type $ mkTransCoercion (mkSymCoercion (theta ty1)) + (mkTransCoercion ty (theta ty2)) + | otherwise + = Type ty + new_ex_args = zipWith cast_ty dc_ex_tyvars ex_args + in ASSERT( all isTypeArg (take arity args) ) ASSERT( equalLength val_args arg_tys ) - Just (dc, map Type tc_arg_tys ++ new_val_args) - }} + Just (dc, map Type tc_arg_tys ++ new_ex_args ++ new_val_args) + }}} exprIsConApp_maybe (Note _ expr) = exprIsConApp_maybe expr @@ -1047,7 +1080,7 @@ eta_expand n us expr ty -- We want to get -- coerce T (\x::[T] -> (coerce ([T]->Int) e) x) - case splitRecNewTypeCo_maybe ty of { + case splitNewTypeRepCo_maybe ty of { Just(ty1,co) -> mkCoerce co (eta_expand n us (mkCoerce (mkSymCoercion co) expr) ty1) ; Nothing -> diff --git a/compiler/deSugar/DsCCall.lhs b/compiler/deSugar/DsCCall.lhs index 0541f5d..4fe5f2d 100644 --- a/compiler/deSugar/DsCCall.lhs +++ b/compiler/deSugar/DsCCall.lhs @@ -34,7 +34,7 @@ import Type ( Type, isUnLiftedType, mkFunTys, mkFunTy, splitRecNewType_maybe, splitForAllTy_maybe, isUnboxedTupleType ) -import Coercion ( Coercion, splitRecNewTypeCo_maybe, mkSymCoercion ) +import Coercion ( Coercion, splitNewTypeRepCo_maybe, mkSymCoercion ) import PrimOp ( PrimOp(..) ) import TysPrim ( realWorldStatePrimTy, intPrimTy, byteArrayPrimTyCon, mutableByteArrayPrimTyCon, @@ -160,7 +160,7 @@ unboxArg arg = returnDs (arg, \body -> body) -- Recursive newtypes - | Just(rep_ty, co) <- splitRecNewTypeCo_maybe arg_ty + | Just(rep_ty, co) <- splitNewTypeRepCo_maybe arg_ty = unboxArg (mkCoerce (mkSymCoercion co) arg) -- Booleans @@ -399,7 +399,7 @@ resultWrapper result_ty (LitAlt (mkMachInt 0),[],Var falseDataConId)]) -- Recursive newtypes - | Just (rep_ty, co) <- splitRecNewTypeCo_maybe result_ty + | Just (rep_ty, co) <- splitNewTypeRepCo_maybe result_ty = resultWrapper rep_ty `thenDs` \ (maybe_ty, wrapper) -> returnDs (maybe_ty, \e -> mkCoerce co (wrapper e)) diff --git a/compiler/simplCore/Simplify.lhs b/compiler/simplCore/Simplify.lhs index 85b4b49..f9cc644 100644 --- a/compiler/simplCore/Simplify.lhs +++ b/compiler/simplCore/Simplify.lhs @@ -1696,7 +1696,7 @@ knownCon env scrut con args bndr alts cont simplExprF env rhs cont (DataAlt dc, bs, rhs) - -> ASSERT( n_drop_tys + length bs == length args ) + -> -- ASSERT( n_drop_tys + length bs == length args ) bind_args env dead_bndr bs (drop n_drop_tys args) $ \ env -> let -- It's useful to bind bndr to scrut, rather than to a fresh diff --git a/compiler/stranal/WwLib.lhs b/compiler/stranal/WwLib.lhs index 5896785..386c9e1 100644 --- a/compiler/stranal/WwLib.lhs +++ b/compiler/stranal/WwLib.lhs @@ -23,7 +23,7 @@ import TysWiredIn ( tupleCon ) import Type ( Type, isUnLiftedType, mkFunTys, splitForAllTys, splitFunTys, splitRecNewType_maybe, isAlgType ) -import Coercion ( Coercion, mkSymCoercion, splitRecNewTypeCo_maybe ) +import Coercion ( Coercion, mkSymCoercion, splitNewTypeRepCo_maybe ) import BasicTypes ( Boxity(..) ) import Var ( Var, isId ) import UniqSupply ( returnUs, thenUs, getUniquesUs, UniqSM ) @@ -225,7 +225,7 @@ mkWWargs :: Type Type) -- Type of wrapper body mkWWargs fun_ty demands one_shots - | Just (rep_ty, co) <- splitRecNewTypeCo_maybe fun_ty + | Just (rep_ty, co) <- splitNewTypeRepCo_maybe fun_ty -- The newtype case is for when the function has -- a recursive newtype after the arrow (rare) -- We check for arity >= 0 to avoid looping in the case diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index bda4e2f..c0a9294 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -54,7 +54,7 @@ import {- Kind parts of -} import Id ( Id, idType, recordSelectorFieldLabel, isRecordSelector, isNaughtyRecordSelector, - isDataConId_maybe ) + isDataConId_maybe, idName ) import DataCon ( DataCon, dataConFieldLabels, dataConStrictMarks, dataConSourceArity, dataConWrapId, isVanillaDataCon, dataConUnivTyVars, diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index 55e20fc..727d0ab 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -170,9 +170,10 @@ import Type ( -- Re-exports pprPred, pprTheta, pprThetaArrow, pprClassPred ) import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique ) +import Coercion ( splitForAllCo_maybe ) import DataCon ( DataCon, dataConStupidTheta, dataConResTys ) import Class ( Class ) -import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails ) +import Var ( TyVar, Id, isCoVar, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails ) import ForeignCall ( Safety, DNType(..) ) import Unify ( tcMatchTys ) import VarSet @@ -642,7 +643,8 @@ tcSplitForAllTys :: Type -> ([TyVar], Type) tcSplitForAllTys ty = split ty ty [] where split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs - split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs) + split orig_ty (ForAllTy tv ty) tvs + | not (isCoVar tv) = split ty ty (tv:tvs) split orig_ty t tvs = (reverse tvs, orig_ty) tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty' @@ -655,6 +657,8 @@ tcSplitPhiTy ty = split ty ty [] split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs split orig_ty (FunTy arg res) ts | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts) + split orig_ty ty ts + | Just (p, ty') <- splitForAllCo_maybe ty = split ty' ty' (p:ts) split orig_ty ty ts = (reverse ts, orig_ty) tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type) diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index c3013ab..b7f521a 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -24,7 +24,7 @@ module Type ( isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, - isCoSuperKind, isSuperKind, isCoercionKind, + isCoSuperKind, isSuperKind, isCoercionKind, isEqPred, mkArrowKind, mkArrowKinds, isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind, @@ -106,7 +106,7 @@ import TypeRep -- friends: import Var ( Var, TyVar, tyVarKind, tyVarName, - setTyVarName, setTyVarKind ) + setTyVarName, setTyVarKind, mkWildTyVar ) import VarEnv import VarSet @@ -164,7 +164,9 @@ coreView :: Type -> Maybe Type -- By being non-recursive and inlined, this case analysis gets efficiently -- joined onto the case analysis that the caller is already doing coreView (NoteTy _ ty) = Just ty -coreView (PredTy p) = Just (predTypeRep p) +coreView (PredTy p) + | isEqPred p = Nothing + | otherwise = Just (predTypeRep p) coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys') -- Its important to use mkAppTys, rather than (foldl AppTy), @@ -305,10 +307,11 @@ splitAppTys ty = split ty ty [] \begin{code} mkFunTy :: Type -> Type -> Type +mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildTyVar (PredTy (EqPred ty1 ty2))) res mkFunTy arg res = FunTy arg res mkFunTys :: [Type] -> Type -> Type -mkFunTys tys ty = foldr FunTy ty tys +mkFunTys tys ty = foldr mkFunTy ty tys isFunTy :: Type -> Bool isFunTy ty = isJust (splitFunTy_maybe ty) @@ -596,6 +599,7 @@ predTypeRep (IParam _ ty) = ty predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys -- Result might be a newtype application, but the consumer will -- look through that too if necessary +predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2)) \end{code} @@ -1423,6 +1427,8 @@ 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 (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) + = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2' isSubKind k1 k2 = False eqKind :: Kind -> Kind -> Bool @@ -1465,4 +1471,8 @@ isCoercionKind :: Kind -> Bool isCoercionKind k | Just k' <- kindView k = isCoercionKind k' isCoercionKind (PredTy (EqPred {})) = True isCoercionKind other = False + +isEqPred :: PredType -> Bool +isEqPred (EqPred _ _) = True +isEqPred other = False \end{code}