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 <r...@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 <sa...@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@haskell.org > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
