Make `Type` not apart from `Constraint`
Right now, GHC accepts this module:
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
type family F a
type instance F Type = Int
type instance F Constraint = Bool
The problem is that the Core this produces includes two axioms that are unsound together: the Core has axFType :: F Type ~ Int and axFConstraint :: F Constraint ~ Bool. The problem is that Type and Constraint are the same in Core, and so (sym axFConstraint ;; axFType) :: Bool ~ Int, and that's bad.
Accepted GHC proposal 32 says that the solution is simply to make Constraint not apart from Type. If we did this, GHC would consider those two equations to overlap, and they would be rejected.
This ticket is to track the implementation of the change to apartness.
I think the key change would be to make GHC.Core.Unify.unify_ty return MaybeApart when passed Type and Constraint.