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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190804/c1b0b089/attachment.html>