Why doesn't this typecheck?

[goldfirere]

{-# LANGUAGE GADTs, PolyKinds, TypeOperators, TemplateHaskell,
             DataKinds, TypeFamilies, UndecidableInstances,
             FlexibleContexts, RankNTypes, ScopedTypeVariables,
             FlexibleInstances #-}
-- {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}

module Part5 where

import Prelude ( Bool(..), undefined, return )
import GHC.TypeLits ( type (-) )
import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Type.Equality
import Data.Singletons.CustomStar

data Nat :: * where
  Zero :: Nat
  Succ :: Nat -> Nat

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

data instance Sing (t :: *) where
  SNat  :: Sing Nat
  SBool :: Sing Bool

(+) :: Nat -> Nat -> Nat
Zero   + m = m
Succ n + m = Succ (n + m)
infixl 6 +

type family a :+ b where
  'Zero :+ m = m
  'Succ n :+ m = 'Succ (n :+ m)

type a ~> b = TyFun a b -> *

$(return [])

data Expr t (st :: Sing t) where
  Val  :: forall (t :: *) (st :: Sing t). t -> Expr t st
  Plus :: Expr Nat 'SNat -> Expr Nat 'SNat -> Expr Nat 'SNat
  If   :: Expr Bool 'SBool -> Expr t st -> Expr t st -> Expr t st

data instance Sing (e :: Expr t st) where
  SVal  :: Sing t -> Sing ('Val t)
  SPlus :: Sing a -> Sing b -> Sing ('Plus a b)
  SIf   :: Sing b -> Sing t -> Sing f -> Sing ('If b t f)

eval :: Expr t st -> t
eval (Val n)        = n
eval (e1 `Plus` e2) = eval e1 + eval e2
eval (If e0 e1 e2)  = if eval e0 then eval e1 else eval e2

type family Eval (x :: Expr t st) :: t where
  Eval ('Val n) = n
  Eval ('Plus e1 e2) = Eval e1 :+ Eval e2
  Eval ('If e0 e1 e2) = If (Eval e0) (Eval e1) (Eval e2)