我可以教 GHC 数学归纳法吗？

我试图创建一个表示无限多种类型的元组的数据类型：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeNats

infixr 5 :!!

data OmegaTuple (t :: Nat -> *) (n :: Nat) = t n :!! OmegaTuple t (n+1)

这可以。

我还试图声明无穷多半群的直积：

instance (Semigroup (t n), Semigroup (OmegaTuple t (n+1))) => Semigroup (OmegaTuple t n) where
    (x :!! xs) <> (y :!! ys) = x <> y :!! xs <> ys

然而 GHC 是这样抱怨的：

• Illegal nested constraint ‘Semigroup (OmegaTuple t (n + 1))’
  (Use UndecidableInstances to permit this)

如果我理解正确，使用UndecidableInstances会使 GHC 陷入无限循环。

另一种尝试：

instance (Semigroup (t n), forall k. Semigroup (t k) => Semigroup (t (k+1))) => Semigroup (OmegaTuple t n) where
    (x :!! xs) <> (y :!! ys) = x <> y :!! xs <> ys

然后 GHC 这样抱怨：

• Illegal type synonym family application ‘k + 1’ in instance:
    Semigroup (t (k + 1))

教GHC数学归纳法真的不行吗？

回答

{-# LANGUAGE GADTs     #-}
{-# LANGUAGE DataKinds #-}
import Data.Kind (Type)
import GHC.TypeLits
data SemigroupSequence (t :: Nat -> Type) (n :: Nat) where
SemigroupSequence :: Semigroup (t n)
=> SemigroupSequence t (n+1) -> SemigroupSequence t n
class SemigroupFamily t where
semigroupSequence :: SemigroupSequence t 0

mappendOmega :: SemigroupSequence t n
-> OmegaTuple t n -> OmegaTuple t n -> OmegaTuple t n
mappendOmega (SemigroupSequence sd') (x :!! xs) (y :!! ys)
= x <> y :!! mappendOmega sd' xs ys
instance (SemigroupFamily t) => Semigroup (OmegaTuple t 0) where
(<>) = mappendOmega semigroupSequence