Reflection of functions with class constraints may produce unsound results

[kleinreact]

As already discussed on the LH Slack, the following example is reported to be safe although it isn't (tested with 8c550df).

import Data.Proxy

class C a where
  classConst :: Proxy a -> Int

instance C Int  where classConst _ = 0
instance C Bool where classConst _ = 1

{-@ reflect classConstR @-}
classConstR :: forall a. C a => a -> Int
classConstR _ = classConst (Proxy :: Proxy a)

{-@ cEq :: a -> b -> { b : Bool | b == True } @-}
cEq :: forall a b. (C a, C b) => a -> b -> Bool
cEq a b = classConstR a == classConstR b

{-@ trueEqualsFive :: { b : Bool | b == True } @-}
trueEqualsFive :: Bool
trueEqualsFive = cEq True (5 :: Int)