You can try yes, and find that the LHS is actually lazier than id, and instead a more precise RHS is \f x y -> f x y

{-# LANGUAGE TemplateHaskell #-}moduleUwhereimportTest.Inspectioncu,id1,id2::(a->b->c)->(a->b->c)cu=curry.uncurryid1f=fid2fxy=fxyinspect$'cu=/='id1inspect$'cu==-'id2

Definitional lawfulness: proof by inspection testing

https://blog.poisson.chat/posts/2020-08-08-definitional-lawfulness.html

@Lysxia interesting, i hadn't heard of inspection-testing before. Would it be able to prove that

`curry . uncurry = id`

for example?You can try yes, and find that the LHS is actually lazier than

`id`

, and instead a more precise RHS is`\f x y -> f x y`

wow, awesome

this is also used in polysemy to check that machinery is optimised away, for small examples - e.g. here

guess that's where a multi-module test is missing?