{-# LANGUAGE PolyKinds, MultiParamTypeClasses, GADTs, ScopedTypeVariables,
TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
module Super where
import Data.Proxy
import GHC.Prim
class (a ~ b) => C a b
data SameKind :: k -> k -> * where
SK :: SameKind a b
bar :: forall (a :: *) (b :: *). C a b => Proxy a -> Proxy b -> ()
bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y)
The following should compile, but doesn't.