Add `Max` types to `PeriodToHz`

[lmbollen]

This satisfies the 1 <= divisor constraint imposed by DivRU. Furthermore implies that all domains have a non-zero, strictly positive frequency.

Did not update the changelog because the types dont exist in any release

[rowanG077]

Personally I think it's nicer to add a 1 <= DomainPeriod dom constraint to KnownDomain. This seems like a bit of a patchwork over something that should always be given.

Edit: The outer Max is unfortunate and can't be removed. Unless we make the ghc-typelits-extra smarter.

[rowanG077]

I think you can basically copy pasta this: https://github.com/clash-lang/clash-compiler/commit/8702badb80b2c3f3e7a6c7d006d04d511bdc8e8c . If you do end up pursuing that direction.

Also bail out when someone passes in a period that is zero in createDomain.

[DigitalBrains1]

I already tried to add 1 <= DomainPeriod dom to KnownDomain, but it starts with

src/Clash/Signal/Internal.hs:512:1: error:
    • Potential superclass cycle for ‘KnownDomain’
        one of whose superclass constraints is headed by a type family:
          ‘1 <= DomainPeriod dom’
      Use UndecidableSuperClasses to accept this
    • In the class declaration for ‘KnownDomain’
    |
512 | class (KnownSymbol dom, KnownNat (DomainPeriod dom), 1 <= DomainPeriod dom) => KnownDomain (dom :: Domain) where

and ends with failures in other source files if I follow the directions in the error messages.

I am all in favour of adding this, either in DomainConfiguration or in KnownDomain, but I couldn't get it to work.

[christiaanb]

What DivRU are you referring to @lmbollen? The code that you changed only has an application of the Div type family. I find it hard to justify this change with the context that's currently been provided.

I thought it would be helpful if PeriodToHz would not reduce to a number when the period is zero. If you want a more explicit error message than perhaps:

type PeriodToHz (period :: Nat) = If (1 <=? n) ((Seconds 1) `Div` period) (TypeError (Text "Period cannot be negative"))

would be better?

[rowanG077]

I already tried to add 1 <= DomainPeriod dom to KnownDomain, but it starts with

src/Clash/Signal/Internal.hs:512:1: error:
    • Potential superclass cycle for ‘KnownDomain’
        one of whose superclass constraints is headed by a type family:
          ‘1 <= DomainPeriod dom’
      Use UndecidableSuperClasses to accept this
    • In the class declaration for ‘KnownDomain’
    |
512 | class (KnownSymbol dom, KnownNat (DomainPeriod dom), 1 <= DomainPeriod dom) => KnownDomain (dom :: Domain) where

and ends with failures in other source files if I follow the directions in the error messages.

I am all in favour of adding this, either in DomainConfiguration or in KnownDomain, but I couldn't get it to work.

Yeah just tried it. And I believe that is a GHC bug, or my brain is too stupid to figure out. Doesn't seem easy to work around. So I guess this solution is out.

[DigitalBrains1]

This PR is not the change I requested. I asked to change PeriodToCycles (and implied that ClockDivider can inherit these changes).

See there for why, in the case of PeriodToCycles, it is more pleasant to deal with the 0 case instead of erroring for it... it leads to added constraints at call sites.

[rowanG077]

I made an upstream issue, link for traceability: https://gitlab.haskell.org/ghc/ghc/-/issues/25022

[christiaanb]

It's probably to do with the fact that 1 <= y is not injective: there are my y that fit the bill.

[christiaanb]

But this PR is for PeriodToHz, not the PeriodToCycles you mentioned in https://github.com/clash-lang/clash-compiler/pull/2734#issuecomment-2182893091

[christiaanb]

I think a better way to get what you want in https://github.com/clash-lang/clash-compiler/pull/2734#issuecomment-2182893091 is this:

--- a/clash-prelude/src/Clash/Signal/Internal.hs
+++ b/clash-prelude/src/Clash/Signal/Internal.hs
@@ -488,6 +488,7 @@ type ClockDivider (dom :: Domain) (period :: Nat) = PeriodToCycles dom period
 -- | Singleton version of 'DomainConfiguration'
 data SDomainConfiguration (dom :: Domain) (conf :: DomainConfiguration) where
   SDomainConfiguration ::
+    1 <= period =>
     { sName :: SSymbol dom
       -- ^ Domain name
     , sPeriod :: SNat period

then the following typechecks:

import Clash.Prelude
import Data.Proxy

f ::
  forall dom .
  KnownDomain dom =>
  Proxy dom ->
  SNat (PeriodToCycles dom (Milliseconds 1))
f Proxy = case knownDomain @dom of
    SDomainConfiguration {} -> SNat

[christiaanb]

I've opened two alternative PRs:

• Constraint on SDomainConfiguration: https://github.com/clash-lang/clash-compiler/pull/2740
• Constraint on KnownDomain: https://github.com/clash-lang/clash-compiler/pull/2741

Of the two I prefer the one with the constraint on SDomainConfiguation as it is very much the least invasive.

[rowanG077]

There is a third solution. Make DomainPeriod always return Max 1 _ could be combined with solution #1. I prefer the first alternative.