Hi Ken,
ideally, you'd want something like
f1 :: TypeLits.SomeNat -> exists n . Foo n
to indicate that this function will produce a Foo with some natural number, but you don't know beforehand what that number is.
However, Haskell doesn't have built-in existential quantification (yet), so you have to use some encoding that uses existing features instead.
There's at least two ways to do this. The first is to use an "existential data type":
data SomeFoo = forall n . MkSomeFoo (Foo n)
You'll notice that it's named quite similarly to SomeNat - that's because SomeNat is also an existential data type.
Then you could have a function like
showSomeFoo :: SomeFoo -> String
showSomeFoo (MkSomeFoo x) = show x
The other way is to pass in a function that tells f1 what to do with Foo it produces:
f1 :: TypeLits.SomeNat -> (forall fn . Foo fn -> a) -> a
f1 mynat f = case mynat of {
TypeLits.SomeNat (_ :: Proxy n) -> let {
x :: Foo n;
x = Mkfoo;
} in f x
};
In this case, you could call `f1 someNat show` to show a Foo made from someNat.
These two encodings are equally powerful, but sometimes one is more convenient than the other.
Cheers,
Jakob