Can't figure out `+` commutes in some contexts on GHC 8.6.3

[martijnbastiaan]

The following compiles on GHC 8.4.4, but fails on 8.6.3:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Test where

import Clash.Prelude

lastBits
  :: forall n a
   . ( BitPack a
     , n <= BitSize a
     , KnownNat (BitSize a)
     , KnownNat n
     )
  => a
  -> BitVector n
lastBits = leToPlus @n @(BitSize a) $ snd . split @_ @_ @n

where

leToPlus
  :: forall (k :: Nat) (n :: Nat) r
   . ( k <= n
     )
  => (forall m . (n ~ (k + m)) => r)
  -- ^ Context with the (k + m ~ n) constraint
  -> r
leToPlus r = r @(n - k)
{-# INLINE leToPlus #-}

Changing leToPlus to:

leToPlus
  :: forall (k :: Nat) (n :: Nat) r
   . ( k <= n
     )
  => (forall m . (n ~ (k + m), n ~ (m + k)) => r)
  -- ^ Context with the (k + m ~ n) constraint
  -> r
leToPlus r = r @(n - k)
{-# INLINE leToPlus #-}

..makes it compile just fine. The error reported by GHC is:

Test.hs:24:45: error:
    • Could not deduce: (w0 + n) ~ BitSize a
        arising from a use of ‘split’
      from the context: (BitPack a, n <= BitSize a, KnownNat (BitSize a),
                         KnownNat n)
        bound by the type signature for:
                   lastBits :: forall (n :: Nat) a.
                               (BitPack a, n <= BitSize a, KnownNat (BitSize a), KnownNat n) =>
                               a -> BitVector n
        at Test.hs:(15,1)-(23,16)
      or from: BitSize a ~ (n + m)
        bound by a type expected by the context:
                   forall (m :: Nat). (BitSize a ~ (n + m)) => a -> BitVector n
        at Test.hs:24:12-58
      The type variable ‘w0’ is ambiguous
    • In the second argument of ‘(.)’, namely ‘split @_ @_ @n’
      In the second argument of ‘($)’, namely ‘snd . split @_ @_ @n’
      In the expression: leToPlus @n @(BitSize a) $ snd . split @_ @_ @n
    • Relevant bindings include
        lastBits :: a -> BitVector n (bound at Test.hs:24:1)
   |
24 | lastBits = leToPlus @n @(BitSize a) $ snd . split @_ @_ @n
   |                                             ^^^^^^^^^^^^^^

For some reason, it sometimes can't figure out that n + m ~ m + n.

[martijnbastiaan]

@christiaanb I kindly request you not to solve this - unless it's blocking for you - until you're back in the office. Leon and I are hoping to get more insight into the plugins, so we'd like to look over your shoulder and ask questions along the way.

[martijnbastiaan]

Similar things happen with *. I'd expect:

proxyEq4
  :: forall m n
   . Proxy (8 * m * (2 ^ n))
  -> Proxy (m * 8 * (2 ^ n))
proxyEq4 = id

to work, but it doesn't. Seems like we should implement a "sort" for these equations.