Strange.hs

{-# LANGUAGE RankNTypes, GADTs, EmptyCase, LambdaCase #-}

module Strange where

-- import Data.Char (ord)

-- Tested with GHC 8.4.3, 8.6.3.

-- I discovered this behaviour while writing church-style ADTs, and thought I'd
-- see if I could write GADTs the same way.

-- Here a GADT is declared in terms of its destructor rather than constructors.
newtype Gadt a = Gadt {
  gadt :: forall c. (a ~ Int => a   -> c) -> (a ~ Char => a    -> c) -> c
--gadt :: forall c. (a ~ Int => Int -> c) -> (a ~ Char => Char -> c) -> c
--gadt :: forall c. (a -> (a ~ Int => c)) -> (a  -> (a ~ Char => c)) -> c
}

-- The constructors (not needed for minimal reproduction):
-- intCon :: Int  -> Gadt Int
-- chaCon :: Char -> Gadt Char
-- intCon = \i -> Gadt (\l _ -> l i)
-- chaCon = \c -> Gadt (\_ r -> r c)


{- It's equivalent to declare the GADT in terms of these constructors, then
-- declare the @gadt@ destructor below. The resulting behaviour is the same.
data Gadt a where
  IntCon :: Int  -> Gadt Int
  ChaCon :: Char -> Gadt Char

gadt   :: Gadt a -> (a ~ Int => a   -> c) -> (a ~ Char => a    -> c) -> c
--gadt :: Gadt a -> (a ~ Int => Int -> c) -> (a ~ Char => Char -> c) -> c
--gadt :: Gadt a -> (a -> (a ~ Int => c)) -> (a  -> (a ~ Char => c)) -> c
gadt = \case
  IntCon i -> \f _ -> f i
  ChaCon c -> \_ g -> g c
-}

-- This usage plays out as expected (not needed for minimal reproduction).
-- gadtToInt :: Gadt a -> Int
-- gadtToInt = \g -> (gadt g)
--   (\i -> i)     -- In this case GHC correctly determines @(i :: a) :: Int@.
--   (\c -> ord c) -- And here GHC also correctly sees that @(c :: a) :: Char@.

-- This usage does not.
fromIntCon :: Gadt Int -> Int
fromIntCon = \g -> (gadt g)
  (\i -> i)
  (\c -> c)  -- With the first and third types for @gadt@, GHC allows us to use
             -- @c :: a@ as an @Int@ even though we require @a ~ Char@.
             -- Using the second type, the error is caught.
--(\case {}) -- Either way, empty case is not accepted as exhaustive.