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

3 files changed, 48 insertions, 23 deletions

diff --git a/compiler/specialise/Rules.lhs b/compiler/specialise/Rules.lhs
index 3205542c8e..f9d02e5ab7 100644
--- a/compiler/specialise/Rules.lhs
+++ b/compiler/specialise/Rules.lhs
@@ -37,10 +37,10 @@ import CoreUtils        ( exprType, eqExpr )
 import PprCore		( pprRules )
 import Type             ( Type )
 import TcType		( tcSplitTyConApp_maybe )
+import Coercion
 import CoreTidy		( tidyRules )
 import Id
 import IdInfo		( SpecInfo( SpecInfo ) )
-import Var		( Var )
 import VarEnv
 import VarSet
 import Name		( Name, NamedThing(..) )
@@ -56,7 +56,6 @@ import Util
 import Data.List
 \end{code}
 
-
 Note [Overall plumbing for rules]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * After the desugarer:
@@ -184,8 +183,9 @@ roughTopNames args = map roughTopName args
 
 roughTopName :: CoreExpr -> Maybe Name
 roughTopName (Type ty) = case tcSplitTyConApp_maybe ty of
-			  Just (tc,_) -> Just (getName tc)
-			  Nothing     -> Nothing
+                               Just (tc,_) -> Just (getName tc)
+                               Nothing     -> Nothing
+roughTopName (Coercion _) = Nothing 
 roughTopName (App f _) = roughTopName f
 roughTopName (Var f)   | isGlobalId f	-- Note [Care with roughTopName]
                        , isDataConWorkId f || idArity f > 0
@@ -625,10 +625,7 @@ match :: RuleEnv
 -- succeed in matching what looks like the template variable 'a' against 3.
 
 -- The Var case follows closely what happens in Unify.match
-match renv subst (Var v1) e2
-  | Just subst <- match_var renv subst v1 e2
-  = Just subst
-
+match renv subst (Var v1)    e2 = match_var renv subst v1 e2
 match renv subst (Note _ e1) e2 = match renv subst e1 e2
 match renv subst e1 (Note _ e2) = match renv subst e1 e2
       -- Ignore notes in both template and thing to be matched
@@ -714,15 +711,29 @@ match renv subst (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2)
 
 match renv subst (Type ty1) (Type ty2)
   = match_ty renv subst ty1 ty2
+match renv subst (Coercion co1) (Coercion co2)
+  = match_co renv subst co1 co2
 
 match renv subst (Cast e1 co1) (Cast e2 co2)
