[Haskell-cafe] help with existential type signature?

[Ken T Takusagawa]

{-
I am experimenting with type-level naturals and with moving 
values known at runtime to type space.

Is there a type signature that I can add to f1 below so that 
this will compile (maybe also requiring some additional 
LANGUAGE pragmas)?

If I were to change the return value of f1 from "x" to "show 
x", then the program does compile, suggesting that there's 
nothing inherently wrong with "x".  But I'd prefer the 
option to compose the output of f1 with other computations 
separately, e.g., "show . f1" .

Thanks,
Ken

-}

{-# LANGUAGE KindSignatures, ScopedTypeVariables, DataKinds, Rank2Types #-}
import qualified GHC.TypeLits as TypeLits;
import Data.Proxy(Proxy);
main = undefined;

data Foo (fn :: TypeLits.Nat) = Mkfoo deriving (Show);

--f1 :: TypeLits.SomeNat -> ? ;
f1 mynat = case mynat of {
  TypeLits.SomeNat (_ :: Proxy n) -> let {
    x :: Foo n;
    x = Mkfoo;
  } in x
};

{-
typelits.hs:27:8: error:
    * Couldn't match expected type `p' with actual type `Foo n'
        because type variable `n' would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor:
          TypeLits.SomeNat :: forall (n :: TypeLits.Nat).
                              TypeLits.KnownNat n =>
                              Proxy n -> TypeLits.SomeNat,
        in a case alternative
        at smalltypelits2.hs:24:3-33
    * In the expression: x
      In the expression:
        let
          x :: Foo n
          x = Mkfoo
        in x
      In a case alternative:
          TypeLits.SomeNat (_ :: Proxy n)
            -> let
                 x :: Foo n
                 x = Mkfoo
               in x
    * Relevant bindings include
        x :: Foo n (bound at smalltypelits2.hs:26:5)
        f1 :: TypeLits.SomeNat -> p (bound at smalltypelits2.hs:23:1)
   |
27 |   } in x
   |        ^
-}