Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

zipEqual: left list is longer #2812

Open
kleinreact opened this issue Sep 26, 2024 · 3 comments
Open

zipEqual: left list is longer #2812

kleinreact opened this issue Sep 26, 2024 · 3 comments

Comments

@kleinreact
Copy link
Contributor

The following reproducer

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=20 #-}
module Top where

import Clash.Prelude

import Data.Proxy
import Data.Type.Bool

data T = A

type family TF (t :: T) :: Nat where
  TF A = 32

data TFacts (t :: T) where
  TFacts :: KnownNat (TF t)  => Proxy t -> TFacts t

class    KnownT t where knownT :: TFacts t
instance KnownT A where knownT  = TFacts Proxy

type RSF t n = If (n <=? TF t) (Div (TF t) n) 1

go ::
  forall t n.
  ( KnownT t, KnownNat n, 1 <= n
  , 1 <= If (n <=? (TF t)) (Div (TF t) n) 1
  ) => BitVector n -> Vec (RSF t n) (BitVector n)
go inp | TFacts{} <- knownT @t = bitCoerce
  $ let ext :: BitVector n -> BitVector (n * RSF t n)
        ext = extend @_ @_ @(n * RSF t n - n)
     in unpack (ext inp) :: Unsigned (n * RSF t n)

topEntity ::
  HiddenClockResetEnable System =>
  Signal System (Vec (RSF A 8) (BitVector 8))
topEntity = go @A @8 <$> pure 0

produces a

Clash: Compiling Top.topEntity

<no location info>: error:
    Clash error call:
    zipEqual: left list is longer
    CallStack (from HasCallStack):
      error, called at src/Data/List/Extra.hs:140:19 in clash-lib-1.9.0-inplace:Data.List.Extra
      zipEqual, called at src/Clash/Normalize/Transformations/Case.hs:206:19 in clash-lib-1.9.0-inplace:Clash.Normalize.Transformations.Case
      caseCon', called at src/Clash/Normalize/Transformations/Case.hs:154:32 in clash-lib-1.9.0-inplace:Clash.Normalize.Transformations.Case
      caseCon, called at src/Clash/Normalize/Transformations/Case.hs:273:23 in clash-lib-1.9.0-inplace:Clash.Normalize.Transformations.Case
      caseCon', called at src/Clash/Normalize/Transformations/Case.hs:154:32 in clash-lib-1.9.0-inplace:Clash.Normalize.Transformations.Case
      caseCon, called at src/Clash/Normalize/Strategy.hs:91:36 in clash-lib-1.9.0-inplace:Clash.Normalize.Strategy

but only if the debug flag has been enabled for clash-lib. Otherwise, it compiles just fine.

I don't think that this one is related to #2376, although producing the same error message, as the example makes no use of unsafeCoerce at all.
@leonschoorl
Copy link
Member

leonschoorl commented Oct 1, 2024 •
edited
Loading

The problematic transformation causing the zipEqual error is:

caseCon {39}
Changes when applying rewrite to:
case GHC.Prim.tagToEnum# @GHC.Types.Bool (GHC.Prim.leWord# 8## 32##) of
  GHC.TypeLits.KnownNat.SFalse
    (co :: GHC.Prim.~#
             GHC.Types.Bool
             GHC.Types.Bool
             (Data.Type.Ord.OrdCond
                GHC.Types.Bool
                (GHC.TypeNats.Internal.CmpNat 8 (Top.TF Top.A))
                GHC.Types.True
                GHC.Types.True
                GHC.Types.False)
             GHC.Types.False) ->
    GHC.Num.Natural.NS 1##
  GHC.TypeLits.KnownNat.STrue
    (ipv :: GHC.Prim.~#
              GHC.Types.Bool
              GHC.Types.Bool
              (Data.Type.Ord.OrdCond
                 GHC.Types.Bool
                 (GHC.TypeNats.Internal.CmpNat 8 (Top.TF Top.A))
                 GHC.Types.True
                 GHC.Types.True
                 GHC.Types.False)
              GHC.Types.True) ->
    GHC.Num.Natural.naturalQuot (GHC.Num.Natural.NS 32##) (GHC.Num.Natural.NS 8##)
Result:
GHC.Num.Natural.naturalQuot (GHC.Num.Natural.NS 32##) (GHC.Num.Natural.NS 8##)

Here GHC.Prim.tagToEnum# @GHC.Types.Bool (GHC.Prim.leWord# 8## 32##) evaluates to GHC.Types.True.
But True doesn't take any arguments, while the STrue in the pattern does take an (unused) argument.
That's what leads zipEqual to throw the error when build with the debug flag.

Looks like this problematic case statement comes from inlining this KnownNat2Bool instance:

inlineWorkFree {37}
Changes when applying rewrite to:
GHC.TypeLits.KnownNat.$fKnownNat2BoolNatural"Data.Type.Bool.If"abc1[GlobalId]
  @(Data.Type.Ord.OrdCond
      GHC.Types.Bool
      (GHC.TypeNats.Internal.CmpNat 8 (Top.TF Top.A))
      GHC.Types.True
      GHC.Types.True
      GHC.Types.False)
  @(GHC.TypeNats.Div (Top.TF Top.A) 8)
  @1
  (GHC.Prim.tagToEnum# @GHC.Types.Bool
     (GHC.Prim.leWord# 8## 32##))
  (GHC.Num.Natural.naturalQuot
     (GHC.Num.Natural.NS 32##)
     (GHC.Num.Natural.NS 8##))
  (GHC.Num.Natural.NS 1##)
Result:
(Λa ->
  Λb ->
  Λc ->
  λ($dKnownBool :: GHC.TypeLits.KnownNat.KnownBool
                     a) ->
  λ($dKnownNat :: GHC.TypeNats.KnownNat b) ->
  λ($dKnownNat1 :: GHC.TypeNats.KnownNat c) ->
  case $dKnownBool[LocalId] of
    GHC.TypeLits.KnownNat.SFalse
      (co :: GHC.Prim.~#
               GHC.Types.Bool
               GHC.Types.Bool
               a
               GHC.Types.False) ->
      $dKnownNat1[LocalId]
    GHC.TypeLits.KnownNat.STrue
      (ipv :: GHC.Prim.~#
                GHC.Types.Bool
                GHC.Types.Bool
                a
                GHC.Types.True) ->
      $dKnownNat[LocalId])
  @(Data.Type.Ord.OrdCond
      GHC.Types.Bool
      (GHC.TypeNats.Internal.CmpNat 8 (Top.TF Top.A))
      GHC.Types.True
      GHC.Types.True
      GHC.Types.False)
  @(GHC.TypeNats.Div (Top.TF Top.A) 8)
  @1
  (GHC.Prim.tagToEnum# @GHC.Types.Bool
     (GHC.Prim.leWord# 8## 32##))
  (GHC.Num.Natural.naturalQuot
     (GHC.Num.Natural.NS 32##)
     (GHC.Num.Natural.NS 8##))
  (GHC.Num.Natural.NS 1##)

Probably caused by ghc-typelits-knownnat lying to us here that SBool ~ Bool.

@christiaanb
Copy link
Member

Ah, so the problem is also that we drop casts in the translation from GHC's Core to Clash's Core. So something that will need #1064

@kleinreact
Copy link
Contributor Author

I made two more observations here:

  1. The zipEqual error goes away on GHC 9.10.
  2. The following error pops up instead, if I compile the reproducer with -fclash-compile-ultra, which looks quite related to the problem mentioned by @leonschoorl above.
<no location info>: error:
    Clash error call:
    scrutinise: case GHC.Types.True[3891110078048108586] of
      GHC.TypeLits.KnownNat.SFalse[8214565720323787694]
        (co[8214565720323811387] :: GHC.Prim.~#[3674937295934324842]
                                      GHC.Types.Bool[3674937295934324744]
                                      GHC.Types.Bool[3674937295934324744]
                                      (GHC.Internal.Data.Type.Ord.OrdCond[8214565720323788087]
                                         GHC.Types.Bool[3674937295934324744]
                                         (GHC.Internal.TypeNats.Internal.CmpNat[3674937295934325550]
                                            8
                                            (Top.TF[8214565720323799923] Top.A[8214565720323799925]))
                                         GHC.Types.True[3891110078048108586]
                                         GHC.Types.True[3891110078048108586]
                                         GHC.Types.False[3891110078048108556])
                                      GHC.Types.False[3891110078048108556]) ->
        x[3][LocalId]
      GHC.TypeLits.KnownNat.STrue[8214565720323787695]
        (ipv[8214565720323811389] :: GHC.Prim.~#[3674937295934324842]
                                       GHC.Types.Bool[3674937295934324744]
                                       GHC.Types.Bool[3674937295934324744]
                                       (GHC.Internal.Data.Type.Ord.OrdCond[8214565720323788087]
                                          GHC.Types.Bool[3674937295934324744]
                                          (GHC.Internal.TypeNats.Internal.CmpNat[3674937295934325550]
                                             8
                                             (Top.TF[8214565720323799923] Top.A[8214565720323799925]))
                                          GHC.Types.True[3891110078048108586]
                                          GHC.Types.True[3891110078048108586]
                                          GHC.Types.False[3891110078048108556])
                                       GHC.Types.True[3891110078048108586]) ->
        x[4][LocalId]
    CallStack (from HasCallStack):
      error, called at src-ghc/Clash/GHC/Evaluator.hs:475:3 in clash-ghc-1.9.0-inplace:Clash.GHC.Evaluator

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@christiaanb @leonschoorl @kleinreact