-  = do	{ subst1 <- match_ty renv subst co1 co2
+  = do	{ subst1 <- match_co renv subst co1 co2
 	; match renv subst1 e1 e2 }
 
 -- Everything else fails
 match _ _ _e1 _e2 = -- pprTrace "Failing at" ((text "e1:" <+> ppr _e1) $$ (text "e2:" <+> ppr _e2)) $
                     Nothing
 
+-------------
+match_co :: RuleEnv
+      	 -> RuleSubst
+      	 -> Coercion
+      	 -> Coercion
+      	 -> Maybe RuleSubst
+match_co renv subst (CoVarCo cv) co
+  = match_var renv subst cv (Coercion co)
+match_co _ _ co1 _ 
+  = pprTrace "match_co baling out" (ppr co1) Nothing
+
+-------------
 rnMatchBndr2 :: RuleEnv -> RuleSubst -> Var -> Var -> RuleEnv
 rnMatchBndr2 renv subst x1 x2
   = renv { rv_lcl  = rnBndr2 rn_env x1 x2
@@ -1038,6 +1049,7 @@ ruleCheck :: RuleCheckEnv -> CoreExpr -> Bag SDoc
 ruleCheck _   (Var _) 	    = emptyBag
 ruleCheck _   (Lit _) 	    = emptyBag
 ruleCheck _   (Type _)      = emptyBag
+ruleCheck _   (Coercion _)  = emptyBag
 ruleCheck env (App f a)     = ruleCheckApp env (App f a) []
 ruleCheck env (Note _ e)    = ruleCheck env e
 ruleCheck env (Cast e _)    = ruleCheck env e
diff --git a/compiler/specialise/SpecConstr.lhs b/compiler/specialise/SpecConstr.lhs
index 4fa42046e8..5fc0226941 100644
--- a/compiler/specialise/SpecConstr.lhs
+++ b/compiler/specialise/SpecConstr.lhs
@@ -33,9 +33,9 @@ import CoreMonad
 import HscTypes         ( ModGuts(..) )
 import WwLib		( mkWorkerArgs )
 import DataCon
-import Coercion	
+import Coercion		hiding( substTy, substCo )
 import Rules
-import Type		hiding( substTy )
+import Type		hiding ( substTy )
 import Id
 import MkCore		( mkImpossibleExpr )
 import Var
@@ -50,6 +50,7 @@ import Demand
 import DmdAnal		( both )
 import Serialized       ( deserializeWithData )
 import Util
+import Pair
 import UniqSupply
 import Outputable
 import FastString
@@ -699,6 +700,9 @@ scSubstId env v = lookupIdSubst (text "scSubstId") (sc_subst env) v
 scSubstTy :: ScEnv -> Type -> Type
 scSubstTy env ty = substTy (sc_subst env) ty
 
+scSubstCo :: ScEnv -> Coercion -> Coercion
+scSubstCo env co = substCo (sc_subst env) co
+
 zapScSubst :: ScEnv -> ScEnv
 zapScSubst env = env { sc_subst = zapSubstEnv (sc_subst env) }
 
@@ -777,7 +781,7 @@ extendCaseBndrs env scrut case_bndr con alt_bndrs
 		       	vanilla_args = map Type (tyConAppArgs (idType case_bndr)) ++
 				       varsToCoreExprs alt_bndrs
 
-   zap v | isTyCoVar v = v		-- See NB2 above
+   zap v | isTyVar v = v		-- See NB2 above
          | otherwise = zapIdOccInfo v
 
 
@@ -997,11 +1001,12 @@ scExpr' env (Var v)     = case scSubstId env v of
 		            e'     -> scExpr (zapScSubst env) e'
 
 scExpr' env (Type t)    = return (nullUsage, Type (scSubstTy env t))
+scExpr' env (Coercion c) = return (nullUsage, Coercion (scSubstCo env c))
 scExpr' _   e@(Lit {})  = return (nullUsage, e)
 scExpr' env (Note n e)  = do (usg,e') <- scExpr env e
                              return (usg, Note n e')
 scExpr' env (Cast e co) = do (usg, e') <- scExpr env e
-                             return (usg, Cast e' (scSubstTy env co))
+                             return (usg, Cast e' (scSubstCo env co))
 scExpr' env e@(App _ _) = scApp env (collectArgs e)
 scExpr' env (Lam b e)   = do let (env', b') = extendBndr env b
                              (usg, e') <- scExpr env' e
@@ -1047,7 +1052,7 @@ scExpr' env (Case scrut b ty alts)
 	   ; return (usg', b_occ `combineOcc` scrut_occ, (con, bs2, rhs')) }
 
 scExpr' env (Let (NonRec bndr rhs) body)
-  | isTyCoVar bndr	-- Type-lets may be created by doBeta
+  | isTyVar bndr	-- Type-lets may be created by doBeta
   = scExpr' (extendScSubst env bndr rhs) body
 
   | otherwise	
@@ -1417,6 +1422,7 @@ calcSpecStrictness fn qvars pats
     dmd_env = go emptyVarEnv dmds pats
 
     go env ds (Type {} : pats) = go env ds pats
+    go env ds (Coercion {} : pats) = go env ds pats
     go env (d:ds) (pat : pats) = go (go_one env d pat) ds pats
     go env _      _            = env
 
@@ -1517,7 +1523,7 @@ callToPats env bndr_occs (con_env, args)
 		-- at the call site
 		-- See Note [Shadowing] at the top
 		
-	      (tvs, ids) = partition isTyCoVar qvars
+	      (tvs, ids) = partition isTyVar qvars
 	      qvars'     = tvs ++ ids
 		-- Put the type variables first; the type of a term
 		-- variable may mention a type variable
@@ -1552,6 +1558,9 @@ argToPat :: ScEnv
 
 argToPat _env _in_scope _val_env arg@(Type {}) _arg_occ
   = return (False, arg)
+    
+argToPat _env _in_scope _val_env arg@(Coercion {}) _arg_occ
+  = return (False, arg)
 
 argToPat env in_scope val_env (Note _ arg) arg_occ
   = argToPat env in_scope val_env arg arg_occ
@@ -1577,8 +1586,8 @@ argToPat env in_scope val_env (Case scrut _ _ [(_, _, rhs)]) arg_occ
 -}
 
 argToPat env in_scope val_env (Cast arg co) arg_occ
-  | isIdentityCoercion co     -- Substitution in the SpecConstr itself
-                              -- can lead to identity coercions
+  | isReflCo co     -- Substitution in the SpecConstr itself
+                    -- can lead to identity coercions
   = argToPat env in_scope val_env arg arg_occ
   | not (ignoreType env ty2)
   = do	{ (interesting, arg') <- argToPat env in_scope val_env arg arg_occ
@@ -1588,10 +1597,10 @@ argToPat env in_scope val_env (Cast arg co) arg_occ
 	{ -- Make a wild-card pattern for the coercion
 	  uniq <- getUniqueUs
 	; let co_name = mkSysTvName uniq (fsLit "sg")
-	      co_var = mkCoVar co_name (mkCoKind ty1 ty2)
-	; return (interesting, Cast arg' (mkTyVarTy co_var)) } }
+	      co_var = mkCoVar co_name (mkCoType ty1 ty2)
+	; return (interesting, Cast arg' (mkCoVarCo co_var)) } }
   where
-    (ty1, ty2) = coercionKind co
+    Pair ty1 ty2 = coercionKind co
 
     
 
@@ -1699,7 +1708,7 @@ isValue env (Var v)
 	-- as well, for let-bound constructors!
 
 isValue env (Lam b e)
-  | isTyCoVar b = case isValue env e of
+  | isTyVar b = case isValue env e of
 		  Just _  -> Just LambdaVal
 		  Nothing -> Nothing
   | otherwise = Just LambdaVal
@@ -1734,6 +1743,7 @@ samePat (vs1, as1) (vs2, as2)
     same (App f1 a1) (App f2 a2) = same f1 f2 && same a1 a2
 
     same (Type {}) (Type {}) = True	-- Note [Ignore type differences]
+    same (Coercion {}) (Coercion {}) = True
     same (Note _ e1) e2	= same e1 e2	-- Ignore casts and notes
     same (Cast e1 _) e2	= same e1 e2
     same e1 (Note _ e2) = same e1 e2
diff --git a/compiler/specialise/Specialise.lhs b/compiler/specialise/Specialise.lhs
index 415378ac47..c192b3f60a 100644
--- a/compiler/specialise/Specialise.lhs
+++ b/compiler/specialise/Specialise.lhs
@@ -709,11 +709,12 @@ specExpr :: Subst -> CoreExpr -> SpecM (CoreExpr, UsageDetails)
 
 ---------------- First the easy cases --------------------
 specExpr subst (Type ty) = return (Type (CoreSubst.substTy subst ty), emptyUDs)
+specExpr subst (Coercion co) = return (Coercion (CoreSubst.substCo subst co), emptyUDs)
 specExpr subst (Var v)   = return (specVar subst v,         emptyUDs)
 specExpr _     (Lit lit) = return (Lit lit,                 emptyUDs)
 specExpr subst (Cast e co) = do
     (e', uds) <- specExpr subst e
-    return ((Cast e' (CoreSubst.substTy subst co)), uds)
+    return ((Cast e' (CoreSubst.substCo subst co)), uds)
 specExpr subst (Note note body) = do
     (body', uds) <- specExpr subst body
     return (Note (specNote subst note) body', uds)
@@ -1518,7 +1519,7 @@ instance Ord CallKey where
 		  cmp Nothing   Nothing   = EQ
 		  cmp Nothing   (Just _)  = LT
 		  cmp (Just _)  Nothing   = GT
-		  cmp (Just t1) (Just t2) = tcCmpType t1 t2
+		  cmp (Just t1) (Just t2) = cmpType t1 t2
 
 unionCalls :: CallDetails -> CallDetails -> CallDetails
 unionCalls c1 c2 = plusVarEnv_C unionCallInfoSet c1 c2
@@ -1603,7 +1604,9 @@ interestingDict :: CoreExpr -> Bool
 interestingDict (Var v) =  hasSomeUnfolding (idUnfolding v)
 			|| isDataConWorkId v
 interestingDict (Type _)	  = False
+interestingDict (Coercion _)      = False
 interestingDict (App fn (Type _)) = interestingDict fn
+interestingDict (App fn (Coercion _)) = interestingDict fn
 interestingDict (Note _ a)	  = interestingDict a
 interestingDict (Cast e _)	  = interestingDict e
 interestingDict _                 = True