Combining `SomeNat` and `Nat`

Question

I was following the example set out in the question Can I have an unknown KnownNat?

I wanted to make a small change to the code.

The original code was

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: (KnownNat n) => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let a :: Bar n
                a = Bar "as"
            print $ bar a

which works as expected. I wanted to make a change in which I modify the type level n.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: (KnownNat n) => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let a :: Bar (n + 5)
                a = Bar "as"
            print $ bar a

The error message I get is

    Could not deduce (KnownNat (n + 5)) arising from a use of ‘bar’
    from the context (KnownNat n)
      bound by a pattern with constructor
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,
               in a case alternative
      at Blag.hs:19:9-30
    In the second argument of ‘($)’, namely ‘bar a’
    In a stmt of a 'do' block: print $ bar a
    In the expression:
      do { let a :: Bar (n + 5)
               a = Bar "as";
           print $ bar a }
Failed, modules loaded: none.

Why can't the compiler deduce KnownNat (n + 5) from KnownNat n?

My guess is that GHC is unable to reduce `n + 5` to any type of normal form, and because of that it can't go looking up type class instances - because it doesn't know what it's looking for! Without knowing what `n` is, evaluation of `n + 5` can't proceed (assuming the classic problem of defining + by induction on the left argument). I don't quite know the magic behind how KnownNat works, but it probably only knows how to find that instance if it is given a concrete type. — ocharles, Sep 01 '15 at 12:40
GHC has no idea that `n + 5` is known if `n` is known. The only `Nat` expressions that are known are the numeric literals. On the other hand, if you use custom unary numbers on the type level and implement known-ness and addition inductively, it may result in more facts being apparent to GHC, including the implication in question. — András Kovács, Sep 01 '15 at 13:18
If the only `Nat` expressions that are known are numeric literals, how does the first example work? — Alpaca, Sep 01 '15 at 22:21

score 1 · Answer 1 · answered Sep 27 '15 at 05:49

The first example works by the pure magic of someNatVal, which manufactures a type-level Nat and knowledge to go with it. In the second example, you have knowledge of n, but you're asking about n+5. There are two reasons this won't work.

The first problem is that the type system would see all the "extra" instances as incoherent. That is, it would need to know KnownNat 2 and KnownNat 7 and also KnownNat n => KnownNat (n + 5) and KnownNat n => KnownNat (5 + n) and so on. These instances would all clash with each other, so the compiler would need special built-in knowledge about how to deal with the situation, and everything would be rather painful.

The other problem is that TypeLits are pretty simple-minded. They don't seem to have the useful inductive structure you'd expect from type-level naturals.

As a result of these problems, it seems that for many purposes, the easy and efficient TypeLit mechanism must be set aside in favor of The Slow Way, hand-built unary natural numbers that you can find in singleton-nats. You need separate functions to deal with computations on the value and type levels, but at least the type checker will make sure they match up properly, and there's some Template Haskell about to try to make it easier to write both at once.

Combining `SomeNat` and `Nat`

1 Answers1