The following code compiles on GHC 8.0.2 through GHC 8.6.3 with -dcore-lint:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

data family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b

data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
type instance Apply (TyCon1 f) x = f x

data SomeApply :: (k ~> Type) -> Type where
  SomeApply :: Apply f a -> SomeApply f

f :: SomeApply (TyCon1 Sing :: k ~> Type)
  -> SomeApply (TyCon1 Sing :: k ~> Type)
f (SomeApply s)
 = SomeApply s

However, it chokes on GHC HEAD:

$ ~/Software/ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint
GHCi, version 8.7.20190120: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the expression: SomeApply
                         @ k_a1Dz
                         @ (TyCon1 Sing)
                         @ Any
                         (s_a1Bq
                          `cast` (Sub (D:R:ApplyabTyCon1x[0]
                                           <k_a1Dz>_N
                                           <*>_N
                                           <Sing>_N
                                           <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]
                                                                 <k_a1Dz>_N <*>_N <Sing>_N <Any>_N))
                                  :: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any))
    Trans coercion mis-match: D:R:ApplyabTyCon1x[0]
                                  <k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]
                                                                                  <k_a1Dz>_N
                                                                                  <*>_N
                                                                                  <Sing>_N
                                                                                  <Any>_N)
      Apply (TyCon1 Sing) a_a1DB
      Sing a_a1DB
      Sing Any
      Apply (TyCon1 Sing) Any
*** Offending Program ***

<elided>

f :: forall k. SomeApply (TyCon1 Sing) -> SomeApply (TyCon1 Sing)
[LclIdX]
f = \ (@ k_a1Dz) (ds_d1EV :: SomeApply (TyCon1 Sing)) ->
      case ds_d1EV of wild_00 { SomeApply @ a_a1DB s_a1Bq ->
      break<0>(s_a1Bq)
      SomeApply
        @ k_a1Dz
        @ (TyCon1 Sing)
        @ Any
        (s_a1Bq
         `cast` (Sub (D:R:ApplyabTyCon1x[0]
                          <k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]
                                                                          <k_a1Dz>_N
                                                                          <*>_N
                                                                          <Sing>_N
                                                                          <Any>_N))
                 :: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any))
      }

Note that if I change the definition of Sing to this:

data family Sing (a :: k)

Then the error goes away.

Also, if I extend SomeProxy with an additional proxy field:

data SomeApply :: (k ~> Type) -> Type where
  SomeApply :: proxy a -> Apply f a -> SomeApply f

f :: SomeApply (TyCon1 Sing :: k ~> Type)
  -> SomeApply (TyCon1 Sing :: k ~> Type)
f (SomeApply p s)
 = SomeApply p s

Then the error also goes away. Perhaps a being ambiguous plays an important role here?

Possibly related to #16188 (closed) or #16204 (closed).