Solving stuck type families with a TC plugin

[Sandy Maguire]

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.

Cheers!

On Mon, Aug 5, 2019 at 10:36 AM Richard Eisenberg <rae at richarde.dev> wrote:

> Hi Sandy,
>
> 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.
>
> 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.
>
> I hope this helps!
> Richard
>
> > On Aug 4, 2019, at 1:06 PM, Sandy Maguire <sandy at sandymaguire.me> wrote:
> >
> > 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!
> >
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190805/45ca58e8/attachment.html>