I am trying to understand how to iterate over a singleton list of nats to produce the product of their integer value to use at runtime.
I have tried the following
listToInt :: forall (ns :: [Nat]). SList ns -> Integer listToInt SNil = 1 listToInt (SCons x xs) = natVal x * listToInt xs
but I get the following error:
• Could not deduce (KnownNat n1) arising from a use of ‘natVal’ from the context: ns ~ (n1 : n2) bound by a pattern with constructor: SCons :: forall a0 (n1 :: a0) (n2 :: [a0]). singletons-2.6:Data.Singletons.Internal.Sing n1 -> singletons-2.6:Data.Singletons.Internal.Sing n2 -> SList (n1 : n2), in an equation for ‘listToInt’ at src/Frechet/Eval.hs:18:12-21 Possible fix: add (KnownNat n1) to the context of the data constructor ‘SCons’ • In the first argument of ‘(*)’, namely ‘natVal x’ In the expression: natVal x * listToInt xs In an equation for ‘listToInt’: listToInt (SCons x xs) = natVal x * listToInt xs | 18 | listToInt (SCons x xs) = natVal x * listToInt xs | ^^^^^^^^
Any idea how to do this?