<div dir="ltr">Thanks Richard! Matt pointed me in the same direction, and generating givens seems to work. Planning on releasing this solving tyfams stuff as a small library soon.<div><br></div><div>Cheers!</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Aug 5, 2019 at 10:36 AM Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Hi Sandy,<br>
<br>
I think the problem is that you're generating *Wanted* constraints. A Wanted is something that has not yet been proven, but which you would like to prove. If you have a metavariable a0, then created a Wanted `a0 ~ Bool` will work: you want to prove that, so GHC just unifies a0 := Bool. But anything more complicated than a unification variable will run into trouble, as GHC won't know how to prove it.<br>
<br>
Instead, create Givens. With these, you are providing the evidence to GHC that something holds -- exactly what you want here. Also, there shouldn't be a need to use unsafeTcPluginTcM or runTcSDeriveds here: just use newGiven (or newWanted) from the TcPluginM module, and return these constraints (perhaps wrapped in mkNonCanonical) from your plugin function.<br>
<br>
I hope this helps!<br>
Richard<br>
<br>
> On Aug 4, 2019, at 1:06 PM, Sandy Maguire <<a href="mailto:sandy@sandymaguire.me" target="_blank">sandy@sandymaguire.me</a>> wrote:<br>
> <br>
> Hi all,<br>
> <br>
> I'm attempting to use a plugin to solve a generic<br>
> <br>
> type family CmpType (a :: k) (b :: k) :: Ordering<br>
> <br>
> by doing some sort of arbitrary hashing on `a` and `b` and ensuring they're the same.<br>
> <br>
> In the past, I've been successful at getting GHC to unify things by emitting new wanted CNonCanonical cts. This sort of works:<br>
> <br>
> <br>
> mkWanted :: TyCon -> CompareType -> TcPluginM Ct<br>
> mkWanted cmpType cmp = do<br>
>   (ev, _) <- unsafeTcPluginTcM<br>
>              . runTcSDeriveds<br>
>              $ newWantedEq<br>
>                  (cmpTypeLoc cmp)<br>
>                  Nominal<br>
>                  (cmpTypeType cmp)<br>
>                  (doCompare cmp)<br>
>   pure $ CNonCanonical ev<br>
> <br>
> <br>
> Which is to say that this will compile:<br>
> <br>
> <br>
> foo :: Proxy 'EQ<br>
> foo = Proxy @(CmpType 2 2)<br>
> <br>
> <br>
> So far so good! However, this acts strangely. For example, if I ask for bar with the incorrect type:<br>
> <br>
> <br>
> bar :: Proxy 'GT<br>
> bar = Proxy @(CmpType 2 2)<br>
> <br>
> <br>
> I get the error:<br>
> <br>
>     • Couldn't match type ‘CmpType 2 2’ with ‘'GT’<br>
>       Expected type: Proxy 'GT<br>
>         Actual type: Proxy (CmpType 2 2)<br>
> <br>
> when I would expect<br>
> <br>
>     • Couldn't match type ‘'EQ’ with ‘'GT’<br>
> <br>
> <br>
> 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!<br>
> <br>
> <br>
> type family IsEQ (a :: Ordering) :: Bool where<br>
>   IsEQ 'EQ = 'True<br>
>   IsEQ _   = 'False<br>
> <br>
> zop :: Proxy 'True<br>
> zop = Proxy @(IsEQ (CmpType 2 2))<br>
> <br>
> <br>
>     • Couldn't match type ‘IsEQ (CmpType 2 2)’ with ‘'True’<br>
>       Expected type: Proxy 'True<br>
>         Actual type: Proxy (IsEQ (CmpType 2 2))<br>
> <br>
> <br>
> Any suggestions for what I might be doing wrong, and how to convince GHC to make `zop` work properly? Thanks!<br>
> <br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
<br>
</blockquote></div>