{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main where

import GHC.TypeLits
import Data.Proxy

class C (n :: Nat) where
  foo :: Proxy n -> ()

instance C 0 where
  foo _ = ()

instance C (n - 1) => C n where
  foo _ = ()

bar :: forall n. C n => ()
bar = foo (Proxy @n)

main :: IO ()
main = return ()