Sorry I left out some important information.
I'm trying to understand how to write a function that takes an Integer and
produces a value with a Nat corresponding to that Integer, such that the
compiler can infer the type.
The whole example based on
http://www.howtobuildsoftware.com/index.php/how-do/hUF/haskell-dependent-typ...
:
On Sun, Feb 28, 2016 at 4:40 PM Jake
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables, GADTs, AllowAmbiguousTypes #-}
import GHC.TypeLits import Data.Proxy import Data.Type.Equality
data NatString (n :: Nat) = NatString String deriving Show
showNS :: KnownNat n => NatString n -> (String, Integer) showNS b@(NatString s) = (s, natVal b)
In this example, we use NatString like this:
showNS (NatString "hey" :: NatString 4) -- ("hey", 4)
We can then dynamically make NatStrings from Integers. For example, we can read an Integer from stdin and use it to create a NatString
main :: IO () main = do i <- readLn case someNatVal i of Just (SomeNat (p :: Proxy n)) -> let ns :: NatString n ns = NatString "hello!" in print $ showNS NatString
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. 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.
fromN :: forall n. KnownNat n => Integer -> NatString n fromN i = case someNatVal i of Just (SomeNat p) -> case sameNat p (Proxy :: Proxy n) of Just (Refl) -> let ns :: NatString n ns = NatString "hello!" in ns
This compiles, but if you try and use it the compiler complains.
showNS (fromN 3) -- No instance for (KnownNat n0) arising from a use of ‘showNS’
If we manually add the type annotation, everything is fine, but that kind of defeats the entire purpose.
showNS (fromN 3 :: NatString 3) -- ("hello!",3)
Strangely enough, when the NatString is immediately consumed instead of being returned, the compiler does its job and infers the correct type.
showFromN :: Integer -> (String, Integer) showFromN i = case someNatVal i of Just (SomeNat (p :: Proxy n)) -> let ns :: NatString n ns = NatString "hello!" in showNS ns
showFromN 3 -- ("hello!", 3)
Clearly the intermediate value of ns inside of showFromN has a type NatString 3 because showNS is using that fact. How can I make the compiler infer that fromN 3 :: NatString 3 separately?