Visible quantification???

Whole.hs

{-# LANGUAGE GADTs        #-}
{-# LANGUAGE GADTs        #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType   #-}
module Data.Whole where

import Data.Kind (Type)

data Sign = Positive | Negative

data Whole :: Sign -> Type where
  Z :: Whole either
  S :: Whole 'Positive -> Whole 'Positive
  P :: Whole 'Negative -> Whole 'Negative

type family Succ (x :: Whole sign)
    :: Whole (SuccSign x) where
  Succ  'Z     = 'S  'Z
  Succ ('S  x) = 'S ('S x)
  Succ ('P 'Z) = 'Z
  Succ ('P  x) =  x

type family SuccSign (x :: Whole sign) :: Sign where
  SuccSign  'Z     = 'Positive
  SuccSign ('S  x) = 'Positive
  SuccSign ('P 'Z) = forall k -> k -- ?????
  SuccSign ('P  x) = 'Negative