Extracting values from arbitrary un-Known Nats

Question

Given the type-level list function (from this blog post)

type family Length (xs :: [*]) :: Nat where
    Length '[] = 0
    Length (_ ': xs) = 1 + Length xs

The value extraction of 'hard-coded' type-list lengths works as expected

t1 :: Integer
t1 = natVal (Proxy :: Proxy (Length '[Int]))

And t1 = 1. However, making a function to get the value from an arbitrary list seems to fail.

t2 :: forall (xs :: [*]). Proxy xs -> Integer
t2 _ = natVal (Proxy :: Proxy (Length xs))

Gives the error

    • No instance for (KnownNat (Length xs))
        arising from a use of ‘natVal’

Which seems unfortunate but reasonable since only the literals are 'Known'. However, forcing the constraint to be satisfied as follows results in complaints about ambiguous types.

unsafeKnownConstr :: c :~: (KnownNat n :: Constraint)
unsafeKnownConstr = unsafeCoerce Refl

t3 :: forall (xs :: [*]). Proxy xs -> Integer
t3 _ = case Proxy :: Proxy (Length xs) of
         p@(_ :: Proxy l) -> case unsafeKnownConstr @(KnownNat l) of
                             Refl -> natVal @l p

Specifically,

    • Could not deduce (KnownNat n0) arising from a use of ‘natVal’
      from the context: KnownNat n0 ~ KnownNat (Length xs)
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a case alternative
...
      The type variable ‘n0’ is ambiguous

What is GHC (8.10.4) complaining about here? Alternatively, is there another way to extract these un-Known Nats?

Answer 1

You can do this:

t4 :: forall n xs. (n ~ Length xs, KnownNat n) => Proxy xs -> Integer
t4 _ = natVal $ Proxy @n

This says your callers have to know the type level list xs well enough to fully resolve Length xs to fixed value, for which they'll be able to produce a KnownNat instance.¹ But inside t4 you get to operate on lists you don't statically know.

λ t4 $ Proxy @[Int, Char, Bool]
3
it :: Integer

---

Your attempt didn't work because unsafeKnownConstr has type forall c n. c :~: KnownNat n. It promises that for any constraint c you like, it can prove that the constraint is equal to KnownNat n for any n you like.

Quite apart from how that is obviously a false promise, when you use unsafeKnownConstr @(KnownNat l) you're only setting c. n is still a type variable that can be instantiated to anything. GHC doesn't know what to pick for n; that's the ambiguous type variable GHC is complaining about. Effectively you've lied and told it that any arbitrarily chosen n is equal to the length of the list, but you haven't actually chosen the n to use, so GHC has no way of telling what KnownNat dictionary you want to consider (falsely) the KnownNat dictionary for Length xs.

If you fix the second type parameter for unsafeKnownConstr, then you can get something like this to compile:

t3 :: forall (xs :: [*]). Proxy xs -> Integer
t3 _ = case Proxy :: Proxy (Length xs) of
         p@(_ :: Proxy l) -> case unsafeKnownConstr @(KnownNat l) @17928 of
                             Refl -> natVal @l p

Which then allows you to do this in GHCI:

λ t3 $ Proxy @[Int, Char, Bool]
17928
it :: Integer

Whatever value you choose, though, unsafely coercing KnownNat constraints isn't going to be very useful to you because they do actually contain information: the value that is known for the Nat!

---

¹ Or they too can punt on solving it and pass the constraints on to their own callers via their own types.