<div dir="ltr"><div style="font-size:13px;line-height:19.5px"><div>{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables, GADTs, AllowAmbiguousTypes #-}</div><div><br></div><div>import GHC.TypeLits</div><div>import Data.Proxy</div><div>import Data.Type.Equality</div><div><br></div><div>data NatString (n :: Nat) = NatString String deriving Show</div><div><br></div><div>showNS :: KnownNat n => NatString n -> (String, Integer)</div><div>showNS b@(NatString s) = (s, natVal b)</div><div><br></div><div>In this example, we use NatString like this:</div><div><br></div>> showNS (NatString "hey" :: NatString 4)</div><div style="font-size:13px;line-height:19.5px"><div>-- ("hey", 4)</div><div><br></div></div><div style="font-size:13px;line-height:19.5px">We can then dynamically make NatStrings from Integers. For example, we can read an Integer from stdin and use it to create a NatString</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px"><div>main :: IO ()</div><div>main = do</div><div>  i <- readLn</div><div>  case someNatVal i of</div><div>    Just (SomeNat (p :: Proxy n)) -></div><div>      let ns :: NatString n</div><div>          ns = NatString "hello!"</div><div>      in print $ showNS NatString</div></div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">However, if I have trouble when I try to refactor out the middle part to create a function with type forall n. KnownNat n => Integer -> Bar n.</div><div style="font-size:13px;line-height:19.5px">I use sameNat to convince the compiler that the Nat we get from the Integer is the same type as the the type n of the output.</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px"><div>fromN :: forall n. KnownNat n => Integer -> NatString n</div><div>fromN i =</div><div> case someNatVal i of</div><div>   Just (SomeNat p) -></div><div>     case sameNat p (Proxy :: Proxy n) of</div><div>       Just (Refl) -></div><div>         let ns :: NatString n</div><div>             ns = NatString "hello!" in ns</div></div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">This compiles, but if you try and use it the compiler complains.</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">> showNS<span style="color:rgb(0,0,0)"> (fromN 3)</span></div><div style="font-size:13px;line-height:19.5px">-- <span style="color:rgb(0,0,0)">No instance for (KnownNat n0) arising from a use of ‘showNS’</span></div><div style="font-size:13px;line-height:19.5px"><span style="color:rgb(0,0,0)"><br></span></div><div style="font-size:13px;line-height:19.5px"><span style="color:rgb(0,0,0)">If we manually add the type annotation, everything is fine, but that kind of defeats the entire purpose.</span></div><br style="font-size:13px;line-height:19.5px"><span style="font-size:13px;line-height:19.5px">> showNS (fromN 3 :: NatString 3)</span><br style="font-size:13px;line-height:19.5px"><span style="font-size:13px;line-height:19.5px">-- ("hello!",3)</span><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">Strangely enough, when the NatString is immediately consumed instead of being returned, the compiler does its job and infers the correct type.</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px"><div>showFromN :: Integer -> (String, Integer)</div><div>showFromN i =</div><div> case someNatVal i of</div><div>   Just (SomeNat (p :: Proxy n)) -></div><div>     let ns :: NatString n</div><div>         ns = NatString "hello!" in showNS ns</div></div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">> showFromN 3</div><div style="font-size:13px;line-height:19.5px">-- ("hello!", 3)</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">Clearly the intermediate value of ns inside of showFromN has a type NatString 3 because showNS is using that fact.</div><div style="font-size:13px;line-height:19.5px">How can I make the compiler infer that fromN 3 :: NatString 3 separately?</div></div>