CLog type family reduction #3078
Description
Clash's normalization time for the following reproducer still grows exponentially in the argument to Run, e.g., on my machine 6s for Run 17, 12s for Run 18, 24s for Run 19, and so forth ...
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
import Clash.Prelude
import GHC.TypeLits.KnownNat
type family Calc (n :: Nat) (t :: Nat) :: Nat where
Calc 0 _ = 1
Calc n t = Calc (n - 1) (t + t)
instance (KnownNat n, KnownNat t) => KnownNat2 $(nameToSymbol ''Calc) n t
where
natSing2 = SNatKn $ calc (natToNum @n) (natToNum @t)
{-# INLINE natSing2 #-}
calc :: Natural -> Natural -> Natural
calc 0 _ = 1
calc n t = calc (n - 1) (t + t)
type Run n = Calc (n - CLog 2 2) 0
topEntity :: Int
topEntity = natToNum @(Run 17)The recipe is simple: we use a custom type family Calc recursing n-times over the first argument and creating an exponentially growing expression via t + t in the second argument. Unfolding the expression, but not evaluating the +-type family then causes the exponential blowup.
Now this problem should have been fixed with #3071, which takes care of reducing the type expression before handing it over to Clash. However, the problem here is the CLog 2 2 being part of the expression to be reduced as well. Looking at the implementation of CLog in ghc-typelits-extra reveals that the equations of the type-family are given by the plugin, but are not part of the Haskell definition at first. Hence, the solution of #3071 won't be able to reduce CLog 2 2, as there is no reduction defined.
This being the actual issue is quite easy to check, as just replacing CLog 2 2 by 1 in the above reproducer fixes the exponential blowup. The behavior can also be checked via loading the example with ghci and executing
ghci> :k! Calc (11 - CLog 2 2) 0
Calc (11 - CLog 2 2) 0 :: Nat
= Calc (11 - CLog 2 2) 0
ghci> :k! Calc (11 - 1) 0
Calc (11 - 1) 0 :: Natural
= 1
It may be that the problem is better to be fixed in the plugin, however, the exponential blowup still is a problem of Clash, which is why I'm reporting the error here at first.