Trying to figure out B. Milewski's slide from Lambda Jam 2019

Ind.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall #-}

module Ind where

import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import GHC.TypeNats (Nat, KnownNat, type (+), type (-))
import GHC.TypeLits (natVal)

-- data Nat where
--   Z :: Nat
--   S :: Nat -> Nat

-- deriving instance Show Nat

data Vec (n :: Nat) (a :: Type) where
  Nil :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (1 + n) a

deriving instance Show a => Show (Vec n a)

ind
  :: forall (a :: Type) (n :: Nat)
   . KnownNat n
  => Vec 0 a
  -> (  forall (m :: Nat)
      . KnownNat m
     => Proxy m
     -> Vec m a
     -> Vec (1 + m) a
     )
  -> Proxy n
  -> Vec n a
ind base step nProxy =
  if natVal nProxy == 0
    then base -- Type error ... fair enough
    else step (Proxy @(n - 1)) (ind base step (Proxy @(n - 1))) -- Type error

-- The second type error is pretty interesting to me. 
-- 
-- It wants to know that `n ~ 1 + (n - 1)`. 
-- If you add that to the context then it wants to know that `(n - 1) ~ (1 + (n - 1)) - 1` ... 
-- And so on. Cool.