Solving stuck type families with a TC plugin

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Solving stuck type families with a TC plugin

Sandy Maguire
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Solving stuck type families with a TC plugin

Richard Eisenberg-5
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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs