Constraint vs. Type causes instance incoherence

This issue manifests (at least) with GHC 8.6.5, 8.8.4, 8.10.7, 9.0.1. (The latter two currently are stable releases.)

Confusion between Constraint and Type permits the creation of local instances. Compare with #20356 (closed).

{-# LANGUAGE
TypeApplications, PolyKinds, KindSignatures,
ScopedTypeVariables, TypeFamilies, RankNTypes,
ExistentialQuantification, ImpredicativeTypes,
ConstraintKinds, UndecidableInstances,
DataKinds, AllowAmbiguousTypes #-}

module DDict9 where

import Data.Kind
import Data.Coerce
import Data.Typeable
import Data.Type.Equality

type family X (x :: k) :: l where { X x = x }
type family Y (x :: k) :: l where { Y (x -> y) = x -> y }

newtype DDict (c :: Constraint) = DDict (X c)

idY1 :: forall c. Y (c => X c)
idY1 = id @(X c)

idY2 :: forall c r. Y (c => r) -> (c => r)
idY2 = coerce @(Y (c => r)) @(c => r)

idY3 :: forall c. c => X c
idY3 = idY2 @c @(X c) (idY1 @c)

ddict :: forall c. c => DDict c
ddict = DDict (idY3 @c)

idY4 :: forall c r. (c => r) -> Y (c => r)
idY4 = coerce @(c => r) @(Y (c => r))

idY5 :: forall c r. Y (c => r) -> (X c -> r)
idY5 = id @(Y (c => r))

withDDict :: forall c r. DDict c -> (c => r) -> r
withDDict (DDict x) cont = idY5 @c @r (idY4 @c @r cont) x

outDDict :: forall a. DDict (X a) -> a
outDDict = coerce @(DDict (X a)) @a

inDDict :: forall a. a -> DDict (X a)
inDDict = coerce @a @(DDict (X a))

data family E :: k
newtype instance E a = E (a -> a -> Bool)

newtype N (k :: Type) a = N a

-- GHC panics after simplifying the type @X (E a :: Type)@ and using it.
-- So put the variable @k@ so that we can store the evidence before
-- simplifying the type.
instance (Typeable k, X (E a :: k)) => Eq (N k a) where
  (N x) == (N y) =
    let
      dEq :: DDict (X (E a :: k))
      dEq = ddict @(X (E a :: k))
    in case eqT @k @Type of
      Nothing -> error "not Type"
      Just Refl ->
        let
          eEq :: E a
          eEq = outDDict @(E a :: Type) dEq
          eq :: a -> a -> Bool
          E eq = eEq
        in eq x y
  a /= b = not (a == b)

ddictImpl :: forall k a. Typeable k =>
  DDict (X (E a :: k)) -> DDict (Eq (N k a))
ddictImpl e = withDDict e ddict

incohA :: forall a. (a -> a -> Bool) -> DDict (Eq (N Type a))
incohA eq =
  let
    d :: DDict (X (E a :: Type))
    d = inDDict @(E a :: Type) (E eq)
  in ddictImpl @Type @a d

main :: IO ()
main = do
  let
    n :: N Type ()
    n = N ()
  print $ withDDict (incohA (\ () () -> True)) (n == n)
  print $ withDDict (incohA (\ () () -> False)) (n == n)

Results:

• Core lint fails with GHC 8.6 (“In the coercion … kind application error”), but succeeds with the other versions.
• A bogus warning (“Couldn't match kind ‘Constraint’ with ‘Type’. Inaccessible code …”) is emitted.
• Prints True\nFalse\n.

(Amusingly, DDict is like Dict, but without an indirection, and we can UNPACK dictionaries as Kmett wants in #19630. So this bug is partially useful.)

All these versions of GHC reduce Y (a => b) to a -> b, which is identified with a => b except in GHC 9.0. Even in GHC 9.0, there is a coercion-thing between a => b and a -> b.

I have not tested with GHC HEAD. The comment 18762#note_317540 suggests that it may not work. However maybe the tricks of coerce can still cause problems.