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