Infinite loop in the solver

[basile-henry]

I expected the following code to complain about a missing KnownNat constraint for halfBatchSize (the one commented out). Instead it seems to have thrown the plugin into an infinite loop (I can keep on increasing the number of iterations with any effect).

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}

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

module Test where

import Clash.Prelude

test
  :: ( KnownNat batchSize
     -- , KnownNat halfBatchSize
     , (halfBatchSize * 2) ~ batchSize
     )
   => proxy halfBatchSize
   -> Integer
test = natVal

Test.hs:1:1: error:
    solveSimpleWanteds: too many iterations (limit = 4)
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
      Simples = {[WD] $dKnownNat_a6Pj {0}:: KnownNat n0 (CNonCanonical)}
      WC = WC {wc_simple =
                 [WD] $dKnownNat_a6UM {0}:: KnownNat
                                              (halfBatchSize * 2) (CNonCanonical)
                 [WD] $dKnownNat_a6UN {0}:: KnownNat halfBatchSize (CNonCanonical)
                 [WD] $d~_a6UO {0}:: halfBatchSize
                                     <= (halfBatchSize * 2) (CNonCanonical)
                 [WD] hole{co_a6UK} {2}:: (halfBatchSize <=? batchSize)
                                          ~ 'True (CNonCanonical)}
  |
1 | {-# LANGUAGE DataKinds           #-}
  | ^