Break up TcRnTypes, among other modules.

This introduces three new modules:

 - basicTypes/Predicate.hs describes predicates, moving
   this logic out of Type. Predicates don't really exist
   in Core, and so don't belong in Type.

 - typecheck/TcOrigin.hs describes the origin of constraints
   and types. It was easy to remove from other modules and
   can often be imported instead of other, scarier modules.

 - typecheck/Constraint.hs describes constraints as used in
   the solver. It is taken from TcRnTypes.

No work other than module splitting is in this patch.

This is the first step toward homogeneous equality, which will
rely more strongly on predicates. And homogeneous equality is the
next step toward a dependently typed core language.

1 files changed, 52 insertions, 25 deletions

diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index d0000e1e35..7695e31643 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -37,11 +37,13 @@ module Coercion (
         mkPhantomCo,
         mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
         mkAxiomInstCo, mkProofIrrelCo,
-        downgradeRole, maybeSubCo, mkAxiomRuleCo,
+        downgradeRole, mkAxiomRuleCo,
         mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
         mkKindCo, castCoercionKind, castCoercionKindI,
 
         mkHeteroCoercionType,
+        mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
+        mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
 
         -- ** Decomposition
         instNewTyCon_maybe,
@@ -138,7 +140,7 @@ import Unique
 import Pair
 import SrcLoc
 import PrelNames
-import TysPrim          ( eqPhantPrimTyCon )
+import TysPrim
 import ListSetOps
 import Maybes
 import UniqFM
@@ -506,22 +508,6 @@ coVarRole cv
            Just tc0 -> tc0
            Nothing  -> pprPanic "coVarRole: not tyconapp" (ppr cv)
 
--- | Makes a coercion type from two types: the types whose equality
--- is proven by the relevant 'Coercion'
-mkCoercionType :: Role -> Type -> Type -> Type
-mkCoercionType Nominal          = mkPrimEqPred
-mkCoercionType Representational = mkReprPrimEqPred
-mkCoercionType Phantom          = \ty1 ty2 ->
-  let ki1 = typeKind ty1
-      ki2 = typeKind ty2
-  in
-  TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
-
-mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
-mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
-mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
-mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
-
 -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
 -- produce a coercion @rep_co :: r1 ~ r2@.
 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
@@ -1232,13 +1218,6 @@ downgradeRole r1 r2 co
       Just co' -> co'
       Nothing  -> pprPanic "downgradeRole" (ppr co)
 
--- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
--- Note that the input coercion should always be nominal.
-maybeSubCo :: EqRel -> Coercion -> Coercion
-maybeSubCo NomEq  = id
-maybeSubCo ReprEq = mkSubCo
-
-
 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 mkAxiomRuleCo = AxiomRuleCo
 
@@ -2357,6 +2336,54 @@ cf Type.piResultTys (which in fact we call here).
 
 -}
 
+-- | Makes a coercion type from two types: the types whose equality
+-- is proven by the relevant 'Coercion'
+mkCoercionType :: Role -> Type -> Type -> Type
+mkCoercionType Nominal          = mkPrimEqPred
+mkCoercionType Representational = mkReprPrimEqPred
+mkCoercionType Phantom          = \ty1 ty2 ->
+  let ki1 = typeKind ty1
+      ki2 = typeKind ty2
+  in
+  TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
+
+mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
+mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
+mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
+mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
+
+-- | Creates a primitive type equality predicate.
+-- Invariant: the types are not Coercions
+mkPrimEqPred :: Type -> Type -> Type
+mkPrimEqPred ty1 ty2
+  = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
+  where
+    k1 = typeKind ty1
+    k2 = typeKind ty2
+
+-- | Makes a lifted equality predicate at the given role
+mkPrimEqPredRole :: Role -> Type -> Type -> PredType
+mkPrimEqPredRole Nominal          = mkPrimEqPred
+mkPrimEqPredRole Representational = mkReprPrimEqPred
+mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"
+
+-- | Creates a primite type equality predicate with explicit kinds
+mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
+mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
+
+-- | Creates a primitive representational type equality predicate
+-- with explicit kinds
+mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
+mkHeteroReprPrimEqPred k1 k2 ty1 ty2
+  = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
+
+mkReprPrimEqPred :: Type -> Type -> Type
+mkReprPrimEqPred ty1  ty2
+  = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
+  where
+    k1 = typeKind ty1
+    k2 = typeKind ty2
+
 -- | Assuming that two types are the same, ignoring coercions, find
 -- a nominal coercion between the types. This is useful when optimizing
 -- transitivity over coercion applications, where splitting two