{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T16188 where

import Data.Kind (Type)
import Data.Type.Bool (type (&&))

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: forall k. k -> Type

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

(%&&) :: forall (x :: Bool) (y :: Bool).
         Sing x -> Sing y -> Sing (x && y)
SFalse %&& _ = SFalse
STrue  %&& a = a

data RegExp :: Type -> Type where
  App :: RegExp t -> RegExp t -> RegExp t

data instance Sing :: forall t. RegExp t -> Type where
  SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)

data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
type instance Apply ReNotEmptySym0 r = ReNotEmpty r

type family ReNotEmpty (r :: RegExp t) :: Bool where
  ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2

sReNotEmpty :: forall t (r :: RegExp t).
               Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2

blah :: forall (t :: Type) (re :: RegExp t).
        Sing re -> ()
blah (SApp sre1 sre2)
  = case (sReNotEmpty sre1, sReNotEmpty sre2) of
      (STrue, STrue) -> ()