[Haskell-cafe] question about "singletons"

[TP]

Hi all,


Following a discussion on Haskell Cafe some time ago (1), Roman C. wrote:

"""
On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have
any inhabitants — only types of kind * do.
"""

Indeed, this is what seems to occur in the following example:

-----------------------
{-# LANGUAGE DataKinds #-}

data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )

main = do

let one = undefined :: 'Succ 'Zero
print one
-----------------------

We obtain an error (ghc 7.6.2):
-----------------------
    Kind mis-match
    Expected kind `OpenKind', but `Succ Zero' has kind `Nat'
    In an expression type signature: Succ Zero
    In the expression: undefined :: Succ Zero
    In an equation for `one': one = undefined :: Succ Zero
-----------------------

(note that the error is slightly different in the HEAD version of GHC (2)).
Is it related to the sentence "As bottom is an inhabitant of every type 
(though with some caveats concerning types of unboxed kind), bottoms can be 
used wherever a value of that type would be. " found at address (3)? Here we 
have a non-* kind, such that bottom would not be an inhabitant of ('Succ 
'Zero). Why is this so? This seems to be an assumed choice (4), but I would 
like to understand the reason for this design, which makes necessary to use 
singletons, as explained at (4).

Now, if I use a singleton to make my example work, I obtain an error when 
trying to make the type (Sing a) an instance of Show:

-----------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )

data Sing :: a -> *

deriving instance Show (Sing a)

main = do

let one = undefined :: Sing ('Succ 'Zero)
print one
-----------------------

The error is simply:

-----------------------
test_noinhabitant_corrected.hs: Void showsPrec
-----------------------

Why?

Thanks,

TP


References:
----------

(1):
https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/AltmX5iCFi8

(2):
-----------------------
    Expected a type, but ‛Succ Zero’ has kind ‛Nat’
    In an expression type signature: Succ Zero
    In the expression: undefined :: Succ Zero
    In an equation for ‛one’: one = undefined :: Succ Zero
-----------------------

(3):
http://www.haskell.org/haskellwiki/Bottom

(4):
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics

"""
Both numeric and symbol literal types are empty---they have no inhabitants. 
However, they may be used as parameters to other type constructors, which 
makes them useful. 
"""

"""
A singleton type is simply a type that has only one interesting inhabitant.
"""