Hi all, I'm attempting to use a plugin to solve a generic type family CmpType (a :: k) (b :: k) :: Ordering by doing some sort of arbitrary hashing on `a` and `b` and ensuring they're the same. In the past, I've been successful at getting GHC to unify things by emitting new wanted CNonCanonical cts. This sort of works: mkWanted :: TyCon -> CompareType -> TcPluginM Ct mkWanted cmpType cmp = do (ev, _) <- unsafeTcPluginTcM . runTcSDeriveds $ newWantedEq (cmpTypeLoc cmp) Nominal (cmpTypeType cmp) (doCompare cmp) pure $ CNonCanonical ev Which is to say that this will compile: foo :: Proxy 'EQ foo = Proxy @(CmpType 2 2) So far so good! However, this acts strangely. For example, if I ask for bar with the incorrect type: bar :: Proxy 'GT bar = Proxy @(CmpType 2 2) I get the error: • Couldn't match type ‘CmpType 2 2’ with ‘'GT’ Expected type: Proxy 'GT Actual type: Proxy (CmpType 2 2) when I would expect • Couldn't match type ‘'EQ’ with ‘'GT’ This is more than just an issue with the error messages. A type family that is stuck on the result of CmpType, even after I've solved CmpType via the above! type family IsEQ (a :: Ordering) :: Bool where IsEQ 'EQ = 'True IsEQ _ = 'False zop :: Proxy 'True zop = Proxy @(IsEQ (CmpType 2 2)) • Couldn't match type ‘IsEQ (CmpType 2 2)’ with ‘'True’ Expected type: Proxy 'True Actual type: Proxy (IsEQ (CmpType 2 2)) Any suggestions for what I might be doing wrong, and how to convince GHC to make `zop` work properly? Thanks!