Misleading `solverWanteds: too many iterations` error message

[kleinreact]

The following reproducer

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveAnyClass #-}

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

module Test where

import Clash.Prelude

type family Go xs where
  Go (_ : xr) = Go xr
  Go '[]      = 0

type Elements a = 1 + Go a

data RIndex a = RIndex (Index (Elements a))
  deriving (Generic)

deriving instance
  ( KnownNat (Elements a)
  ) =>
  BitPack (RIndex a)

causes some

    solveWanteds: too many iterations (limit = 4)
      Unsolved: WC {wc_simple =
                      [W] $dKnownNat_ajqO {0}:: KnownNat (Go a1) (CNonCanonical)}
      Simples: {[W] $dKnownNat_ajoy {0}:: KnownNat
                                            (BitSize (RIndex a1)) (CNonCanonical)}
    Suggested fix:
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
  |
1 | {-# LANGUAGE DataKinds #-}
  | ^

error, which is misleading in order to figure out the actual problem. Note that the iteration limit is not the problem here. Disabling just the KnownNat plugin reveals

Test.hs:22:1: error: [GHC-39999]
    • Could not deduce ‘KnownNat (CLog 2 (1 + Go a2))’
        arising from the superclasses of an instance declaration
      from the context: KnownNat (Elements a2)
        bound by the instance declaration at Test.hs:(22,1)-(26,20)
      Possible fix:
        If the constraint looks soluble from a superclass of the instance context,
        read 'Undecidable instances and loopy superclasses' in the user manual
    • In the instance declaration for ‘BitPack (RIndex a1)’
   |
22 | deriving instance
   | ^^^^^^^^^^^^^^^^^...

Test.hs:22:1: error: [GHC-39999]
    • Could not deduce ‘KnownNat (Go a2)’
        arising from a use of ‘Clash.Class.BitPack.Internal.$dmpack’
      from the context: KnownNat (Elements a2)
        bound by the instance declaration at Test.hs:(22,1)-(26,20)
    • In the expression:
        Clash.Class.BitPack.Internal.$dmpack @(RIndex a1)
      In an equation for ‘pack’:
          pack = Clash.Class.BitPack.Internal.$dmpack @(RIndex a1)
      When typechecking the code for ‘pack’
        in a derived instance for ‘BitPack (RIndex a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘BitPack (RIndex a1)’
   |
22 | deriving instance
   | ^^^^^^^^^^^^^^^^^...

Test.hs:22:1: error: [GHC-39999]
    • Could not deduce ‘KnownNat (Go a2)’
        arising from a use of ‘Clash.Class.BitPack.Internal.$dmunpack’
      from the context: KnownNat (Elements a2)
        bound by the instance declaration at Test.hs:(22,1)-(26,20)
    • In the expression:
        Clash.Class.BitPack.Internal.$dmunpack @(RIndex a1)
      In an equation for ‘unpack’:
          unpack = Clash.Class.BitPack.Internal.$dmunpack @(RIndex a1)
      When typechecking the code for ‘unpack’
        in a derived instance for ‘BitPack (RIndex a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘BitPack (RIndex a1)’
   |
22 | deriving instance
   | ^^^^^^^^^^^^^^^^^...

which makes it immediately clear that there is just a KnownNat (Go a) constraint missing, e.g., with the KnownNat plugin enabled and

deriving instance
  ( KnownNat (Elements a)
  , KnownNat (Go a)
  ) =>
  BitPack (RIndex a)

it typechecks.

It would be much more useful if the plugins still could print the original type errors in that case.

[christiaanb]

Do you get the same error when you increase the number of solver iterations to e.g. 50?

Because the plugins don’t throw the solver limit error, that’s a GHC thing.

[kleinreact]

You can increase it to any number or set it 0. It won't make any difference (unless that it won't return when setting no limit).

[christiaanb]

Right, so the actual bug/problem is that this code throws GHC + plugins into an infinite solver loop.

[christiaanb]

The original request, to report the outstanding errors when the solver iteration limit is hit, is more something GHC should solve; not individual plugins.

[rowanG077]

A simpler reproducer:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveAnyClass #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}

module Test where

import Data.Proxy
import GHC.Num
import GHC.TypeLits
import Data.Kind

type family Stuck (a :: Type) :: Nat

stuck :: forall a . (KnownNat (1 + Stuck a)) => Proxy a -> Integer
stuck _ = natVal (Proxy @(Stuck a))

It's a nasty interaction between GHC.TypeLits.Normalise and GHC.TypeLits.KnownNat plugins.

1. natVal (Proxy @(Stuck a)) leads to an emission of KnownNat (Stuck a) wanted.

2. GHC.TypeLits.KnownNat solves KnownNat (Stuck a) by using the KnownNat (1 + Stuck a) given and using subtraction. This makes GHC.TypeLits.KnownNat emit a new wanted 1 <= (1 + Stuck a)

3. GHC.TypeLits.Normalise solves the 1 <= (1 + Stuck a) wanted but emits a new wanted KnownNat (Stuck a). The logic is essentially: 1 + Stuck a is only natural if Stuck a is natural so emit a KnownNat (Stuck a) so later on this is made sure to be the case.

4. GHC.TypeLits.KnownNat goes to work again trying to solve KnownNat (Stuck a) and the loop is closed.

I see two ways forward:

1. Revise the check in 3. KnownNat here seems like a workaround as it gives a much stronger guarantee then is a natural, namely that there even is a runtime representation available. But this was explicitly implemented in clash-lang/ghc-typelits-natnormalise@ede7626 by @christiaanb. Perhaps there is a better way.

2. Maintain a set of prior emitted KnownNat constraints in the GHC.TypeLits.Normalise solver so it can ensure it doesn't emit the same KnownNat x wanted multiple times..

[rowanG077]

Implemented solution proposal 2 in clash-lang/ghc-typelits-natnormalise#122 and it works with the reproducer. clash-protocols (and thus clash-prelude) compile fine with the change.

Perhaps still proposal 1 is better. But as it's uncertain to me I went with 2.

[christiaanb]

We could implement proposal 1 on GHC 9.4 by emitting a 0 <= X constraint instead. That’s because the TypeError mechanism will properly in combination with stuck type family application such as Div 3 0; i.e. you will get a proper “Div 3 0 not greater than 0” error.

[rowanG077]

If we emit 0 <= x then the reproducer will not work as it now need a 0 <= Stuck a constraint. I expect many regression if we change that. A solution could be to allow a given KnownNat x to solve a 0 <= x.

I will investigate what kind of fallout there is if this is changed.

Is there anything wrong with stop emitting duplicate KnownNat wanteds by maintaining the set?

edit: At least a naive implementation also causes a loop. Since the new emitted wanted 0 <= Stuck a is again picked up by natnormalise which generates a new 0 <= Stuck a.

edit 2: I solved the loop, but indeed the reproducer still doesn't work due to requiring 0 <= Stuck a. So I greatly prefer a solution that keeps the KnownNat pipeline.

[christiaanb]

Ah, it’s too bad the 0 <= X trick induces a self-loop with natnormalise itself.

The reason I’m worried about keeping a simple set is that:

1. variables are only unique within their scope, and
2. Plugin state is module-wide

So you might have two distinct case alternative (GADT pattern match) that bring a type variable in scope which are themselves not distinct. So with a simple set could end up in a situation where you emit a wanted constraint in one branch A, but then not emit it in branch B, even though it would be required for soundness.

Perhaps we need to maintain a set of

1. Location (perhaps https://hackage-content.haskell.org/package/ghc-9.14.1/docs/GHC-Tc-Types-CtLoc.html#v:getCtLocEnvLoc) of the constraint that is requiring us to generate that KnownNat constraint
2. Whether we already emitted a KnownNat constraint for that location.
   Thar way we can distinguish scopes.