Haskell simplify Dependent Type function signature

This is an example of dependent type haskell function dfunc. Its type depends on the argument value: zero maps to value of Int one maps to value of Integer and so on as defined in type family below.

So I have function dfunc with signature GADTInt a -> Dt a But I want to get rid of this wierd GADTInt a encoding of int and implement a function with type signature Int -> Dt a I understand that a type is to generic for this.., but I try to cheat with typeclass NTI and function ff without type signature, to let haskell do type inference for me, and get error, as i understand because ff implementation inexpressible in a type signature.

Can I do some "magic" here to get rid of GADTInt a -> Dt a and replace it with 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

Solution

The only way to use a Dt a is to know what a is. Because types are erased, you will need a run-time representation of it, for example using the GADTInt singleton. You can package those in an existential type:

data SomeDt where
  SomeDt :: GADTInt a -> Dt a -> SomeDt

It's also useful to wrap the singleton in another existential type:

data SomeGADTInt where
  SomeGADTInt :: GADTInt a -> SomeGADTInt

so that you can define the "non-dependent" tagging:

toTag :: Int -> SomeGADTInt
toTag 0 = SomeGADTInt GADTZero
toTag 1 = SomeGADTInt GADTOne
toTag 2 = SomeGADTInt GADTTwo
toTag 3 = SomeGADTInt GADTThree

wrap dfunc:

someDFunc :: SomeGADTInt -> SomeDt
someDFunc (SomeGADTInt i) = SomeDt i (dfunc i)

compose:

ff :: Int -> SomeDt
ff = someDFunc . toTag