Attempting to recreate https://twitter.com/CodaFi_/status/905583919550132226 in Haskell without unsafeCoerce

NotQuiteIdentity.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Typeable
import Control.Monad
import Control.Exception
import Prelude hiding (id)

-- Is it possible to do something like this without Typeable?
id :: forall a. Typeable a => a -> a
id x =
  case eqT of
    Just (Refl :: a :~: Int) -> 5
    Nothing -> x

expect :: Bool -> IO ()
expect cond = void (evaluate (assert cond ()))

main :: IO ()
main = do
  expect $ id True == True
  expect $ id @Int 1 == 5