G X XX

gadt-X.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}

import Data.Kind

data I a
data X a

data XX

type F :: (Type -> Type) -> Type -> Type
type family F f a where
  F X a = XX
  F I a = a
  F f a = f a

data G f a where
  GU :: G f (F f ())

gx :: forall a. G X a -> G X XX
gx = \case
  GU -> GU

{-

-- Does not typecheck:
gx2 :: forall a. G X a -> a
gx2 = \case
  GU -> ()

-}

gi :: forall a. G I a -> a
gi = \case
  GU -> ()