Difficulty in trying to implement a type-safe `at` for length-indexed vectors

I have just learnt about the DataKinds extension, type-level literals, and found out that type-levels natural numbers can be compared using constraints provided in the Data.Type.Ord such as (>), and manipulated using type-level operations provided in GHC.TypeNats such as (+).

With these in mind, I came across the idea of implementing a safe version of !! for length-indexed vectors. The idea is simple: you pass in an ix :: Natural as the index, and a vec :: Vec len a with length len and type a, and you get the element at index ix. The compiler should detect and shout at you for any illegal ix (ix < 0 || ix >= len) or vec (whose len == 0).

So I began by defining the type signature for such safeAt (imports and magic comments of extensions ignored):

infixr 5 :.
data Vec :: Nat -> * -> * where
  Nil :: Vec 0 a
  (:.) :: a -> Vec m a -> Vec (m + 1) a

safeAt :: forall (ix :: Nat) (len :: Nat) (proxy :: Nat -> *) a.
            (KnownNat ix, {- ix >= 0, -} len >= 1, ix < len) =>
              proxy ix -> Vec len a -> a
safeAt = undefined

Working as intended:

v :: Vec 10 Int
v = 1 :. 2 :. 3 :. 4 :. 5 :. 6 :. 7 :. 8 :. 9 :. 10 :. Nil

ok :: Int
ok = safeAt (Proxy :: Proxy 3) v

oops :: Int
oops = safeAt (Proxy :: Proxy 10) v  -- expected compilation error

Here I made use of a proxy to hold the ix at the type-level so it can be checked by the type-level constraints. This however became a problem when I try to implement safeAt:

safeAt p (x:.xs) = case natVal p of
                     0 -> x
                     n -> safeAt (??? (n - 1)) xs

I need to promote (n - 1) to Proxy :: Proxy (n - 1). I cannot work out such function, not even writing out its type signature, and came to doubt if such a type-dependent function would even exist in the Haskell's typing system. I know you can pull down a Nat from type-level to term-level using natVal, but is there a "reverse" of this? Maybe there's a magic function out there that I don't know? Also I believe there are other problems in this implementation, such as how would you comfort the compiler that (ix - 1) is KnownNat and (len - 1) >= 1 still given the proxy p is not holding a 0. Maybe there are some alternative approaches out there to implement safeAt in a non-recursive way? I have so much confusions.

Solution

Proxies are a mostly obsolete/legacy thing since -XTypeApplications and -XAllowAmbiguousTypes have been available. Using these extensions together with -XScopedTypeVariables gives you almost everything proxies can do.

In many cases, including yours, that's not enough though: you need something stronger than proxies to propagate the KnownNat constraint. Singletons offer that capability. A Sing n for n :: Nat packs the KnownNat constraint in a value like a proxy, in a way that you can carry out computations with it.

Throwing in the big singletons-base package (kinda overkill), you can start with the following:

{-# LANGUAGE TypeApplications #-}

import Prelude.Singletons (SNum(..), sing)
import Data.Kind (Type)

safeAt :: forall (ix :: Nat) (len :: Nat) a.
              Sing ix -> Vec len a -> a
safeAt i (x:.xs) = case fromSing i of
                     0 -> x
                     _ -> safeAt (i %- sing @1) xs

Of course that's not all: how do we express those size constraints?
It seems obvious that ix < len implies ix-1 < len-1, but this is the kind of trivial thing compilers tend to disagree with.

Welcome to the joy of dependently-typed programming!

...There's definitely work on getting this kind of thing behaving smoothly, both in GHC itself and the singletons-presburger plugin but I'm not sure how well it works.

Pragmatically speaking, you may be better off with a different approach: either

Don't bother doing dependently-typed recursion. Instead, just use an unsafe implementation underneath and add the type constraints on top. This is IMO the idiomatic Haskell solution for problems like this. Of course it doesn't offer the same correctness-verification level as a fully-dependent-total version, but if you need that then you should use Agda or Idris instead of Haskell.
Express it with Peano numbers. Induction over these is just ordinary pattern matching.
Put the indexing into the value level (which is probably more useful anyway), but with a range-limited type. finite-typelits offers that.

In the first version, you don't need any proxies or singletons. This will do:

{-# LANGUAGE ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes #-}

unsafeAt :: Integer -> Vec len a -> a
unsafeAt = ...

safeAt :: ∀ ix len a . (KnownNat len, KnownNat ix, ix >= 0, ix < len)
  => Vec len a -> a
safeAt = unsafeAt (natVal @ix Proxy)