Hi! Some code of mine doesn’t pass the type checker, and I have no clue to what problem GHC’s error message is meant to point. Consider the following reduced variant of my code: {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE PartialTypeSignatures #-} data Dict c = c => Dict class T a ~ a => C a where type T a :: * op :: C a => a -> a op = undefined fromDict :: Dict (C a) -> _ fromDict (Dict @(C a)) = op @a Feeding this to GHC 9.12.2 results in GHC telling me that it “could not deduce `w ~ (a -> a)` from the context `C a`” bound by the argument pattern of `fromDict`, where “`w` is a rigid type variable bound by the inferred type of `fromDict`”, which is “`Dict (C a) -> w`” and that this all happened “in the expression `op @a`”. After removing the constraint `T a ~ a` from the class declaration, the code is accepted. At the moment, I don’t understand at all why the presence of an equality constraint should make this program type-incorrect, and I also don’t understand the error message, in particular the role of that rigid type variable `w`. Could someone perhaps enlighten me? 🙂 All the best, Wolfgang