Panic with dependent composition

[goldfirere]

{-# LANGUAGE DeriveDataTypeable, TypeFamilies, TemplateHaskell, DataKinds,
             PolyKinds, GADTs, RankNTypes, MultiParamTypeClasses,
             FlexibleInstances, UndecidableInstances, UnicodeSyntax,
             FunctionalDependencies, StandaloneDeriving,
             TypeOperators, ScopedTypeVariables, NoMonomorphismRestriction,
             MonadComprehensions, DeriveGeneric, FlexibleContexts,
             GeneralizedNewtypeDeriving, ConstraintKinds,
             LambdaCase, ViewPatterns, AllowAmbiguousTypes,
             DefaultSignatures, RecursiveDo, -- ImpredicativeTypes,
             ImplicitParams, MagicHash, UnboxedTuples, RoleAnnotations,
             ExtendedDefaultRules, PatternSynonyms, EmptyCase,
             BangPatterns, InstanceSigs, DeriveFunctor, Arrows
             , NamedWildCards, PartialTypeSignatures
             , TypeInType, TypeApplications, TypeFamilyDependencies
--             , NoImplicitPrelude
--             , OverloadedLists
  #-}

module Scratch where

import Data.Kind
import Data.Singletons
import Data.Singletons.TH

data instance Sing (x :: Proxy k) where
  SProxy :: Sing 'Proxy

dcomp :: forall (a :: Type)
                (b :: a ~> Type)
                (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
                (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
                (g :: forall (x :: a). Proxy x ~> b @@ x)
                (x :: a).
         Sing f
      -> Sing g
      -> Sing x
      -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
dcomp f g x = undefined