{-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeOperators,
RankNTypes, MultiParamTypeClasses, ConstraintKinds #-}
module Typeable where
data (a :: k1) :~: (b :: k2) where
Refl :: forall k (a :: k). a :~: a
class EqT (t1 :: k1 -> *) (t2 :: k2 -> *) where
eqT :: t1 a -> t2 b -> Maybe (a :~: b)
type EqT' (t :: forall k. k -> *) = EqT t t
yields (with -ddump-tc)
type EqT' (t :: forall k. k -> *) =
EqT
(GHC.Prim.Any *)
(GHC.Prim.Any *)
(t (GHC.Prim.Any *))
(t (GHC.Prim.Any *))
yields (with
-ddump-tc
)That should be generalized.