Pattern match(es) are non-exhaustive

Test.hs

{-# LANGUAGE DataKinds
           , KindSignatures
           , TypeFamilies
           , GADTs
           , TypeOperators
           , ScopedTypeVariables
           , MultiParamTypeClasses
           , FlexibleInstances
           , StandaloneDeriving
           , RankNTypes
           , FlexibleContexts
           , ConstraintKinds #-}

data Level = Core
           | Unbound
           | Syntax

data SLevel (l :: Level) where
    SCore    :: SLevel Core
    SUnbound :: SLevel Unbound
    SSyntax  :: SLevel Syntax

class Sing a where
    sing :: a

instance Sing (SLevel Core)    where sing = SCore
instance Sing (SLevel Unbound) where sing = SUnbound
instance Sing (SLevel Syntax)  where sing = SSyntax

type CLevel (l :: Level) = Sing (SLevel l)

type family Sup (a :: Level) (b :: Level) :: Level where
    Sup Syntax  x       = Syntax
    Sup x       Syntax  = Syntax
    Sup Unbound b       = Unbound
    Sup x       Unbound = Unbound
    Sup x       x       = Core

data Term (l :: Level) where
    S    :: Term Core
    K    :: Term Core
    I    :: Term Core
    (:$) :: (CLevel a, CLevel b) => Term a -> Term b -> Term (Sup a b)
    Var  :: String -> Term Unbound
    Lam  :: CLevel a => String -> Term a -> Term Syntax
    Let  :: (CLevel a, CLevel b) => String -> Term a -> Term b -> Term Syntax

infixr 1 :$

levelOf :: CLevel a => Term a -> SLevel a
levelOf _ = sing

reduce :: Term Core -> Term Core
reduce (I :$ x) = case levelOf x of
                    SCore -> reduce x
                    -- SUnbound -> undefined
                    -- SSyntax -> undefined
reduce t = t

main :: IO ()
main = undefined