Clash fails to eliminate all sources of polymorphism

[christiaanb]

The following:

{-# LANGUAGE GADTs #-}
module Test where

import Clash.Prelude

data Ex where
  Ex :: forall n . SNat n -> Bool -> Ex

f :: Ex -> Bool
f (Ex n y) = h (replicate n y)
{-# NOINLINE f #-}

h :: Vec n Bool -> Bool
h xs = foldr (||) True xs
{-# NOINLINE h #-}

g :: Int -> Bool -> Ex
g 0 b = Ex (SNat @3) b
g n b = g (n-1) b

topEntity :: Bool -> Bool
topEntity b = f (g 1 b)

fails with:

Test.hs:14:1: error:
    
    Clash.Normalize(179): Clash can only normalize monomorphic functions, but this is polymorphic:
    Test.h :: forall (n :: GHC.Types.Nat).
          Clash.Sized.Vector.Vec n GHC.Types.Bool
          -> GHC.Types.Bool
    
    The source location of the error is not exact, only indicative, as it is acquired 
    after optimizations. The actual location of the error can be in a function that is 
    inlined. To prevent inlining of those functions, annotate them with a NOINLINE pragma.
   |
14 | h xs = foldr (||) True xs
   | ^

Which is happening because Clash considered

data Ex where
  Ex :: forall n . SNat n -> Bool -> Ex

to be "representable" (can have a "trivial" bit-encoding), which in a way it true because the underlying representation of SNat n is a Natural; but does cause certain transformations not to fire leaving h not being specialized on the vector length n. To remedy the situation, Clash should simply consider all types with unconstrained existential types in their data constructors to be "non-representable" as they can induce lingering polymorphism.