Note [Type and Constraint are not apart]

Type and Constraint are not equal (eqType) but they are not /apart/
either. Reason (c.f. #7451):

* We want to allow newtype classes, where
    class C a where { op :: a -> a }

* The axiom for such a class will look like
    axiom axC a :: (C a :: Constraint) ~# (a->a :: Type)

* This axiom connects a type of kind Type with one of kind Constraint
  That is dangerous: kindCo (axC Int) :: Type ~N Constraint
  And /that/ is bad because we could have
     type family F a where
        F Type       = Int
        F Constraint = Bool
  So now we can prove Int ~N Bool, and all is lost.  We prevent this
  by saying that Type and Constraint are not Apart, which makes the
  above type family instances illegal.

So we ensure that Type and Constraint are not apart; or, more
precisely, that TYPE and CONSTRAINT are not apart.  This
non-apart-ness check is implemented in GHC.Core.Unify.unify_ty: look
for `maybeApart MARTypeVsConstraint`.

Note that, as before, nothing prevents writing instances like:

  instance C (Proxy @Type a) where ...

In particular, TYPE and CONSTRAINT (and the synonyms Type, Constraint
etc) are all allowed in instance heads. It's just that TYPE is not
apart from CONSTRAINT, which means that the above instance would
irretrievably overlap with:

  instance C (Proxy @Constraint a) where ...

Wrinkles

(W1) In GHC.Core.RoughMap.roughMatchTyConName we are careful to map
     TYPE and CONSTRAINT to the same rough-map key.  Reason:
     If we insert (F @Constraint tys) into a FamInstEnv, and look
     up (F @Type tys'), we /must/ ensure that the (C @Constraint tys)
     appears among the unifiables when we do the lookupRM' in
     GHC.Core.FamInstEnv.lookup_fam_inst_env'.  So for the RoughMap we
     simply pretend that they are the same type constructor.  If we
     don't, we'll treat them as fully apart, which is unsound.

(W2) We must extend this treatment to the different arrow types (see
     Note [Function type constructors and FunTy]): if we have
       FunCo (axC Int) <Int> :: (C Int => Int) ~ ((Int -> Int) -> Int),
     then we could extract an equality between (=>) and (->). We thus
     must ensure that (=>) and (->) (among the other arrow combinations)
     are not Apart. See the FunTy/FunTy case in GHC.Core.Unify.unify_ty.

(W3) Are (TYPE IntRep) and (CONSTRAINT WordRep) apart?  In truth yes,
     they are.  But it's easier to say that they are not apart, by
     reporting "maybeApart" (which is always safe), rather than
     recurse into the arguments (whose kinds may be utterly different)
     to look for apartness inside them.  Again this is in
     GHC.Core.Unify.unify_ty.

(W4) We give a different Typeable instance for Type than for Constraint.
     For type classes instances (unlike type family instances) it is not
     /unsound/ for Type and Constraint to treated as fully distinct; and
     for Typeable is desirable to give them different TypeReps.
     Certainly,
       - both Type and Constraint must /have/ a TypeRep, and
       - they had better not be the same (else eqTypeRep would give us
         a proof Type ~N Constraint, which we do not want
     So in GHC.Tc.Instance.Class.matchTypeable, Type and Constraint are
     treated as separate TyCons; i.e. given no special treatment.