[commit: ghc] supercompiler: Fix newtype unfoldings (coercion direction) and prevent data unfoldings with strange tyvar kinds (d54e4c5)

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : supercompiler

http://hackage.haskell.org/trac/ghc/changeset/d54e4c5e73caadb53fe53b5e7a4a71579476746b

>---------------------------------------------------------------

commit d54e4c5e73caadb53fe53b5e7a4a71579476746b
Author: Max Bolingbroke <[email protected]>
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