{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

import Data.Kind
import Unsafe.Coerce

type family Sing :: k -> Type

class SingI a where
  sing :: Sing a

data SingInstance :: forall k. k -> Type where
  SingInstance :: SingI a => SingInstance a

newtype DI (a :: k) = Don'tInstantiate (SingI a => SingInstance a)

singInstance :: forall k (a :: k). Sing a -> SingInstance a
singInstance s = with_sing_i SingInstance
  where
    with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
    with_sing_i si = unsafeCoerce (Don'tInstantiate si) s

{-# COMPLETE Sing #-}
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
pattern Sing <- (singInstance -> SingInstance)
  where Sing = sing

-----

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True
type instance Sing = SBool

f :: SBool b -> ()
f Sing = ()

g :: Sing (b :: Bool) -> ()
g Sing = ()