TypeInType, index GADT by constraint witness

Just wondering if it would ever make sense to allow or use constraints like this

{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}

import Data.Kind

data Struct :: (k -> Constraint) -> (k -> Type) where
  S :: cls a => Struct cls a

data Foo a where
  F :: Foo (S::Struct Eq a)

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

/tmp/test.hs:9:13: error:
    • Illegal constraint in a type: cls0 a0
    • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
      In the type ‘Foo (S :: Struct Eq a)’
      In the definition of data constructor ‘F’
  |
9 |   F :: Foo (S::Struct Eq a)
  |             ^
Failed, no modules loaded.
Prelude> 

Please close the ticket if it doesn't

Trac metadata

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