typeappvsproxy2.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# 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 :: forall c r. (Drop (Length (a:as)) ((a:as) ++ c) ~ c => r) -> r
    withDropProp = withDropProp @as @c
    
test.hs:28:21: error:
    • Could not deduce: Drop (Length as) (as ++ c) ~ c
      from the context: Drop (Length (a : as)) ((a : as) ++ c0) ~ c0
        bound by the type signature for:
                   withDropProp :: (Drop (Length (a : as)) ((a : as) ++ c0) ~ c0) => r
        at test.hs:28:21-82
      ‘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:28:21-82
    • When checking that instance signature for ‘withDropProp’
        is more general than its signature in the class
        Instance sig: forall (c :: [*]) r.
                      ((Drop (Length (a : as)) ((a : as) ++ c) ~ c) => r) -> r
           Class sig: forall (c :: [*]) r.
                      ((Drop (Length (a : as)) ((a : as) ++ c) ~ c) => r) -> r
      In the instance declaration for ‘DropProp (a : as)’
   |
28 |     withDropProp :: forall c r. (Drop (Length (a:as)) ((a:as) ++ c) ~ c => r) -> r
   |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^