staroperator
Results
2
comments of
staroperator
> I did a bit of digging, the issue with the MWE is that `mkAppOptM'` in `RelKind.mkRel` can't infer the `M k V` instances while adding the trans instance. Changing...
> I feel the problem is that `mkAppOptM'` tries to synthesize the instances but we want to make them mvars as more as possible. A smaller MWE for your new...