Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information