Tidy up Coercion.mkRuntimeRepCowip/spj-early-inline4

Summary:
It was hard to understand, and inefficient in the common case.
Better now.

Reviewers: austin, goldfire, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3208

2 files changed, 28 insertions, 20 deletions

diff --git a/compiler/prelude/TysWiredIn.hs-boot b/compiler/prelude/TysWiredIn.hs-boot
index 26e42010c9..c740690603 100644
--- a/compiler/prelude/TysWiredIn.hs-boot
+++ b/compiler/prelude/TysWiredIn.hs-boot
@@ -17,6 +17,7 @@ constraintKind :: Kind
 
 runtimeRepTyCon, vecCountTyCon, vecElemTyCon :: TyCon
 runtimeRepTy :: Type
+liftedRepTy  :: Type
 
 liftedRepDataConTyCon, vecRepDataConTyCon, tupleRepDataConTyCon :: TyCon
 
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 353134d4a9..f53968edc1 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -123,7 +123,7 @@ import Pair
 import SrcLoc
 import PrelNames
 import TysPrim          ( eqPhantPrimTyCon )
-import {-# SOURCE #-} TysWiredIn ( constraintKind )
+import {-# SOURCE #-} TysWiredIn ( liftedRepTy, constraintKind )
 import ListSetOps
 import Maybes
 import UniqFM
@@ -427,42 +427,49 @@ mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
 mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
 
 constraintIsLifted :: CoAxiomRule
-constraintIsLifted =
-    CoAxiomRule { coaxrName = mkFastString "constraintIsLifted"
+-- constratintIsLifted :: Type ~N Constraint
+constraintIsLifted
+  = CoAxiomRule { coaxrName      = mkFastString "constraintIsLifted"
                 , coaxrAsmpRoles = []
-                , coaxrRole = Nominal
-                , coaxrProves =
-                      const $ Just $ Pair constraintKind liftedTypeKind
+                , coaxrRole      = Nominal
+                , coaxrProves    = const $ Just $
+                                   Pair constraintKind liftedTypeKind
                 }
 
--- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
--- produce a coercion @rep_co :: r1 ~ r2@.
+-- | Given a coercion @co :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
+-- produce a coercion @rep_co :: r1 ~N r2@.
+--
+-- HACK for Constraint (which is currently a different kind than TYPE r):
+--    treat Constraint like TYPE LiftedRep, so
+--    if   co :: (a :: Constraint) ~ (b :: TYPE r2)
+--         return rep_co :: LiftedRep ~ r2
 mkRuntimeRepCo :: Coercion -> Coercion
 mkRuntimeRepCo co
     -- This is currently a bit tricky since we can see types of kind Constraint
     -- in addition to the usual things of kind (TYPE rep). We first map
     -- Constraint-kinded types to (TYPE 'LiftedRep).
     -- FIXME: this is terrible
-  | isConstraintKind a && isConstraintKind b
-  = mkNthCo 0 $ constraintToLifted
-  $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
+  | isReflCo kind_co   -- kind_co :: <TYPE r> or <Constraint>
+  = -- If a=b, things are easy
+    if isConstraintKind a
+    then mkNomReflCo liftedRepTy         -- <LiftedTypeRep>
+    else mkNomReflCo (tyConAppArgN 0 a)  -- <r>
 
-  | isConstraintKind a
+  | isConstraintKind a  -- Presumably b = TYPE r2
   = WARN( True, text "mkRuntimeRepCo" )
-    mkNthCo 0
-  $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
+    mkNthCo 0 (mkSymCo cl_co `mkTransCo` kind_co)
 
-  | isConstraintKind b
+  | isConstraintKind b  -- Presumably a = TYPE r1
   = WARN( True, text "mkRuntimeRepCo" )
-    mkNthCo 0 $ constraintToLifted kind_co
+    mkNthCo 0 (kind_co `mkTransCo` cl_co)
 
-  | otherwise
+  | otherwise           -- a = TYPE r1, t = TYPE r2
   = mkNthCo 0 kind_co
   where
-    -- the right side of a coercion from Constraint to TYPE 'LiftedRep
-    constraintToLifted = (`mkTransCo` mkAxiomRuleCo constraintIsLifted [])
+    -- cl_co :: Constraint ~ TYPE LiftedRep
+    cl_co = mkAxiomRuleCo constraintIsLifted []
 
-    kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
+    kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~N TYPE r2
                            -- (up to silliness with Constraint)
     Pair a b = coercionKind kind_co  -- Pair of (TYPE r1, TYPE r2)