product.hs

{-# language FlexibleInstances, DataKinds, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableInstances, UndecidableSuperClasses, FunctionalDependencies, PolyKinds #-}

import GHC.Exts
import GHC.TypeLits

import Data.Proxy

type family AllC (c :: k -> Constraint) (xs :: [k]) :: Constraint where
    AllC _ '[] = ()
    AllC c (k ': ks) = (c k, AllC c ks)

class (KnownNat res, AllC KnownNat ns) => Product (ns :: [Nat]) (res :: Nat) | ns -> res

instance {-# Overlapping #-} KnownNat n => Product '[n] n

instance
    ( KnownNat res
    , KnownNat n
    , KnownNat answer
    , answer ~ (n * res)
    , Product ns res
    , AllC KnownNat ns
    ) => Product (n ': ns) answer
    
-- *Main Data.Proxy> :t mult (Proxy :: Proxy '[1,3,3])
-- mult (Proxy :: Proxy '[1,3,3]) :: Proxy 9

mult :: Product ns m => Proxy ns -> Proxy m
mult _ = Proxy