{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module TySet where

import Data.Typeable
import GHC.TypeLits

class UpdateCompose (k :: Nat) (v :: Nat) where
  update :: Proxy k -> Proxy v -> [Double] -> [Double]

instance UpdateComposeCase (k <=? v) k v => UpdateCompose k v where
  update = updateCase (Proxy :: Proxy (k <=? v))

class UpdateComposeCase (leq :: Bool) (k :: Nat) (v::Nat) where
  updateCase :: Proxy leq -> Proxy k -> Proxy v -> [Double] -> [Double]

instance UpdateComposeCase True k v where
  updateCase _ _ _ = id
instance UpdateComposeCase False k v where
  updateCase _ _ _ = error "Something meaningful"