GitLab

Same code as #19092 (closed) but where TryUnify is given the kind Bool -> PolyKinded (PolyKinded Constraint) rather than TryUnify :: Bool -> forall k. k -> forall j. j -> Constraint.

{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}

{-# Options_GHC -dcore-lint #-}

import Data.Type.Equality
import Data.Kind

type PolyKinded :: Type -> Type
type PolyKinded res = (forall (k :: Type). k -> res)

infix 4
 ===
type
 (===) :: PolyKinded (PolyKinded Bool)
type family
 a === b where
 a === a = True
 _ === _ = False

type  TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)
class (a === b) ~ cond
   => TryUnify cond a b
instance (a === b) ~ False
      => TryUnify False @k a @j b
instance {-# Incoherent #-}
         ( (a === b) ~ True
         , a ~~ b
         )
      => TryUnify True @k a @j b

Somewhat surprisingly to me, using PolyKinded affects

$ ghc --interactive -ignore-dot-ghci file.hs
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( file.hs, interpreted )

/home/baldur/hs/file.hs:24:10: error:
    * Could not deduce: (a === b) ~ 'False
        arising from the superclasses of an instance declaration
      from the context: (a === b) ~ 'False
        bound by the instance declaration
        at ..file.hs:(24,10)-(25,33)
    * In the instance declaration for `TryUnify 'False a b'
   |
24 | instance (a === b) ~ False
   |          ^^^^^^^^^^^^^^^^^^...
Failed, no modules loaded.

So what is different, the program compiles with any of these variants:

type  TryUnify :: Bool -> forall k. k -> PolyKinded Constraint

type  TryUnify :: Bool -> forall k. k -> forall j. j -> Constraint

type  TryUnify :: Bool -> PolyKinded (forall j. j -> Constraint) -- -XLiberalTypeSynonyms