Now I see that since you don't have a type list anywhere in the return type, you might try to use type classes: (works with GHC context stack set to at least one more than the value of N) ------- {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE PolyKinds #-} import GHC.TypeLits import Data.Proxy import Data.Singletons data Haar (a :: Nat) (b :: Nat) = Haar { unHaar :: Double -> Double } haar :: forall n k . (KnownNat n, KnownNat k, (2 * k - 1 <=? 2^n - 1) ~ 'True) => Haar n (2 * k - 1) haar = Haar g where g t | (k' - 1) * 2 ** (-n') < t && t <= k' * 2 ** (-n') = 2 ** ((n' - 1) / 2) | k' * 2 ** (-n') < t && t <= (k' + 1) * 2 ** (-n') = -2 ** ((n' - 1) / 2) | otherwise = 0 where n' = fromIntegral (natVal (Proxy :: Proxy n)) k' = 2 * (fromIntegral (natVal (Proxy :: Proxy k))) - 1 data Natural = Z | S Natural type family FromNat n where FromNat Z = 0 FromNat (S n) = 1 + (FromNat n) type family ToNat i where ToNat 0 = Z ToNat n = S (ToNat (n - 1)) class Upto n where upto :: sing n -> [Integer] instance Upto Z where upto _ = [] instance (KnownNat (FromNat n), Upto n) => Upto (S n) where upto _ = natVal (undefined :: sing (FromNat n)) : upto (undefined :: sing n) class MapHaar (n :: Nat) (xs :: [(Nat,Nat)]) where maphaar :: sing1 n -> sing2 xs -> [[(Double, Double)]] instance MapHaar n '[] where maphaar _ _ = [] instance (Upto (ToNat n), MapHaar n xs, b ~ (2 * k - 1), b <= 2^a - 1, KnownNat n, KnownNat k, KnownNat a) => MapHaar n ('(a,b) ': xs) where maphaar sn _ = h : t where l = map (\i -> fromIntegral i / fromIntegral (natVal sn)) $ upto (undefined :: sing (ToNat n)) h = map (\x -> (x, unHaar (haar :: Haar a b) x)) l t = maphaar sn (undefined :: sing xs) data instance Sing 100 = S100 foo = maphaar S100 (undefined :: sing '[ '(1,1), '(2,1), '(2,3), '(3,1), '(3,5), '(3,7)]) ----- Regards, Marcin