良く型付けされたtake関数

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses , ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts , TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

data Zero = Zero
data Succ a where
    Succ :: (Nat a,NimusLemma a) => a -> Succ a

class Nat a where
    split :: (Nat a,Nat b,NimusLemma b) => a -> List e b -> (List e a,List e (Nimus b a))
instance Nat Zero where
    split Zero (b :: List e b) = (Nil,b')
        where
          b' :: List e (Nimus b Zero)
          b' = convList b (Symm lemma)
instance (Nat a) => Nat (Succ a) where
    split (Succ a :: Succ a) (Cons b c :: List e b) = goal
        where
          (f :: List e a,s :: List e (Nimus (Pred b) a)) = split a c
          f' :: List e (Succ a)
          f' = Cons b f

          p :: Id a (Nimus a Zero)
          p = Symm $ lemma

          p' :: Id (Nimus (Pred b) a) (Nimus b (Succ a))
          p' = proof (length' (Cons b c) :: b) (a :: a)

          p'' ::List e (Nimus b (Succ a))
          p'' = convList s p'

          goal :: (List e (Succ a),List e (Nimus b (Succ a)))
          goal = (f',p'')

type family Nimus a b
type instance Nimus Zero b = Zero
type instance Nimus (Succ a) Zero = (Succ a)
type instance Nimus (Succ a) (Succ b) = Nimus a b

type family Pred a
type instance Pred Zero = Zero
type instance Pred (Succ a) = a

data Id :: * -> * -> * where
           Refl :: Id a a
           Symm :: (Id a b) -> (Id b a)
           Trans :: (Id a b) -> (Id b c) -> Id a c
           MapId :: Id a b -> Id (f a) (f b)

convList :: List e a -> Id a b -> List e b
convList (list :: List e a) (eq :: Id a b) = goal
    where
      p :: Id (List e a) (List e b)
      p = MapId eq

      goal :: List e b
      goal = conv list p

conv :: a -> Id a b -> b
conv a Refl = a

class (Nat a) => NimusLemma a where
    lemma :: Id (Nimus a Zero) a
instance NimusLemma Zero where
    lemma = Refl
instance (Nat a) => NimusLemma (Succ a) where
    lemma = Refl

class (Nat a,Nat b) => NimusProof a b where
    proof :: a -> b -> Id (Nimus (Pred a) b) (Nimus a (Succ b))
instance (Nat a) => NimusProof Zero a where
    proof _ _ = Refl
instance (Nat a,Nat b) => NimusProof (Succ a) b where
    proof _ _ = Refl

data List a n where
    Nil :: List a Zero
    Cons :: (Nat n,NimusLemma n) => a -> List a n -> List a (Succ n)

instance (Show a) => Show (List a n) where
    show Nil = "[]"
    show (Cons x xs) = show x ++ "," ++ show xs

length' :: List a n -> n
length' Nil = Zero
length' (Cons x xs) = Succ (length' xs)

-- 単にこれが書きたかった！！
take' :: (Nat n,Nat l,NimusLemma n) => l -> List a n -> List a l
take' l list = fst $ split l list

-- 一応使ってみる
intlist :: List Int (Succ (Succ (Succ (Succ Zero))))
intlist = Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))

taked :: List Int (Succ (Succ (Succ Zero)))
taked = take' (Succ (Succ (Succ Zero))) intlist

超力業。で、力業に見えなくも無い程度にはすんなり収まった気配を見せているがクラスコンテキストがぐちゃぐちゃになってるのと、Natにsplitって一体全体みたいな感じに成っていて、まぁsplitがまずかった！！

Nimusくんまじやばいで・・・。

あと途中こんなコード断片が出て来て

convList :: (Nat a,Nat b,NimusProof a b) => List e (Nimus (Pred a) b) -> List e (Nimus a (Succ b))
convList (list :: List e (Nimus (Pred a) b)) = undefined

エラーメッセージが

    Pattern signature must exactly match: List e (Nimus (Pred a) b)
    In the pattern: list :: List e (Nimus (Pred a) b)
    In the definition of `convList':
        convList (list :: List e (Nimus (Pred a) b)) = undefined

良く分からんなーみたいな。

証明はforallに対して書けるのですが、type familyが型変数を持って手放してくれない場合はそれは型変数ではなくてrigitな型で実型が隠れているみたいな感じなので、どうしてもScopedTypeVariableを使って引っ張りださないといけない => でも書けない => なのでproofには第一引数と第二引数を与えてそれにあう証明にしちゃう、という感じにしています。

丸一日かかった。頭悪過ぎる。

例によって使わないオプションも存在。