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
.