"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.

[Mikolaj]

Or is this a known GHC bug that it doesn't try to solve things without context? But it seems this spurious context was also enough to solve the complications introduced by the context and type-check correctly.

[sheaf]

Here's a full test-case:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
import Data.Proxy
import GHC.TypeNats

module T71 where

data Ast (n :: Nat) where
  AstBuildPairN :: forall m n r. Proxy m -> Proxy n -> Ast (m + n)

build1VectorizeIndexVar
  :: forall m n
  .  (KnownNat m, KnownNat n)
  => Ast (m + n)
  -> Ast (1 + n)
build1VectorizeIndexVar v1 =
  case v1 of
    AstBuildPairN{} ->
      let x = recAstBuildPairN2 (Proxy @(1 + (m + n))) (Proxy @((1 + m) + n))
      in undefined

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

Here are the constraints the plugin sees:

[G] (m1 + n1) ~ (m2 + n2)
[W] (1 + m1) + n1 ~ 1 + (m2 + n2)

Alternative test:

t1 :: ( (1 + m1) + n1 ~ 1 + (m2 + n2) ) => Proxy '(m1, n1, m2, n2) -> ()
t1 _ = ()

t2 :: (m1 + n1 ~ m2 + n2) => Proxy '(m1, n1, m2, n2) -> ()
t2 px = t1 px

This is a simple oversight in the unifier.