Good day, I am currently developing a typechecker plugin for GHC for realizing an idea regarding types based on regular expressions to describe the contents of a string. This is done using type-level literals to denote a particular regex. Additionally there are additional constraints for working with such types. One of those constraints is called Intersectable and denotes whether an intersection between two regexes would be possible in the sense that there is some common alphabet between them. Furthermore there is a type-level function that calculates the actual intersection between two regex types and returns the resulting regex type: type family Intersectable (a :: Symbol) (b :: Symbol) :: Constraint type family Intersection (a :: Symbol) (b :: Symbol) :: Symbol Now i've created a typechecker plugin that resolves such constraints by using a finite-automata representation of the regexes to do the actual work. While my plugin is already able to proof progams where regexes are fully applied, i.e. they can reduce terms to a single regex and then verify the constraints accordingly or reject them, it fails to type "intermediate" functions. As a small example assume the following program: checkFour :: Intersectable a "[0-4]" => RgxString a -> RgxString (Intersection a "[0-4]") checkFour a = undefined checkEight :: Intersectable a "[0-8]" => RgxString a -> RgxString (Intersection a "[0-8]") checkEight a = undefined test = checkFour . checkEight  -- this fails to type correctly test2 = checkFour $ checkEight $ (RgxString :: RegexString ".*") -- this works fine The constraint solver wants me to proof the following constraints for test: tcPluginSolve given   = [] derived = [] wanted  = [ [WD] irred_a2GV {0}:: Intersectable     (Intersection a0 "[0-8]")     "[0-4]" (CNonCanonical), [WD] irred_a2GY {0}:: Intersectable a0 "[0-8]" (CNonCanonical)] My plugin reduces the first constraint to Intersectable a0 [0-4] as regex intersection is commutative so i can intersect [0-8] with [0-4] first. But i haven't found out yet how i would tell the compiler to put this reduced constraint to the type signature instead of the current one where the constraint got dropped at all instead of at least remain unnormalized, and the return type remains unnormalized as well: RgxString a -> RgxString (Intersection (Intersection a "[0-8]") "[0-4]") I'd need to tell the typechecker somehow that (Intersection (Intersection a "[0-8]") "[0-4]") is equal to Intersection a "[0-4]" so it substitutes it accordingly. My idea is that i have to generate given type and function equality constraints during the  typechecking telling it that those representations are equal, but i am really not sure what kind of constraints i need. CTyEqCan for instance seems to require a TyVar on one side while i though i could generate something like Intersection (Intersection a "[0-8]") "[0-4]" ~ Intersection a "[0-4]" I have already tried a lot but there is little documentation on the whole constraint solving process and i am slowly getting stuck. Thanks for helping!