"Could not deduce ... from the context ...", but if the context removed, deduced outright

[Mikolaj]

I don't know if this is related to #65. Tested with ghc-9.4.3 and ghc-9.0.2 and with newest plugin in both cases.

This snippet of larger code

build1VectorizeIndexVar
  :: forall m n r. (KnownNat m, KnownNat n, Show r, Numeric r)
  => Int -> AstVarName Int -> Ast (m + n) r -> AstIndex m r
  -> Ast (1 + n) r
build1VectorizeIndexVar k var v1 is =
  case v1 of
    AstBuildPairN{} -> let x = recAstBuildPairN2 @(1 + (m + n)) @((1 + m) + n) in undefined

recAstBuildPairN2 :: forall (p1m1n1 :: Nat) r1m1n1. (p1m1n1 ~ r1m1n1) => ()
recAstBuildPairN2 = ()

fails with

simplified/HordeAd/Core/TensorClass.hs:571:13: error:
    • Could not deduce ((1 + (m1 + n1)) ~ ((1 + m) + n))
        arising from a use of ‘recAstBuildPairN2’
      from the context: (m + n) ~ (m1 + n1)
        bound by a pattern with constructor:
                   AstBuildPairN :: forall (m :: GHC.Num.Natural.Natural)
                                           (n :: GHC.Num.Natural.Natural) b.
                                    ShapeInt (m + n) -> (AstVarList m, Ast n b) -> Ast (m + n) b,
                 in a case alternative
        at simplified/HordeAd/Core/TensorClass.hs:569:5-19
      NB: ‘+’ is a non-injective type family
    • In the expression:
        recAstBuildPairN2 @(1 + (m + n)) @((1 + m) + n)
      In an equation for ‘x’:
          x = recAstBuildPairN2 @(1 + (m + n)) @((1 + m) + n)
      In the expression:
        let x = recAstBuildPairN2 @(1 + (m + n)) @((1 + m) + n)
        in undefined
    • Relevant bindings include
        is :: AstIndex m r
          (bound at simplified/HordeAd/Core/TensorClass.hs:566:34)
        v1 :: Ast (m + n) r
          (bound at simplified/HordeAd/Core/TensorClass.hs:566:31)
        build1VectorizeIndexVar :: Int
                                   -> AstVarName Int
                                   -> Ast (m + n) r
                                   -> AstIndex m r
                                   -> Ast (1 + n) r
          (bound at simplified/HordeAd/Core/TensorClass.hs:566:1)
    |
571 |             recAstBuildPairN2 @(1 + (m + n)) @((1 + m) + n)
    |             ^^^^^^^^^^^^^^^^^

where the "context" is taken from

  AstBuildPairN :: forall m n r.
                   ShapeInt (m + n) -> (AstVarList m, Ast n r) -> Ast (m + n) r

However, if I remove the context by replacing the constructor in the offending line with _

    _ -> let x = recAstBuildPairN2 @(1 + (m + n)) @((1 + m) + n) in undefined

it goes through fine.