Oh… this works.

PlusZero.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module PlusZero where

import Data.Type.Equality

data Nat
  = Zero
  | Succ Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat where
  Plus 'Zero m     = m
  Plus ('Succ n) m = 'Succ (Plus n m)

data SNat (n :: Nat) where
  SZero :: SNat 'Zero
  SSucc :: SNat n -> SNat ('Succ n)

congSucc :: a :~: b -> 'Succ a :~: 'Succ b
congSucc Refl = Refl

plusZero :: SNat n -> Plus n 'Zero :~: n
plusZero SZero     = Refl
plusZero (SSucc n) = congSucc (plusZero n)