I think constraint kinds and quantified constraints would be more likely to be accepted than type families and GADTs. I can’t think of any features they conflict with, and they would be especially useful in
purescript-variant (so that
VariantF could internalize evidence other than
Traversable). It would also allow
Functor to imply
forall a b. Coercible a b => Coercible (f a) (f b) (essentially representational role). (Some resources on that: Roles for type families (#8177) · Issues · Glasgow Haskell Compiler / GHC · GitLab and Oleg's gists - Should fmap coerce = coerce hold?)
(Right now we do have a kind called
Constraint, but constraints cannot be used outside of particular syntactic contexts. Constraint kinds would mean that constraints can be parameters to datatypes, like
Dict :: Constraint -> Type would reify the data/evidence for an arbitrary constraint.)
I personally don’t see so much value in type applications, but I don’t have any strong objection to adding them.
Of course it would be good for other core team members to weight in before you start anything, particularly @natefaubion who added polykinds.
These are just some thoughts I have. I’m not sure what the requirements are for a master’s thesis, so you would have to work with your advisor to determine what’s appropriate and what’s feasible.
EDIT: Some more links on roles and coercible in Haskell: roles2 · Wiki · Glasgow Haskell Compiler / GHC · GitLab and How QuantifiedConstraints can let us put join back in Monad - Ryan Scott