haskell - 昇格された型の型クラスでの網羅性チェック

Question

type を昇格Nat = Suc Nat | Zeroさせたので、 typeclass を作成したいと思いclass C (a :: Nat) bます。GHCにそれを納得させ、すべてのケースinstance C Zero bをカバーする方法はありますか?したがって、クラスのメソッドを使用するたびに、制約としてinstance C (Seq x) b明示的に宣言する必要はありません。Cここにいくつかのコードがあります：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
-- Some of these may not be necessary for the particular snippet.

data Nat = Zero | Suc Nat
-- TypeApplications, I know. I am traditional.
data NProxy :: Nat -> * where
  NProxy :: NProxy n

class C (a :: Nat) b where
  f :: NProxy a -> b -> Maybe b

instance C Zero b where
  f _ _ = Nothing
instance C (Suc a) b where
  f _ = Just
-- instance C n b where
--   f = error "This should not have been reached using GetNum."


class C1 a where
  f1 :: a -> Maybe a

instance C1 a where
  f1 = Just

type family GetNum a :: Nat where
  GetNum Char = (Suc Zero)
  GetNum Int = Suc (Suc Zero)
  GetNum [x] = Suc (GetNum x)
  GetNum a = Suc Zero

-- Error:
-- • No instance for (C (GetNum a) a) arising from a use of ‘f’
-- • In the expression: f (NProxy :: NProxy (GetNum a)) x
--   In an equation for ‘noGreet’:
--       noGreet x = f (NProxy :: NProxy (GetNum a)) x
noGreet :: forall a . a -> Maybe a
noGreet x = f (NProxy :: NProxy (GetNum a)) x

-- This one works fine though.
dumb :: a -> Maybe a
dumb = f1

編集:関連する質問は、コメントアウトされたインスタンス if を考えると、repl に例外が発生し、例外が発生しないとC言ったのはなぜですか。noGreet "hi"Just "hi"