Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : supercompiler
http://hackage.haskell.org/trac/ghc/changeset/d54e4c5e73caadb53fe53b5e7a4a71579476746b >--------------------------------------------------------------- commit d54e4c5e73caadb53fe53b5e7a4a71579476746b Author: Max Bolingbroke <batterseapo...@hotmail.com> Date: Tue Oct 23 17:56:26 2012 +0100 Fix newtype unfoldings (coercion direction) and prevent data unfoldings with strange tyvar kinds >--------------------------------------------------------------- compiler/supercompile/Supercompile.hs | 11 +++++++---- compiler/supercompile/Supercompile/Core/Syntax.hs | 20 ++++++++++++++++++++ compiler/supercompile/Supercompile/Drive/MSG.hs | 19 ------------------- 3 files changed, 27 insertions(+), 23 deletions(-) diff --git a/compiler/supercompile/Supercompile.hs b/compiler/supercompile/Supercompile.hs index 573c308..e577c62 100644 --- a/compiler/supercompile/Supercompile.hs +++ b/compiler/supercompile/Supercompile.hs @@ -30,9 +30,10 @@ import CoreSyn import CoreFVs (exprFreeVars) import CoreUtils (exprType) import MkCore (mkWildValBinder) -import Coercion (isCoVar, mkCoVarCo, mkAxInstCo) +import Coercion (isCoVar, mkCoVarCo, mkAxInstCo, mkSymCo) import DataCon (dataConAllTyVars, dataConRepArgTys, dataConTyCon, dataConWorkId) import VarSet +import Var (tyVarKind) import Id import MkId (realWorldPrimId) import FastString (fsLit) @@ -175,7 +176,7 @@ termUnfoldings e = go (S.termFreeVars e) emptyVarSet [] [] -- which can literall never be used. varUnfolding x | Just pop <- isPrimOpId_maybe x = Right $ primOpUnfolding pop - | Just dc <- isDataConWorkId_maybe x = Right $ dataUnfolding dc + | Just dc <- isDataConWorkId_maybe x = dataUnfolding dc | otherwise = case S.shouldExposeUnfolding x of Left why_not -> Left why_not Right super -> case realIdUnfolding x of @@ -194,9 +195,11 @@ termUnfoldings e = go (S.termFreeVars e) emptyVarSet [] [] dataUnfolding dc | Just co_axiom <- newTyConCo_maybe (dataConTyCon dc) , let [x] = xs - = S.tyLambdas as $ S.lambdas [x] $ S.var x `S.cast` mkAxInstCo co_axiom (map mkTyVarTy as) + = Right $ S.tyLambdas as $ S.lambdas [x] $ S.var x `S.cast` mkSymCo (mkAxInstCo co_axiom (map mkTyVarTy as)) -- Axiom LHS = TyCon, RHS = Rep Type + | any (not . S.canAbstractOverTyVarOfKind . tyVarKind) as + = Left "some type variable which we cannot abstract over" | otherwise - = S.tyLambdas as $ S.lambdas xs $ S.value (S.Data dc (map mkTyVarTy as) (map mkCoVarCo qs) ys) + = Right $ S.tyLambdas as $ S.lambdas xs $ S.value (S.Data dc (map mkTyVarTy as) (map mkCoVarCo qs) ys) where as = dataConAllTyVars dc arg_tys = dataConRepArgTys dc xs = zipWith (mkSysLocal (fsLit "x")) bv_uniques arg_tys diff --git a/compiler/supercompile/Supercompile/Core/Syntax.hs b/compiler/supercompile/Supercompile/Core/Syntax.hs index 1bc8fcb..f818383 100644 --- a/compiler/supercompile/Supercompile/Core/Syntax.hs +++ b/compiler/supercompile/Supercompile/Core/Syntax.hs @@ -272,6 +272,26 @@ mkTransCastBy _ cast_by1 Uncast = cast_by1 mkTransCastBy ids (CastBy co1 _tg1) (CastBy co2 tg2) = castBy (mkTransCo ids co1 co2) tg2 +canAbstractOverTyVarOfKind :: Kind -> Bool +canAbstractOverTyVarOfKind = ok + where + -- TODO: I'm not 100% sure of the correctness of this check + -- In particular, I don't think we need to check for non-conforming + -- kinds in "negative" positions since they would only appear if the + -- definition site had erroneously abstracted over a non-conforming + -- kind. For example, this *should* never be allowed: + -- data Foo (a :: * -> #) = Bar (a Int) + -- Foo :: (* -> #) -> * + -- Bar :: forall (a :: * -> #). a Int -> Foo a + ok k | isOpenTypeKind k || isUbxTupleKind k || isArgTypeKind k || isUnliftedTypeKind k = False + ok (TyVarTy _) = True -- This is OK because kinds dont get generalised, and we assume all incoming kind instantiations satisfy the kind invariant + ok (AppTy k1 k2) = ok k1 && ok k2 + ok (TyConApp _ ks) = all ok ks + ok (FunTy k1 k2) = ok k1 && ok k2 + ok (ForAllTy _ k) = ok k + ok (LitTy _) = True + + valueType :: Copointed ann => ValueF ann -> Type valueType (TyLambda a e) = mkForAllTy a (termType e) valueType (Lambda x e) = idType x `mkFunTy` termType e diff --git a/compiler/supercompile/Supercompile/Drive/MSG.hs b/compiler/supercompile/Supercompile/Drive/MSG.hs index 935d48f..57e4d60 100644 --- a/compiler/supercompile/Supercompile/Drive/MSG.hs +++ b/compiler/supercompile/Supercompile/Drive/MSG.hs @@ -828,25 +828,6 @@ msgCoerced _ _ _ _ _ _ = fail "msgCoerced" msgKind :: RnEnv2 -> Kind -> Kind -> MSG Kind msgKind = msgType -canAbstractOverTyVarOfKind :: Kind -> Bool -canAbstractOverTyVarOfKind = ok - where - -- TODO: I'm not 100% sure of the correctness of this check - -- In particular, I don't think we need to check for non-conforming - -- kinds in "negative" positions since they would only appear if the - -- definition site had erroneously abstracted over a non-conforming - -- kind. For example, this *should* never be allowed: - -- data Foo (a :: * -> #) = Bar (a Int) - -- Foo :: (* -> #) -> * - -- Bar :: forall (a :: * -> #). a Int -> Foo a - ok k | isOpenTypeKind k || isUbxTupleKind k || isArgTypeKind k || isUnliftedTypeKind k = False - ok (TyVarTy _) = True -- This is OK because kinds dont get generalised, and we assume all incoming kind instantiations satisfy the kind invariant - ok (AppTy k1 k2) = ok k1 && ok k2 - ok (TyConApp _ ks) = all ok ks - ok (FunTy k1 k2) = ok k1 && ok k2 - ok (ForAllTy _ k) = ok k - ok (LitTy _) = True - -- NB: we don't match FunTy and TyConApp literally because -- we can do better MSG for combinations like: -- Either Int Char `msg` Maybe Char _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
