这是一个依赖类型haskell函数dfunc的例子，它的类型取决于参数值：0Map到Int的值，1Map到Integer的值，等等，如下面类型族中定义的。
所以我有一个函数，带有签名，但是我想去掉这个奇怪的int编码，然后用类型签名，实现一个函数，我知道，类型对于这个来说太通用了，但是我尝试用，没有类型签名的函数，来欺骗，让haskell来做类型推断，并得到错误，据我所知，因为ff实现在类型签名中无法表达。
我可以在这里使用一些“魔法”来删除GADTInt a -> Dt a并将其替换为Int -> ?吗

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Main where

data Nat :: * where
    Z :: Nat
    S :: Nat -> Nat

data GADTInt a where
    GADTZero :: GADTInt Z
    GADTOne :: GADTInt (S Z)
    GADTTwo :: GADTInt (S (S Z))   
    GADTThree :: GADTInt (S (S (S Z)))   

type family Dt a where
    Dt 'Z = Int
    Dt ('S 'Z) = Integer
    Dt ('S ('S 'Z)) = Float
    Dt ('S ('S ('S 'Z))) = String

class NTI a where
    toi :: a -> Int

instance NTI (GADTInt a) where
    toi GADTZero = 0 
    toi GADTOne = 1 
    toi GADTTwo = 2
    toi GADTThree = 3

dfunc :: GADTInt a -> Dt a
dfunc GADTZero = 1
dfunc GADTOne = 1000000000000000000000000000000
dfunc GADTTwo = 3.14
dfunc GADTThree = "Hi"

ff i 
     | toi GADTZero == i = dfunc GADTZero     
     | toi GADTOne == i = dfunc GADTOne
     | toi GADTTwo == i = dfunc GADTTwo     
     | toi GADTThree == i = dfunc GADTThree
     | otherwise = undefined