The PR adds the CLogWZ type family to the solver, which allows for a CLog definition with a well defined output for the case of the second non-base argument being zero. In this case the third argument is returned instead. The type family can be useful in cases, where the zero case needs to defined, as for example in the Index 0 case within clash-prelude (cf. clash-compiler PR #2784).
Reviewers Note
The currently used naming scheme might still be a bit adhoc, but I couldn't figure out any more elegant solution yet. One option might be to add total versions for all non-total type families of ghc-typelits-extra with extra parameters defining the return value in the undefined cases. In terms of naming we then just could add Total as a prefix / suffix to these versions, e.g., TotalDiv or DivTotal. In the particular case of CLog there are many undefined cases, however, which makes me unsure of how practical this approach would be.
TODOs
[ ] This still is a draft PR, as I'd like to see this fact being covered here within the plugin as well.
[ ] Add the new type families to the readme and check the generated documentation.
The PR adds the
CLogWZtype family to the solver, which allows for aCLogdefinition with a well defined output for the case of the second non-base argument being zero. In this case the third argument is returned instead. The type family can be useful in cases, where the zero case needs to defined, as for example in theIndex 0case withinclash-prelude(cf. clash-compiler PR #2784).Reviewers Note
The currently used naming scheme might still be a bit adhoc, but I couldn't figure out any more elegant solution yet. One option might be to add total versions for all non-total type families of
ghc-typelits-extrawith extra parameters defining the return value in the undefined cases. In terms of naming we then just could addTotalas a prefix / suffix to these versions, e.g.,TotalDivorDivTotal. In the particular case ofCLogthere are many undefined cases, however, which makes me unsure of how practical this approach would be.TODOs