This BIG PATCH contains most of the work for the New Coercion Representation

See the paper "Practical aspects of evidence based compilation in System FC"

* Coercion becomes a data type, distinct from Type

* Coercions become value-level things, rather than type-level things,
  (although the value is zero bits wide, like the State token)
  A consequence is that a coerion abstraction increases the arity by 1
  (just like a dictionary abstraction)

* There is a new constructor in CoreExpr, namely Coercion, to inject
  coercions into terms

2 files changed, 29 insertions, 5 deletions

diff --git a/compiler/stgSyn/CoreToStg.lhs b/compiler/stgSyn/CoreToStg.lhs
index 2059937e0b..fc7550fe01 100644
--- a/compiler/stgSyn/CoreToStg.lhs
+++ b/compiler/stgSyn/CoreToStg.lhs
@@ -18,8 +18,8 @@ import StgSyn
 
 import Type
 import TyCon
+import MkId		( coercionTokenId )
 import Id
-import Var              ( Var )
 import IdInfo
 import DataCon
 import CostCentre       ( noCCS )
@@ -218,7 +218,7 @@ coreTopBindToStg this_pkg env body_fvs (Rec pairs)
 -- floated out a binding, in which case it will be approximate.
 consistentCafInfo :: Id -> GenStgBinding Var Id -> Bool
 consistentCafInfo id bind
-  = WARN( not (exact || is_sat_thing) , ppr id )
+  = WARN( not (exact || is_sat_thing) , ppr id <+> ppr id_marked_caffy <+> ppr binding_is_caffy )
     safe
   where
     safe  = id_marked_caffy || not binding_is_caffy
@@ -572,6 +572,10 @@ coreToStgArgs (Type _ : args) = do     -- Type argument
     (args', fvs) <- coreToStgArgs args
     return (args', fvs)
 
+coreToStgArgs (Coercion _ : args)  -- Coercion argument; replace with place holder
+  = do { (args', fvs) <- coreToStgArgs args
+       ; return (StgVarArg coercionTokenId : args', fvs) }
+
 coreToStgArgs (arg : args) = do         -- Non-type argument
     (stg_args, args_fvs) <- coreToStgArgs args
     (arg', arg_fvs, _escs) <- coreToStgExpr arg
@@ -1124,7 +1128,7 @@ myCollectArgs expr
     go (Cast e _)       as = go e as
     go (Note _ e)       as = go e as
     go (Lam b e)        as
-       | isTyCoVar b         = go e as  -- Note [Collect args]
+       | isTyVar b         = go e as  -- Note [Collect args]
     go _                _  = pprPanic "CoreToStg.myCollectArgs" (ppr expr)
 \end{code}
 
diff --git a/compiler/stgSyn/StgSyn.lhs b/compiler/stgSyn/StgSyn.lhs
index 3bce28148a..dd026eb80c 100644
--- a/compiler/stgSyn/StgSyn.lhs
+++ b/compiler/stgSyn/StgSyn.lhs
@@ -68,7 +68,8 @@ import FastString
 
 #if mingw32_TARGET_OS
 import Packages		( isDllName )
-
+import Type		( typePrimRep )
+import TyCon		( PrimRep(..) )
 #endif
 \end{code}
 
@@ -118,8 +119,27 @@ isDllConApp this_pkg con args
   = isDllName this_pkg (dataConName con) || any is_dll_arg args
   where
     is_dll_arg ::StgArg -> Bool
-    is_dll_arg (StgVarArg v) = isDllName this_pkg (idName v)
+    is_dll_arg (StgVarArg v) =  isAddrRep (typePrimRep (idType v))
+                             && isDllName this_pkg (idName v)
     is_dll_arg _             = False
+
+isAddrRep :: PrimRep -> Bool
+-- True of machine adddresses; these are the things that don't
+-- work across DLLs.
+-- The key point here is that VoidRep comes out False, so that
+-- a top level nullary GADT construtor is False for isDllConApp
+--    data T a where
+--      T1 :: T Int
+-- gives
+--    T1 :: forall a. (a~Int) -> T a
+-- and hence the top-level binding
+--    $WT1 :: T Int
+--    $WT1 = T1 Int (Coercion (Refl Int))
+-- The coercion argument here gets VoidRep
+isAddrRep AddrRep = True
+isAddrRep PtrRep  = True
+isAddrRep _       = False
+
 #else
 isDllConApp _ _ _ = False
 #endif