Singleton TypeRepStar Sing Data Instance

Question

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

The singleton library provides an instance Singfor view *in import Data.Singletons.TypeRepStar.

A data family is Singdefined as follows.

data family Sing (a :: k)

and the instance *is defined as ..

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

I am 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 get 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
    |   ^

Answer 1

, a Bloop (a :: *) a Typeable a => Bloop a a. ​​ , b:

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

* Data constructor `Blop' returns type `Bloop a'
    instead of an instance of its parent type `Bloop b'
* In the definition of data constructor `Blop'
  In the data instance declaration for `Bloop'

-fprint-explicit-kinds:

* Data constructor `Blop' returns type `Bloop k 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'

, a k, *. - a:

data instance Bloop (a :: *) where
      Blop :: Typeable (a :: *) => Bloop (a :: *)  -- Works now

, - PolyKinds. , a *, , , .

Answer 2

, PolyKinds . data family data instance . , PolyKinds , , . , KindSignatures.

Def.hs

{-# LANGUAGE PolyKinds, TypeFamilies #-}

module Def (Bloop) where

data family Bloop (a :: k)

Main.hs

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

module Main where

import Def
import Data.Typeable

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

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