{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE NoIncoherentInstances #-}

-- {-# LANGUAGE ConstraintKinds -}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs, NoMonoLocalBinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
-- {-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-- Needed for a nested type family instance:
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

{-# LANGUAGE NoMonomorphismRestriction #-}

module Vivid.SynthDef.TypesafeArgs (

   -- * Type Set Operations
     SubsetBoolToBool -- (..)
   , ElemBoolToBool
   , SetInsert --(..)
   , SetEqual --(..)
   , SetUnion --(..)

   , IsSubsetOf --(..)
   , Bool_IsSubsetOf(..)
   , Subset -- (..)

   , IsElemOf
   , Bool_IsElemOf(..)
   , Elem

   -- * Type arguments
   , TagList(..)
   , VarList(..)
   , V
   , Vs(..)
      -- | This is aliased as 'V':
   , Variable(..)
   , I(..)
   , VarSet(..)
   , TypedVarList -- (..)
   , emptyVarSet
   , iToLiteralVar
   , iToVar
   , AddParams(..)

   -- * Other
--    , (?>) -- not exporting so it doesn't pollute namespace
   , toI
   , toF
   , GetSymbolVals(..)
   ) where

import Control.Arrow (first, second)
import GHC.Exts
import GHC.TypeLits
import qualified Data.Map as Map
import Data.Proxy
import Data.Type.Bool
import System.Random -- For a Random instance

type family SubsetBoolToBool (a :: Bool_IsSubsetOf) :: Bool where
   SubsetBoolToBool 'True_IsSubsetOf = 'True
   SubsetBoolToBool 'False_IsSubsetOf = 'False


type family ElemBoolToBool (a :: Bool_IsElemOf) :: Bool where
   ElemBoolToBool 'True_IsElemOf = 'True
   ElemBoolToBool 'False_IsElemOf = 'False

-- | So for example if you have:
-- 
--   @
--   foo = sd (440 ::I "freq") $ do
--      s <- sinOsc (freq_ (A::A "freq!!!"))
--      out 0 [s,s]
--   @
--
--   It'll tell you that you have an invalid synthdef with the error:
-- 
--   @
--     Couldn't match type ‘'False_IsSubsetOf’ with ‘'True_IsSubsetOf’
--                             In the first argument of ‘sinOsc’, namely
--       ‘(freq_ (V :: A "freq!!!"))’
--   @
data Bool_IsSubsetOf
   = True_IsSubsetOf
   | False_IsSubsetOf

type family SetInsert (s :: x) (sSet :: [x]) :: [x] where
   SetInsert e (e ': xs) = (e ': xs)
   SetInsert e xs = e ': xs

type family SetUnion (a :: [x]) (b :: [x]) :: [x] where
   SetUnion '[] bs = bs
   SetUnion (anA ': as) bs = SetUnion as (SetInsert anA bs)

type family SetUnions (a :: [[x]]) :: [x] where
   SetUnions '[] = '[]
   SetUnions (x ': xs) = SetUnion x (SetUnions xs)

-- | >>  .  :kind! SetIntersection '[4,3,4,5] '[7,5,3]
--   >> SetIntersection '[4,3,4,5] '[7,5,3] :: [GHC.TypeLits.Nat]
--   >> = '[3, 5]
type family SetIntersection (a :: [x]) (b :: [x]) :: [x] where
   SetIntersection a b = SetIntersectionPrime a b b

type family SetIntersectionPrime (a :: [x]) (b :: [x]) (allB :: [x]) :: [x] where
   SetIntersectionPrime '[] b allB = '[]
   SetIntersectionPrime (a ': as) '[] allB =
      SetIntersectionPrime as allB allB
   SetIntersectionPrime (a ': as) (a ': bs) allB =
      a ': SetIntersectionPrime as allB allB
   SetIntersectionPrime (a ': as) (b ': bs) allB =
      SetIntersectionPrime (a ': as) bs allB

type family IsSubsetOf (a :: [x]) (b :: [x]) :: Bool_IsSubsetOf where
   IsSubsetOf a b = IsSubsetOfPrime a b b

type family IsSubsetOfPrime (a :: [x]) (b :: [x]) (fullBs :: [x]) :: Bool_IsSubsetOf where
   IsSubsetOfPrime '[] b fullBs = 'True_IsSubsetOf
   IsSubsetOfPrime (a ': as) (a ': bs) fullBs =
      IsSubsetOfPrime as fullBs fullBs
   IsSubsetOfPrime (a ': as) (b ': bs) fullBs =
      IsSubsetOfPrime (a ': as) bs fullBs
   IsSubsetOfPrime as '[] fullBs = 'False_IsSubsetOf

data Bool_IsElemOf
   = True_IsElemOf
   | False_IsElemOf

-- Can rewrite in terms of IsSubsetOf
-- (And have 'Elem' vs 'IsElemOf' -- first is the constraint)
type family IsElemOf (a :: x) (l :: [x]) :: Bool_IsElemOf where
   IsElemOf a '[] = 'False_IsElemOf
   IsElemOf a (a ': b) = 'True_IsElemOf
   IsElemOf a (notA ': b) = IsElemOf a b

-- | >>  >  :kind! SetEqual '["bye", "hi","bye","bye"] '["bye","hi","hi"]
--   >> SetEqual '["bye","hi","bye","bye"] '["bye","hi","hi"] :: Bool
--   >> = 'True
type family SetEqual (a :: [x]) (b :: [x]) :: Bool where
   SetEqual a b = SubsetBoolToBool (IsSubsetOf a b) && SubsetBoolToBool (IsSubsetOf b a)



data Variable a  where
   V :: KnownSymbol a => Variable a

data Vs (a :: [Symbol]) = Vs

instance Show (Variable a) where
   show V = "(V::V " ++ show (symbolVal (Proxy::Proxy a)) ++ ")"

type V = Variable

{-
 >  getSymbolVals (Vs::Vs '["yes", "yes", "yall"])
["yes","yes","yall"]
-}

class GetSymbolVals x where
   getSymbolVals :: x -> [String]

instance GetSymbolVals (proxy '[]) where
   getSymbolVals _ = []

instance (KnownSymbol x, GetSymbolVals (Proxy (xs::[Symbol]))) =>
      GetSymbolVals (proxy (x ': xs)) where
   getSymbolVals _ =
      symbolVal (Proxy::Proxy x) : getSymbolVals (Proxy::Proxy xs)



data VarSet (s :: [Symbol]) = VarSet

instance (GetSymbolVals (VarSet xs)) => Show (VarSet xs) where
   show argSet =
      "(VarSet::VarSet "++show (getSymbolVals argSet)++")"

addVarToSet :: Variable sym -> VarSet syms -> VarSet (sym ': syms)
addVarToSet _ _ = VarSet

emptyVarSet :: VarSet '[]
emptyVarSet = VarSet

data I (x :: Symbol) where
   I :: (KnownSymbol x) => Float -> I x

instance (KnownSymbol s) => Show (I s) where
   show (I f) =
      "(" ++ show f ++ "::I " ++ show (symbolVal (Proxy::Proxy s)) ++ ")"
deriving instance (KnownSymbol s) => Eq (I s)
deriving instance (KnownSymbol s) => Read (I s)
deriving instance (KnownSymbol s) => Ord (I s)

toI :: (Real n, KnownSymbol a) => n -> I a
toI = I . realToFrac

toF :: (Real n) => n -> Float
toF = realToFrac

instance (KnownSymbol s) => Num (I s) where
   fromInteger = I . fromInteger
   (+) (I a) (I b) = I (a + b)
   (-) (I a) (I b) = I (a - b)
   abs (I a) = I (abs a)
   (*) (I a) (I b) = I (a * b)
   signum (I a) = I (signum a)

{-
 .  map (* 20) [3..5] :: [I "note"]
[(60.0::I "note"),(80.0::I "note"),(100.0::I "note")]-}
-- etc

instance (KnownSymbol s) => Fractional (I s) where
   fromRational = I . fromRational
   (/) (I a) (I b) = I (a / b)

instance (KnownSymbol s) => Enum (I s) where
   fromEnum (I f) = fromEnum f
   toEnum = I . toEnum

instance (KnownSymbol s) => Real (I s) where
   toRational (I f) = toRational f

instance (KnownSymbol s) => RealFrac (I s) where
   properFraction (I f) = second I $ properFraction f
   truncate (I f) = truncate f
   round (I f) = round f
   ceiling (I f) = ceiling f
   floor (I f) = floor f

instance (KnownSymbol s) => Floating (I s) where
   pi = I pi
   exp (I i) = I (exp i)
   log (I i) = I (log i)
   sin (I i) = I (sin i)
   cos (I i) = I (cos i)
   asin (I i) = I (asin i)
   acos (I i) = I (acos i)
   atan (I i) = I (atan i)
   sinh (I i) = I (sinh i)
   cosh (I i) = I (cosh i)
   asinh (I i) = I (asinh i)
   acosh (I i) = I (acosh i)
   atanh (I i) = I (atanh i)

instance (KnownSymbol s) => RealFloat (I s) where
   floatRadix (I i) = floatRadix i
   floatDigits (I i) = floatDigits i
   floatRange (I i) = floatRange i
   decodeFloat (I i) = decodeFloat i
   encodeFloat a b = I $ encodeFloat a b
   isNaN (I i) = isNaN i
   isInfinite (I i) = isInfinite i
   isDenormalized (I i) = isDenormalized i
   isNegativeZero (I i) = isNegativeZero i
   isIEEE (I i) = isIEEE i

instance (KnownSymbol s) => Random (I s) where
   randomR :: RandomGen g => (I s, I s) -> g -> (I s, g)
   randomR (I rangeLo, I rangeHi) gen =
      first I $ randomR (rangeLo, rangeHi) gen

   random :: RandomGen g => g -> (I s, g)
   random gen = first I (random gen)

type TypedVarList (c :: [Symbol]) = ([(String, Float)], VarSet c)

iToLiteralVar :: KnownSymbol s => I s -> (String, Float)
iToLiteralVar i@(I f) = (symbolVal i, f)

iToVar :: KnownSymbol s => I s -> V s
iToVar _ = V

infixr ?>
(?>) :: (KnownSymbol a, VarList b) => I a -> b -> TypedVarList (a ': InnerVars b)
(?>) a b =
   let (re, name) = makeTypedVarList b
   in (iToLiteralVar a : re, addVarToSet {- (iToArg a) -} V name)

class VarList from where
   type InnerVars from :: [Symbol]
   makeTypedVarList :: from -> TypedVarList (InnerVars from)

infixl `AddParams`

class TagList from where
   type AllTags from :: [Symbol]
   tagStrings :: from -> [String]

-- | Lets you combine sets of arguments. e.g.
-- 
--   > (1 ::I "foo", 2 ::I "bar") `AddParams` (3 ::I "baz")
-- 
--   means the same thing as
-- 
--   > (1 ::I "foo", 2 ::I "bar", 3 ::I "baz")
--   
-- 
--   This is left-biased, just like 'Map.union'
-- 
--   i.e. if you say:
-- 
--   > (99 ::I "same") `AddParams` (0 ::I "same")
-- 
--   It'll mean the same as
-- 
--   > (99 ::I "same")
data AddParams a b
   = (VarList a, VarList b) => AddParams a b

deriving instance (Show a, Show b) => Show (AddParams a b)

instance VarList (AddParams a b) where
   type InnerVars (AddParams a b) = SetUnion (InnerVars a) (InnerVars b)
   makeTypedVarList (a `AddParams` b) =
        let (Map.fromList -> fooA, _) = makeTypedVarList a
            (Map.fromList -> fooB, _) = makeTypedVarList b
            args = Map.toList $ fooA `Map.union` fooB
        in (args, VarSet :: VarSet (InnerVars (AddParams a b)))

{-
type family Subset (a :: [Symbol]) (b :: [Symbol]) :: Constraint where
   Subset a b = IsSubsetOf a b ~ 'True_IsSubsetOf

type family Elem (a :: Symbol) (b :: [Symbol]) :: Constraint where
   Elem a b = IsElemOf a b ~ 'True_IsElemOf
-}


type family Subset (as :: [Symbol]) (bs :: [Symbol]) :: Constraint where
   Subset '[] bs = ()
   Subset (a ': as) bs = (Elem a bs, Subset as bs)

type family Elem (a :: Symbol) (xs :: [Symbol]) :: Constraint where
   Elem a (a ': xs) = ()
   Elem a (x ': xs) = Elem a xs


-- INSTANCES:

-- | Wheeeeeeeeeeeeeeee!

instance VarList (TypedVarList a) where
   type InnerVars (TypedVarList a) = a
   makeTypedVarList = id

instance VarList () where
   type InnerVars () = '[]
   makeTypedVarList () = ([], emptyVarSet)

instance
   (KnownSymbol a) =>
   VarList (I a)
   where
      type InnerVars (I a) = '[a]
      makeTypedVarList x =
         ([iToLiteralVar (x)], VarSet::VarSet '[a])

instance
   (KnownSymbol a, KnownSymbol b) =>
   VarList (I a, I b)
   where
      type InnerVars (I a, I b) =
         '[a, b]
      makeTypedVarList (a,b) =
         a ?> b

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c) =>
   VarList (I a, I b, I c)
   where
      type InnerVars (I a, I b, I c) =
         '[a,b,c]
      makeTypedVarList (a,b,c) =
         a ?> b ?> c

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d) =>
   VarList (I a, I b, I c, I d)
   where
      type InnerVars (I a, I b, I c, I d) =
         '[a,b,c,d]
      makeTypedVarList (a,b,c,d) =
         a ?> b ?> c ?> d

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e) =>
   VarList
     (I a, I b, I c, I d, I e)
   where
      type InnerVars (I a, I b, I c, I d, I e) =
         '[a,b,c,d,e]
      makeTypedVarList (a,b,c,d,e) =
         a ?> b ?> c ?> d ?> e

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f) =
         '[a,b,c,d,e,f]
      makeTypedVarList (a,b,c,d,e,f) =
         a ?> b ?> c ?> d ?> e ?> f

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g) =
         '[a,b,c,d,e,f,g]
      makeTypedVarList (a,b,c,d,e,f,g) =
         a ?> b ?> c ?> d ?> e ?> f ?> g

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h) =
         '[a,b,c,d,e,f,g,h]
      makeTypedVarList (a,b,c,d,e,f,g,h) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i) =
         '[a,b,c,d,e,f,g,h,i]
      makeTypedVarList (a,b,c,d,e,f,g,h,i) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j) =
         '[a,b,c,d,e,f,g,h,i,j]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k) =
         '[a,b,c,d,e,f,g,h,i,j,k]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l) =
         '[a,b,c,d,e,f,g,h,i,j,k,l]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n

-- 15:
instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ,KnownSymbol u
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t ?> u


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ,KnownSymbol u,KnownSymbol v
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t ?> u ?> v


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ,KnownSymbol u,KnownSymbol v,KnownSymbol w
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t ?> u ?> v ?> w


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ,KnownSymbol u,KnownSymbol v,KnownSymbol w,KnownSymbol x
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w,I x)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w,I x) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t ?> u ?> v ?> w ?> x


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ,KnownSymbol u,KnownSymbol v,KnownSymbol w,KnownSymbol x,KnownSymbol y
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w,I x,I y)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w,I x,I y) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t ?> u ?> v ?> w ?> x ?> y


instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ,KnownSymbol p,KnownSymbol q,KnownSymbol r,KnownSymbol s,KnownSymbol t
   ,KnownSymbol u,KnownSymbol v,KnownSymbol w,KnownSymbol x,KnownSymbol y
   ,KnownSymbol z
   ) =>
   VarList
     (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w,I x,I y,I z)
   where
      type InnerVars (I a, I b, I c, I d, I e, I f, I g, I h, I i, I j, I k, I l, I m, I n, I o,I p,I q,I r,I s,I t,I u,I v,I w,I x,I y,I z) =
         '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z]
      makeTypedVarList (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z) =
         a ?> b ?> c ?> d ?> e ?> f ?> g ?> h ?> i ?> j ?> k ?> l ?> m ?> n ?> o ?> p ?> q ?> r ?> s ?> t ?> u ?> v ?> w ?> x ?> y ?> z




(##) :: (KnownSymbol a, TagList b) => V a -> b -> [String]
(##) (_::V a) b = symbolVal (Proxy::Proxy a) : tagStrings b

instance TagList () where
   type AllTags () = '[]
   tagStrings () = []

instance (KnownSymbol a) => TagList (V a) where
   type AllTags (V a) = '[a]
   tagStrings (_ :: V a) = [symbolVal (Proxy::Proxy a)]

instance (KnownSymbol a, KnownSymbol b) => TagList (V a, V b) where
   type AllTags (V a, V b) = '[a, b]
   tagStrings (a,b) = a ## b

-- Also works:
-- instance (KnownSymbol a , TagList (V b,V c)) => TagList (V a, V b, V c) where
instance (KnownSymbol a, KnownSymbol b, KnownSymbol c) => TagList (V a, V b, V c) where
   type AllTags (V a, V b, V c) = '[a, b, c]
   tagStrings (a,b,c) = a ## (b,c)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d) =>
      TagList (V a,V b,V c,V d) where
   type AllTags (V a,V b,V c,V d) =
      '[a,b,c,d]
   tagStrings (a,b,c,d) = a ## (b,c,d)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e) =>
      TagList (V a,V b,V c,V d,V e) where
   type AllTags (V a,V b,V c,V d,V e) =
      '[a,b,c,d,e]
   tagStrings (a,b,c,d,e) = a ## (b,c,d,e)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f
   ) =>
      TagList (V a,V b,V c,V d,V e,V f) where
   type AllTags (V a,V b,V c,V d,V e,V f) =
      '[a,b,c,d,e,f]
   tagStrings (a,b,c,d,e,f) = a ## (b,c,d,e,f)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g) =
      '[a,b,c,d,e,f,g]
   tagStrings (a,b,c,d,e,f,g) = a ## (b,c,d,e,f,g)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h) =
      '[a,b,c,d,e,f,g,h]
   tagStrings (a,b,c,d,e,f,g,h) = a ## (b,c,d,e,f,g,h)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i) =
      '[a,b,c,d,e,f,g,h,i]
   tagStrings (a,b,c,d,e,f,g,h,i) = a ## (b,c,d,e,f,g,h,i)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j) =
      '[a,b,c,d,e,f,g,h,i,j]
   tagStrings (a,b,c,d,e,f,g,h,i,j) = a ## (b,c,d,e,f,g,h,i,j)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k) =
      '[a,b,c,d,e,f,g,h,i,j,k]
   tagStrings (a,b,c,d,e,f,g,h,i,j,k) = a ## (b,c,d,e,f,g,h,i,j,k)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l) =
      '[a,b,c,d,e,f,g,h,i,j,k,l]
   tagStrings (a,b,c,d,e,f,g,h,i,j,k,l) = a ## (b,c,d,e,f,g,h,i,j,k,l)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l,V m) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l,V m) =
      '[a,b,c,d,e,f,g,h,i,j,k,l,m]
   tagStrings (a,b,c,d,e,f,g,h,i,j,k,l,m) = a ## (b,c,d,e,f,g,h,i,j,k,l,m)

instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l,V m,V n) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l,V m,V n) =
      '[a,b,c,d,e,f,g,h,i,j,k,l,m,n]
   tagStrings (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = a ## (b,c,d,e,f,g,h,i,j,k,l,m,n)

-- 15:
instance
   (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbol d, KnownSymbol e,
    KnownSymbol f, KnownSymbol g, KnownSymbol h, KnownSymbol i, KnownSymbol j,
    KnownSymbol k, KnownSymbol l, KnownSymbol m, KnownSymbol n, KnownSymbol o
   ) =>
      TagList (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l,V m,V n,V o) where
   type AllTags (V a,V b,V c,V d,V e,V f,V g,V h,V i,V j,V k,V l,V m,V n,V o) =
      '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o]
   tagStrings (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = a ## (b,c,d,e,f,g,h,i,j,k,l,m,n,o)