Netlist generation fails on `Unsigned 1`

[rowanG077]

After some refactoring I hit a bug where Clash failed during Normalization. When trying reducing to reduce it to a smaller case I no-longer hit a Normalization but hit a netlist generation issue. So I probably will create another issue once this one is fixed.

Anyway I can reproduce the issue with GHC 8.10.7 and with GHC 9.0.2 with both Clash 1.6.3 and the current master.

When I run synthesis I get this error:

<no location info>: error:
    Clash error call:
    Clash.Netlist(1117): mkDcApplication undefined for: (Unsigned 1,Name {nameSort = User, nameOcc = "GHC.Tuple.(,)", nameUniq = 3963167672086036486, nameLoc = UnhelpfulSpan UnhelpfulNoLocationInfo},[Tick (NameMod PrefixName (LitTy (SymTy "$p2(%,%)"))) (Literal (NaturalLiteral 1)),Tick (NameMod PrefixName (LitTy (SymTy "$p2(%,%)"))) (Literal (NaturalLiteral 1))],[Just (Unsigned 64),Just (Unsigned 64)])
    CallStack (from HasCallStack):
      error, called at src/Clash/Netlist.hs:1117:9 in clash-lib-1.7.0-inplace:Clash.Netlist
      mkDcApplication, called at src/Clash/Netlist.hs:842:16 in clash-lib-1.7.0-inplace:Clash.Netlist
      mkExpr, called at src/Clash/Netlist.hs:505:31 in clash-lib-1.7.0-inplace:Clash.Netlist

And the complete compilation output with DebugApplied enabled available here(GHC 9.0.2 + Clash master): https://gist.github.com/rowanG077/3c330bd65a2c7f66907189eef96443c4

I have created a reproducer which contains 3 modules so to make it easy to debug it I have created a repo for it: https://github.com/rowanG077/clash-netlist-gen-bug

It's based on clash-starter so to run it just clone it and run cabal run clash -- Example.TopEntity --verilog It assumes clash sources are available one directory up.

[alex-mckenna]

EDIT: Removed uniques and qualifiers, since they just add clutter.

It goes wrong here:

DEC {72}
Changes when applying rewrite to:
case eta[LocalId] of
  SDRAMInitRefresh (ds :: CounterOverflow 1 1) ->
    case hasOverflown[GlobalId] 1 1 <prefixName>"$p1(%,%)"(Eq# @Bool @True @True (_CO_ @(~# Bool Bool True True))) ds[LocalId] of
      False  ->
        SDRAMInitRefresh @(SDRAMSpec 1) (tick[GlobalId] 1 1 <prefixName>"$p1(%,%)"(Eq# @Bool @True @True (_CO_ @(~# Bool Bool True True))) ds[LocalId])
      True  ->
        SDRAMInitLoadModeReg @(SDRAMSpec 1)
          <prefixName>"initCount"
          (fromInteger# @(+ 1 (CLog 2 (Max (SDRAMtBDL (SDRAMSpec 1)) (SDRAMtBDL (SDRAMSpec 1))))) (naturalAdd 1 <prefixName>"$w$cnatSing2"0)
             (integerFromNatural (naturalAdd (naturalAdd (naturalSubThrow (naturalShiftL# 1 (int2Word# (integerToInt# (integerFromNatural <prefixName>"$w$cnatSing2"0)))) <prefixName>"$p2(%,%)"1) 1) 0)))
  SDRAMInitLoadModeReg (ds :: CounterOverflow (SDRAMtBDL (SDRAMSpec 1)) (SDRAMtBDL (SDRAMSpec 1))) ->
    SDRAMInitLoadModeReg @(SDRAMSpec 1) (tick[GlobalId] <prefixName>"$p2(%,%)"1 <prefixName>"$p2(%,%)"1 (Eq# @Bool @(<=? 1 (SDRAMtBDL (SDRAMSpec 1))) @True (_CO_ @(~# Bool Bool (<=? 1 (SDRAMtBDL (SDRAMSpec 1))) True))) ds[LocalId])
Result:
letrec
  c$tickOut :: CounterOverflow 1 1
  = letrec
      c$tupIn :: (,) (~ Bool True True) (CounterOverflow 1 1)
      = case eta[LocalId] of
          SDRAMInitRefresh (ds :: CounterOverflow 1 1) ->
            (,) @(~ Bool True True) @(CounterOverflow 1 1) <prefixName>"$p1(%,%)"(Eq# @Bool @True @True (_CO_ @(~# Bool Bool True True))) ds[LocalId]
          SDRAMInitLoadModeReg (ds :: CounterOverflow (SDRAMtBDL (SDRAMSpec 1)) (SDRAMtBDL (SDRAMSpec 1))) ->
            (,) @(~ Bool True True) @(CounterOverflow 1 1) <prefixName>"$p2(%,%)"1 <prefixName>"$p2(%,%)"1
  in tick[GlobalId] 1 1
       (case c$tupIn[LocalId] of
          (,) (c$sel :: ~ Bool True True) (c$wild :: CounterOverflow 1 1) ->
            c$sel[LocalId])
       (case c$tupIn[LocalId] of
          (,) (c$wild :: ~ Bool True True) (c$sel :: CounterOverflow 1 1) ->
            c$sel[LocalId])
in case eta[LocalId] of
     SDRAMInitRefresh (ds :: CounterOverflow 1 1) ->
       case hasOverflown[GlobalId] 1 1 <prefixName>"$p1(%,%)"(Eq# @Bool @True @True (_CO_ @(~# Bool Bool True True))) ds[LocalId] of
         False  ->
           SDRAMInitRefresh @(SDRAMSpec 1) c$tickOut[LocalId]
         True  ->
           SDRAMInitLoadModeReg @(SDRAMSpec 1)
             <prefixName>"initCount"
             (fromInteger# @(+ 1 (CLog 2 (Max (SDRAMtBDL (SDRAMSpec 1)) (SDRAMtBDL (SDRAMSpec 1))))) (naturalAdd 1 <prefixName>"$w$cnatSing2"0)
                (integerFromNatural (naturalAdd (naturalAdd (naturalSubThrow (naturalShiftL# 1 (int2Word# (integerToInt# (integerFromNatural <prefixName>"$w$cnatSing2"0)))) <prefixName>"$p2(%,%)"1) 1) 0)))
     SDRAMInitLoadModeReg (ds :: CounterOverflow (SDRAMtBDL (SDRAMSpec 1)) (SDRAMtBDL (SDRAMSpec 1))) ->
       SDRAMInitLoadModeReg @(SDRAMSpec 1) c$tickOut[LocalId]

[christiaanb]

Ugh... DEC, the bane of my existence... as a clash developer.

Anyhow, it seems to mess up selection of the evidence for the coercion. The short term "fix" would be to disable DEC for GADTs. The better fix is thinking of how to deal with GADTs inside DEC.

[rowanG077]

How can I detect whether it's GADT? I rather not disable the entire DEC, since I then also have to use a custom Clash version. I'd be willing to implement this check and make a PR.

[martijnbastiaan]

We've released v1.6.4, which includes a fix for this issue.