Singletons TypeRepStar Sing Data Instance

Question

I'm new to Haskell, so I'm probably missing something obvious, but what seems to be the problem here?

The singletons library provides a Sing instance for the kind * in import Data.Singletons.TypeRepStar.

The Sing data family is defined as follows..

data family Sing (a :: k)

and the * instance is defined as..

data instance Sing (a :: *) where
  STypeRep :: Typeable a => Sing a

I'm trying to reproduce a minimal version of this using the following ...

{-# LANGUAGE GADTs
           , TypeFamilies
           , PolyKinds
           #-}

module Main where

import Data.Typeable

data family Bloop (a :: k)
data instance Bloop (a :: *) where
  Blop :: Typeable a => Bloop a

main :: IO ()
main = putStrLn "Hello, Haskell!"

But I'm getting the following error...

Main.hs:12:3: error:
    • Data constructor ‘Blop’ returns type ‘Bloop a’
         instead of an instance of its parent type ‘Bloop a’
    • In the definition of data constructor ‘Blop’
         In the data instance declaration for ‘Bloop’
    |
 12 |   Blop :: Typeable a => Bloop a
    |   ^

Singletons TypeRepStar Sing Data Instance

2 Answers