Hi, not sure whether this has been addressed before. Basically the goal is to have a standardised way of witnessing lifted types (=simulating pattern matching on type indices). A particular problem this would be useful for: Given a standard natural-indexed vector (Vec n) provide an Applicative instance for it with n left polymorphic. The issue is that we don't have a way of pattern matching on n, therefore we cannot implement pure/<*>. The way I addressed situations like this before was to have two Applicative instances, one for Vec Zero and one for Vec (Succ n), however I think there is a way to decouple this way of "pattern matching on types" by introducing a GADT: data WNat n where WZero :: WNat Zero WSucc :: WNat n -> WNat (Succ n) and a class class WNatClass n where witness :: WNat n instance WNatClass Zero where witness = WZero instance (WNatClass n) => WNatClass (Succ n) where witness = WSucc witness Now whenever we need to pattern match on a natural index we can just put a WNatClass restriction on it and pattern match on the automatically constructed witness. For the Vec example: instance (WNatClass n) => Applicative (Vec n) where pure = pure' witness where pure' :: WNat n -> a -> Vec n a pure' WZero _ = VecNil pure' (WSucc w) a = a ::: pure' w a (<*>) = app' witness where app' :: WNat n -> Vec n (a -> b) -> Vec n a -> Vec n b app' WZero _ _ = VecNil app' (WSucc w) (f ::: fs) (a ::: as) = f a ::: app' w fs as We can also generalise this concept to any index type with PolyKinds, although I'm not 100% sure why it works in general: class Construct (a :: k) where data Wit a :: * class (Construct a) => Witness a where witness :: Wit a The idea is that each instance of Construct will leave the type 'a' polymorphic and will only bind the kind 'k' and provide an indexed witness: instance Construct (n :: Nat) where data Wit n where WZero :: Wit Zero WSucc :: Wit n -> Wit (Succ n) and the Witness instances will be the same as with WNatClass. We need two classes because one will define the witness type, the other will do the "pattern matching". The part I don't understand is that together with the (n :: Nat) instance we can also have instance Construct (a :: SomeOtherType) where ... without triggering any 'overlapping' diagnostic, even though both instances are "fully polymorphic". I am assuming this is because internally the compiler adds a kind parameter to the class that disambiguates the instances? If so then I think this is a nice uniform way of handling lifted type witnesses. (The instances can be generated automatically too). What do you think? Is there a better way of doing this? Is the decoupling even worth the trouble? Is the performance hit big compared to the explicit instance splitting?