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. """