search

isovector / type-sets

type level sets
BSD 3-Clause "New" or "Revised" License
67 stars 9 forks source link

Error claims the CmpType plugin is not enabled, when it is #9

Closed mgsloan closed 4 years ago

mgsloan commented 5 years ago

If I add the following to cmptype/test/ShouldTypecheck.hs

testWat :: Proxy (CmpType (Proxy "Hmm") (Proxy Int)) -> Proxy 'EQ
testWat = id

I get the error

    /home/mgsloan/oss/type-sets/cmptype/test/ShouldTypecheck.hs:16:11: error:                                 
        • The CmpType plugin isn't enabled.                                                                   
            Fix: enable '-fplugin=Type.Compare.Plugin'
        • In the expression: id                                                                               
          In an equation for ‘testWat’: testWat = id                                                          
       |
    16 | testWat = id

Without the addition of testWat, the test passes fine for me.

Doing some code sleuthing, it looks like this occurs when CmpTypeImpl is stuck. I'm not sure why this is. Before I looked at the plugin implementation, I figured that it is due to comparing types with polykinded arguments, where the kinds differ. However, after looking at the implementation I do not see how this would cause a problem.

isovector commented 5 years ago

CmpType only works for two things of the same kind. It probably makes sense to leave it stuck otherwise, but in that case it hits the default case in CmpType which gives a bad error message in this case. Nice catch. Any idea what the right solution is here?

mgsloan commented 5 years ago

No idea what the right solution is, without digging in to the problem further.

Proxy "Hmm" and Proxy Int have the same kind, *, so I expected it to work.

Is there an implementation reason for having CmpType require the types to be of the same kind? On one hand I see the analogy to Ord, and so the same kind restriction makes sense. On the other hand, comparing types with polykinded arguments, as in this example, seems to require that type comparison handles differing kinds.

isovector commented 5 years ago

Interesting. What happens if you comment out the error case from CmpType?

mgsloan commented 5 years ago

I think I figured it out! I added some tracing to the plugin, and it looks like splitTyConApp_maybe is failing on Symbol. The tests which involve symbols pass because they don't involve the plugin, instead using the CmpType a a = 'Eq and CmpType (a :: Symbol) b = CmpSymbol a b cases.

I have some other reasons to dig into this code, so I will go ahead and try to fix.