1 <= Max (n + 1) 1 constraint isn't solved

[rowanG077]

While working on safe index pull request I ran into this problem.

Consider this code:

module Test where

import Data.Function (id)
import GHC.TypeLits (KnownNat, type (<=), type (+))
import GHC.TypeLits.Extra (Max)
import Data.Proxy (Proxy)

foo :: (KnownNat n, 1 <= Max (n + 1) 1) => Proxy n -> Proxy n
foo = id

bar :: KnownNat n => Proxy n -> Proxy n
bar = foo

The 1 <= Max (n + 1) 1 on foo should be solvable with this plugin. But an error occurs:

/home/rowan.goemans/engineering/clash-compiler/Test.hs:12:7: error:
    • Couldn't match type ‘1 GHC.TypeNats.<=? Max (n + 1) 1’
                     with ‘'GHC.Types.True’
        arising from a use of ‘foo’
    • In the expression: foo
      In an equation for ‘bar’: bar = foo
    • Relevant bindings include
        bar :: Proxy n -> Proxy n
          (bound at /home/rowan.goemans/engineering/clash-compiler/Test.hs:12:1)
   |
12 | bar = foo

The following works though:

baz :: (KnownNat n, 1 <= Max n 1) => Proxy n -> Proxy n
baz = id

bar :: KnownNat n => Proxy n -> Proxy n
bar = baz

This is an issue when using dependently typed folds where Max is used in things like the AResult and MResult types.

[alex-mckenna]

You gave n <= Max (n + 1) 1 as a constraint of foo in that example. Is this a typo?

[martijnbastiaan]

@alex-mckenna I think the title of the issue is the typo :)

We could hardcode it here:

https://github.com/clash-lang/ghc-typelits-extra/blob/63e0e884c2e81e423a4e39ab7cb4a003844bc3ea/src/GHC/TypeLits/Extra/Solver.hs#L159-L179

The proper solution would probably be to introduce some interval logic. Which sounds like fun to implement, but also easy to mess up :-)

[alex-mckenna]

@martijnbastiaan, it's mentioned again in the non-code line below though.

The 1 <= Max (n + 1) 1 on foo should be solvable with this plugin. But an error occurs:

[martijnbastiaan]

Aha, right! The error mentions Couldn't match type ‘n GHC.TypeNats.<=? Max (n + 1) 1’ again, so let's wait for @rowanG077 ! :-)

[rowanG077]

Ah indeed this is a typo... I guess when reducing my example to bare minimum I made this somehow. But both 1 <= Max (n + 1) 1 and n <= Max (n + 1) 1 should be solvable. But this issue is about the former case.

[christiaanb]

Actually, what needs to happen is that we should do a partial solve. Looking at the type-checker trace, I see that ghc-typelits-extra reduced the Max already, and it's now trying to solve: 1 <= n + 1 (or n <= n + 1): which it can't. However, ghc-typelits-natnormalise can!

We should detect that we did make the problem "smaller", and tag the wanted as solved, but emit a new wanted for the "smaller" problem. We have to be careful not to throw the type-checker into an infinite loop though.

[rowanG077]

A partial solve isn't necessary for the "simpler" case I think. 1 <= Max (n + 1) 1 should be solvable outright by the plugin. In fact this plugin already has machinery builtin that recognizes the general case of p <= Max n p:

https://github.com/clash-lang/ghc-typelits-extra/blob/63e0e884c2e81e423a4e39ab7cb4a003844bc3ea/src/GHC/TypeLits/Extra/Solver.hs#L156-L157

But the max constraint is simplified away before that point in the mergeMax function.

https://github.com/clash-lang/ghc-typelits-extra/blob/487ea1c54c75e49ae56f1f3ced5aabfb1337ac1e/src/GHC/TypeLits/Extra/Solver/Operations.hs#L113-L129

I guess this is done to be able to solve constraints like Max (n + 1) 1 ~ 1 + n?

The more complex case of n <= Max (n + 1) 1 would need a partial solve. But I would say this is out of scope for this issue.

[christiaanb]

Fixed with the release of version 0.4.1: https://hackage.haskell.org/package/ghc-typelits-extra-0.4.1