Hi Haskellers!
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]).
singletons2.6:Data.Singletons.Internal.Sing n1
> singletons2.6:Data.Singletons.Internal.Sing n2
> SList (n1 : n2),
in an equation for ‘listToInt’
at src/Frechet/Eval.hs:18:1221
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?
Thanks!
Ahmad Salim