TypeApplications how?

typeappvsproxy.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

data Nat = O | S Nat
type family xs ++ ys where
  '[]      ++ ys = ys
  (x : xs) ++ ys = x : (xs ++ ys)

type family Drop n xs where
  Drop  O         xs  = xs
  Drop (S n) (_ : xs) = Drop n xs

type family Length xs where
  Length '[] = O
  Length  (x : xs) = S (Length xs)

class DropProp a where
    withDropProp :: (Drop (Length a) (a ++ c) ~ c => r) -> r

instance DropProp '[] where withDropProp r = r
--instance DropProp as => DropProp (a:as) where withDropProp = withDropProp @as @c
--test.hs:26:80: error: Not in scope: type variable ‘c’
--   |
--26 | instance DropProp as => DropProp (a:as) where withDropProp = withDropProp @as @c
--   |                                                                                ^

--instance DropProp as => DropProp (a:as) where withDropProp = withDropProp @as
--test.hs:26:62: error:
--    • Could not deduce: Drop (Length as) (as ++ c) ~ c
--      from the context: Drop (Length as) (as ++ c0) ~ c0
--        bound by a type expected by the context:
--                   (Drop (Length as) (as ++ c0) ~ c0) => r
--        at test.hs:26:62-77
--      ‘c’ is a rigid type variable bound by
--        the type signature for:
--          withDropProp :: forall (c :: [*]) r.
--                          ((Drop (Length (a : as)) ((a : as) ++ c) ~ c) => r) -> r
--        at test.hs:26:47-58
--    • In the expression: withDropProp @as
--      In an equation for ‘withDropProp’: withDropProp = withDropProp @as
--      In the instance declaration for ‘DropProp (a : as)’
--    • Relevant bindings include
--        withDropProp :: ((Drop (Length (a : as)) ((a : as) ++ c) ~ c) => r)
--                        -> r
--          (bound at test.hs:26:47)
--   |
--26 | instance DropProp as => DropProp (a:as) where withDropProp = withDropProp @as
--   |                                                              ^^^^^^^^^^^^^^^^