Can not infer Max 1 n ~ n when given 1 <= n

[lmbollen]

Reproducer:

{-# LANGUAGE DataKinds #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}

import GHC.TypeLits
import GHC.TypeLits.Extra
import Data.Proxy

data QQ x where
    QQ :: 1 <= x => Proxy x -> QQ x

f :: QQ x -> Proxy (Max 1 x)
f (QQ z) = z

Produces:

[1 of 2] Compiling Main             ( Test.hs, interpreted )
Test.hs:12:12: error: [GHC-25897]
    • Could not deduce 'Max 1 x ~ x'
      from the context: 1 <= x
        bound by a pattern with constructor:
                   QQ :: forall (x :: Natural). (1 <= x) => Proxy x -> QQ x,
                 in an equation for 'f'
        at Test.hs:12:4-7
      Expected: Proxy (Max 1 x)
        Actual: Proxy x
      'x' is a rigid type variable bound by
        the type signature for:
          f :: forall (x :: Natural). QQ x -> Proxy (Max 1 x)
        at Test.hs:11:1-28
    • In the expression: z
      In an equation for 'f': f (QQ z) = z
    • Relevant bindings include
        z :: Proxy x (bound at Test.hs:12:7)
        f :: QQ x -> Proxy (Max 1 x) (bound at Test.hs:12:1)
   |
12 | f (QQ z) = z
   |            ^

[lmbollen]

Ideally after solving this we'd change https://github.com/clash-lang/clash-compiler/blob/master/clash-prelude/src/Clash/Signal/Internal.hs#L351
to return Max 1 period or similar solution to make sure that DomainPeriod dom is always at least 1 on type level.