GHC can't infer pattern signature, untoucable kinds

{-# Language TypeFamilyDependencies, TypeInType, KindSignatures, PolyKinds, PatternSynonyms, GADTs #-}

import Data.Kind

data T = D | I

type SING k = k -> Type

type family
  Sing = (r :: SING k) | r -> k where
  Sing = ST
  Sing = SPair

data ST :: SING T where
  SD :: ST D
  SI :: ST I

data SPair :: SING (k, k') where
  SPair :: Sing a -> Sing b -> SPair '(a, b)

pattern DD :: SPair '(D, D)
pattern DD = SPair SD SD

works.. until we remove the pattern signature for DD, then we get

$ ghci-8.0.1 -ignore-dot-ghci /tmp/aur.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/aur.hs, interpreted )

/tmp/aur.hs:21:20: error:
    • Couldn't match kind ‘k’ with ‘T’
        ‘k’ is untouchable
          inside the constraints: t ~ '(a, b)
          bound by a pattern with constructor:
                     SPair :: forall k k' (a :: k) (b :: k').
                              Sing a -> Sing b -> SPair '(a, b),
                   in a pattern synonym declaration
          at /tmp/aur.hs:21:14-24
      ‘k’ is a rigid type variable bound by
        the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
      Possible fix: add a type signature for ‘DD’
      When matching the kind of ‘a’
      Expected type: Sing a
        Actual type: ST a
    • In the pattern: SD
      In the pattern: SPair SD SD
      In the declaration for pattern synonym ‘DD’

/tmp/aur.hs:21:23: error:
    • Couldn't match kind ‘k'’ with ‘T’
        ‘k'’ is untouchable
          inside the constraints: a ~ 'D
          bound by a pattern with constructor: SD :: ST 'D,
                   in a pattern synonym declaration
          at /tmp/aur.hs:21:20-21
      ‘k'’ is a rigid type variable bound by
        the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
      Possible fix: add a type signature for ‘DD’
      When matching the kind of ‘b’
      Expected type: Sing b
        Actual type: ST b
    • In the pattern: SD
      In the pattern: SPair SD SD
      In the declaration for pattern synonym ‘DD’
Failed, modules loaded: none.

Restricting the kind of SPair to SPair :: SING (T, T) gets it to work, can it be made to work bidirectionally? Or can it only work unidirectionally

pattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res
pattern DD <- SPair SD SD

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture