[commit: ghc] master: Implement a typing rule for saturated seq, and document it (9789b03)

[Simon Peyton Jones]

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

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/9789b032e9ce7a5030d534847ec94e5398b38def

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

commit 9789b032e9ce7a5030d534847ec94e5398b38def
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Feb 17 13:57:47 2012 +0000

    Implement a typing rule for saturated seq, and document it
    Also add notes about unsafeCoerce
    
    The general thread here is to reduce use of ArgKind after
    the type checker; it is so fragile!

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

 compiler/basicTypes/MkId.lhs  |   37 ++++++++++++++++++++++++++++---------
 compiler/typecheck/TcExpr.lhs |   16 ++++++++++++++++
 2 files changed, 44 insertions(+), 9 deletions(-)

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index 60f4cf1..4671b39 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -881,11 +881,11 @@ unsafeCoerceId
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
            
 
-    ty  = mkForAllTys [argAlphaTyVar,openBetaTyVar]
-                      (mkFunTy argAlphaTy openBetaTy)
-    [x] = mkTemplateLocals [argAlphaTy]
-    rhs = mkLams [argAlphaTyVar,openBetaTyVar,x] $
-          Cast (Var x) (mkUnsafeCo argAlphaTy openBetaTy)
+    ty  = mkForAllTys [openAlphaTyVar,openBetaTyVar]
+                      (mkFunTy openAlphaTy openBetaTy)
+    [x] = mkTemplateLocals [openAlphaTy]
+    rhs = mkLams [openAlphaTyVar,openBetaTyVar,x] $
+          Cast (Var x) (mkUnsafeCo openAlphaTy openBetaTy)
 
 ------------------------------------------------
 nullAddrId :: Id
@@ -906,10 +906,12 @@ seqId = pcMiscPrelId seqName ty info
                        `setSpecInfo`       mkSpecInfo [seq_cast_rule]
            
 
-    ty  = mkForAllTys [alphaTyVar,argBetaTyVar]
-                      (mkFunTy alphaTy (mkFunTy argBetaTy argBetaTy))
-    [x,y] = mkTemplateLocals [alphaTy, argBetaTy]
-    rhs = mkLams [alphaTyVar,argBetaTyVar,x,y] (Case (Var x) x argBetaTy [(DEFAULT, [], Var y)])
+    ty  = mkForAllTys [alphaTyVar,betaTyVar]
+                      (mkFunTy alphaTy (mkFunTy betaTy betaTy))
+              -- NB argBetaTyVar; see Note [seqId magic]
+
+    [x,y] = mkTemplateLocals [alphaTy, betaTy]
+    rhs = mkLams [alphaTyVar,betaTyVar,x,y] (Case (Var x) x betaTy [(DEFAULT, [], Var y)])
 
     -- See Note [Built-in RULES for seq]
     seq_cast_rule = BuiltinRule { ru_name  = fsLit "seq of cast"
@@ -933,12 +935,29 @@ lazyId = pcMiscPrelId lazyIdName ty info
     ty  = mkForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
 \end{code}
 
+Note [Unsafe coerce magic]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We define a *primitive*
+   GHC.Prim.unsafeCoerce#
+and then in the base library we define the ordinary function
+   Unsafe.Coerce.unsafeCoerce :: forall (a:*) (b:*). a -> b
+   unsafeCoerce x = unsafeCoerce# x
+
+Notice that unsafeCoerce has a civilized (albeit still dangerous)
+polymorphic type, whose type args have kind *.  So you can't use it on
+unboxed values (unsafeCoerce 3#).
+
+In contrast unsafeCoerce# is even more dangerous because you *can* use
+it on unboxed things, (unsafeCoerce# 3#) :: Int. Its type is
+   forall (a:OpenKind) (b:OpenKind). a -> b
+
 Note [seqId magic]
 ~~~~~~~~~~~~~~~~~~
 'GHC.Prim.seq' is special in several ways. 
 
 a) Its second arg can have an unboxed type
       x `seq` (v +# w)
+   Hence its second type variable has ArgKind
 
 b) Its fixity is set in LoadIface.ghcPrimIface
 
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index fb6ca80..488e654 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -832,6 +832,10 @@ tcApp (L loc (HsVar fun)) args res_ty
   , [arg] <- args
   = tcTagToEnum loc fun arg res_ty
 
+  | fun `hasKey` seqIdKey
+  , [arg1,arg2] <- args
+  = tcSeq loc fun arg1 arg2 res_ty
+
 tcApp fun args res_ty
   = do	{   -- Type-check the function
 	; (fun1, fun_tau) <- tcInferFun fun
@@ -1118,6 +1122,18 @@ constructors of F [Int] but here we have to do it explicitly.
 It's all grotesquely complicated.
 
 \begin{code}
+tcSeq :: SrcSpan -> Name -> LHsExpr Name -> LHsExpr Name 
+      -> TcRhoType -> TcM (HsExpr TcId)
+-- (seq e1 e2) :: res_ty
+-- We need a special typing rule because res_ty can be unboxed
+tcSeq loc fun_name arg1 arg2 res_ty
+  = do	{ fun <- tcLookupId fun_name
+        ; (arg1', arg1_ty) <- tcInfer (tcMonoExpr arg1)
+        ; arg2' <- tcMonoExpr arg2 res_ty
+        ; let fun'    = L loc (HsWrap ty_args (HsVar fun))
+              ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
+        ; return (HsApp (L loc (HsApp fun' arg1')) arg2') }
+
 tcTagToEnum :: SrcSpan -> Name -> LHsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
 -- tagToEnum# :: forall a. Int# -> a
 -- See Note [tagToEnum#]   Urgh!