Stuck.hs

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}

module Stuck where

data Tag = Tag

type family Fam :: k -> Tag -> k

type family IsTagged (a :: k) :: Bool where
  IsTagged (a 'Tag) = 'True
  IsTagged (a _) = 'False

-- These two cases work perfectly:
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- >>> :kind! IsTagged (Maybe Int)
-- IsTagged (Maybe Int) :: Bool
-- = 'False
--
-- >>> :kind! IsTagged (Fam Int 'Tag)
-- IsTagged (Fam Int 'Tag) :: Bool
-- = 'True

-- But this one doesn't reduce... why?
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- >>> :kind! IsTagged (Fam Maybe 'Tag Int)
-- IsTagged (Fam Maybe 'Tag Int) :: Bool
-- = IsTagged (Fam Maybe 'Tag Int)