Could not deduce: (n0 + 1) ~ m from the context: 1 <= m

[adamwalker]

The code below:

{- OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -}
import Clash.Prelude

f :: forall n m. m ~ (n + 1)
  => Vec m Bool
  -> Bool
f = undefined

g :: forall m. 1 <= m
  => Vec m Bool
  -> Bool
g = f

Fails with the error:

test.hs:12:5: error:
    • Could not deduce: (n0 + 1) ~ m arising from a use of ‘f’
      from the context: 1 <= m
        bound by the type signature for:
                   g :: forall (m :: Nat). (1 <= m) => Vec m Bool -> Bool
        at test.hs:(9,1)-(11,9)
      ‘m’ is a rigid type variable bound by
        the type signature for:
          g :: forall (m :: Nat). (1 <= m) => Vec m Bool -> Bool
        at test.hs:(9,1)-(11,9)
    • In the expression: f
      In an equation for ‘g’: g = f
    • Relevant bindings include
        g :: Vec m Bool -> Bool (bound at test.hs:12:1)

I think this should compile because if m is greater than or equal to one, then there exists a suitable n0. Is this something this plugin could infer?

[alex-mckenna]

Worth noting: you can use leToPlus for this if you're working on a Clash project

[adamwalker]

Ok. That looks very useful.

[christiaanb]

The implementation of the plugin cannot solve this. And there's no easy fix, see also: #33