Coercion: Try dropping constraintIsLifted axiom

While working through the FunCo patch I encountered some lint issues
which suggested that `Constraint` wasn't being considered equal to `TYPE
'LiftedRep`.  Consequently I introduced this axiom and associated messy
ball of logic to explicitly coerce `Constraint`.

However, as @goldfire points out on D3208 this really shouldn't be
necessary.  Indeed, I tried ripping out the axiom and things appear to
just work. I suspect the issue motivating the axiom was a bug elsewhere
in the FunCo branch that I fixed during development.

Test Plan: Validate

Reviewers: simonpj, goldfire, austin

Reviewed By: goldfire

Subscribers: thomie, goldfire

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

1 files changed, 0 insertions, 34 deletions

diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index f5791457ac..d195b2f5b0 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -108,7 +108,6 @@ module Coercion (
 
 import TyCoRep
 import Type
-import Kind
 import TyCon
 import CoAxiom
 import Var
@@ -116,14 +115,12 @@ import VarEnv
 import Name hiding ( varName )
 import Util
 import BasicTypes
-import FastString
 import Outputable
 import Unique
 import Pair
 import SrcLoc
 import PrelNames
 import TysPrim          ( eqPhantPrimTyCon )
-import {-# SOURCE #-} TysWiredIn ( constraintKind )
 import ListSetOps
 import Maybes
 import UniqFM
@@ -404,45 +401,14 @@ mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
 mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
 
-constraintIsLifted :: CoAxiomRule
-constraintIsLifted =
-    CoAxiomRule { coaxrName = mkFastString "constraintIsLifted"
-                , coaxrAsmpRoles = []
-                , 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@.
 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
-
-  | isConstraintKind a
-  = WARN( True, text "mkRuntimeRepCo" )
-    mkNthCo 0
-  $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
-
-  | isConstraintKind b
-  = WARN( True, text "mkRuntimeRepCo" )
-    mkNthCo 0 $ constraintToLifted kind_co
-
-  | otherwise
   = mkNthCo 0 kind_co
   where
-    -- the right side of a coercion from Constraint to TYPE 'LiftedRep
-    constraintToLifted = (`mkTransCo` mkAxiomRuleCo constraintIsLifted [])
-
     kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
                            -- (up to silliness with Constraint)
-    Pair a b = coercionKind kind_co  -- Pair of (TYPE r1, TYPE r2)
 
 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
 -- very quickly. Sometimes a coercion can be reflexive, but not obviously