desugar-local-typeable.hs

-- Context: https://github.com/ghc-proposals/ghc-proposals/pull/273#issuecomment-530215302

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Typeable
import Data.Reflection
import Data.Proxy
import Debug.Trace (trace)

data W = forall a. (Typeable a, Ord a) => W a

wrapOrderedInt :: Bool -> Int -> W
wrapOrderedInt ascending n =
  reifyTypeable ascending $ \(Proxy :: Proxy ascending) -> W (V n :: V ascending)

newtype V s = V Int
    deriving Eq

instance Reifies ascending Bool => Ord (V ascending) where
  compare (V a) (V b)
    | reflect (Proxy :: Proxy ascending) = compare a b
    | otherwise = compare b a

broken :: W -> W -> Bool
broken (W (a :: a)) (W (b :: b)) =
  case eqT of
     -- BROKEN!  In the call below, GHC thinks the types are the same,
     -- but there are two different instances to pick from.
    Just (Refl :: a :~: b) -> a > b
    Nothing -> trace "Not typeable-ey equal" False

main = print (broken (wrapOrderedInt True 3) (wrapOrderedInt True 2))

Output:

Not typeable-ey equal                                                                                                                                       
False

Very interesting!