Add support for GHC 9.12

[martijnbastiaan]

Closes #2930

Still TODO:

• Write a changelog entry (see changelog/README.md)
• Check copyright notices are up to date in edited files
• Fix issues exposed with cabal run -- clash-testsuite -p VACC -p VHDL -p clash
  • Do not pass deps to mkUnivCo ghc-typelits-natnormalise#88
• Fix issues exposed by cabal run -- clash-testsuite -p Numbers -p Strict
  • Good news: unrelated to typechecker business
  • Perhaps we shouldn't use newtype for any GHC version?
• Remove wrongly added changes to Add source for GHC 9.12 executable commit
• Find out how to remove {-# OPTIONS_GHC -Wno-deprecations #-} from clash-ghc/src-ghc/Clash/GHC/Util.hs

[christiaanb]

Do you have more information on what’s going on? As in, how is it failing? Could there be a GHC bug that an OPAQUE pragma isn’t being handled as it should?

Also, would it be possible to run the clash-prelude benchmark to see the effects of newtype vs data?

[martijnbastiaan]

It seems to come down to in which order GHC decides to do the seq/casts.. Here is a minimal reproducer:

module Strict where

import Clash.Prelude

type Nr = Unsigned (64+4)

topEntity :: Nr -> Nr -> Vec 1 Nr
topEntity x y = let res = x + y
        in res `seq` res :> Nil

Normalization log with newtype:

topEntity after normalization:

λ(c$arg :: Unsigned (+ 64 4)) ->
λ(c$arg :: Unsigned (+ 64 4)) ->
letrec
  result :: Vec 1 (Unsigned 68)
  = topEntity1[GlobalId] c$arg[LocalId]
      c$arg[LocalId]
in result[LocalId]

topEntity1 before normalization:

λ(x :: Unsigned (+ 64 4)) ->
λ(y :: Unsigned (+ 64 4)) ->
let
  nt :: Natural
  = +# @68 topEntity2[GlobalId] x[LocalId]
      y[LocalId]
in case nt[LocalId] of
     _ ->
       Cons @(+ 0 1) @(Unsigned 68) @0
         (_CO_ @(~# Natural Natural (+ 0 1) (+ 0 1)))
         nt[LocalId]
         ((Λb ->
            Nil @0 @b (_CO_ @(~# Natural Natural 0 0)))
            @(Unsigned 68))

Normalization log with data:

topEntity after normalization:

λ(c$arg :: Unsigned (+ 64 4)) ->
λ(c$arg :: Unsigned (+ 64 4)) ->
letrec
  result :: Vec 1 (Unsigned 68)
  = topEntity1[GlobalId] c$arg[LocalId]
      c$arg[LocalId]
in result[LocalId]

topEntity1 before normalization:

λ(x :: Unsigned (+ 64 4)) ->
λ(y :: Unsigned (+ 64 4)) ->
let
  res :: Unsigned 68
  = +# @68 topEntity2[GlobalId] x[LocalId]
      y[LocalId]
in case res[LocalId] of
     U (ipv :: Natural) ->
       Cons @(+ 0 1) @(Unsigned 68) @0
         (_CO_ @(~# Natural Natural (+ 0 1) (+ 0 1)))
         res[LocalId]
         ((Λb ->
            Nil @0 @b (_CO_ @(~# Natural Natural 0 0)))
            @(Unsigned 68))

Core with newtype:

topEntity1_r3Mt :: Nr -> Nr -> Vec 1 (Unsigned 68)
[GblId, Arity=2, Str=<L><L>, Unf=OtherCon []]
topEntity1_r3Mt
  = \ (x_a3H7 :: Nr) (y_a3H8 [OS=OneShot] :: Nr) ->
      case (+ @(Unsigned 68)
              $dNum_r3Mo
              (x_a3H7
               `cast` ((Unsigned (AddDef <64>_N <4>_N))_R
                       :: Unsigned (64 + 4) ~R# Unsigned 68))
              (y_a3H8
               `cast` ((Unsigned (AddDef <64>_N <4>_N))_R
                       :: Unsigned (64 + 4) ~R# Unsigned 68)))
           `cast` (Clash.Sized.Internal.Unsigned.N:Unsigned <68>_N
                   :: Unsigned 68 ~R# Natural)
      of nt_s3M1
      { __DEFAULT ->
      (Clash.Sized.Vector.$b:>
         @(Unsigned 68)
         @0
         (nt_s3M1
          `cast` (Sym (Clash.Sized.Internal.Unsigned.N:Unsigned <68>_N)
                  :: Natural ~R# Unsigned 68))
         (Clash.Sized.Vector.$WNil @(Unsigned 68)))
      `cast` ((Vec (Add0L <1>_N) <Unsigned 68>_R)_R
              :: Vec (0 + 1) (Unsigned 68) ~R# Vec 1 (Unsigned 68))
      }

Core with data:

topEntity1_r3Mp :: Nr -> Nr -> Vec 1 (Unsigned 68)
[GblId, Arity=2, Str=<L><L>, Unf=OtherCon []]
topEntity1_r3Mp
  = \ (x_a3H2 :: Nr) (y_a3H3 [OS=OneShot] :: Nr) ->
      case + @(Unsigned 68)
             $dNum_r3Mk
             (x_a3H2
              `cast` ((Unsigned (AddDef <64>_N <4>_N))_R
                      :: Unsigned (64 + 4) ~R# Unsigned 68))
             (y_a3H3
              `cast` ((Unsigned (AddDef <64>_N <4>_N))_R
                      :: Unsigned (64 + 4) ~R# Unsigned 68))
      of res_a3H4
      { Clash.Sized.Internal.Unsigned.U ipv_s3LU ->
      (Clash.Sized.Vector.$b:>
         @(Unsigned 68)
         @0
         res_a3H4
         (Clash.Sized.Vector.$WNil @(Unsigned 68)))
      `cast` ((Vec (Add0L <1>_N) <Unsigned 68>_R)_R
              :: Vec (0 + 1) (Unsigned 68) ~R# Vec 1 (Unsigned 68))
      }

Though I'm not sure, it seems pretty fundamental to me that we cannot support coercion/casts between types that we represent differently in hardware.

[martijnbastiaan]

Love to hear what you make of it.

You did already do a benchmark a while back: #2535. Are you asking for a 9.12 one?

[christiaanb]

No, there doesn't seem to be anything we can do. Once this is merged, could you add an issue to see if we can revert back to newtypes at some later day/ghc version. Maybe we can try once again to track the actual size of Integer and Natural, instead of fixing it at 64.

[martijnbastiaan]

Okay, I'll make an issue. I've got some comments but I'll leave that for the replies there.

@christiaanb It seems to me this is perfectly fine behavior for any GHC, so I'd prefer to remove newtype for every GHC release we support. Agreed?

[martijnbastiaan]

I've added Use data for `Signed`, `Unsigned`, `Index`, and `BiSignalOut` . I didn't add a changelog because I don't think it is a public API change.

[DigitalBrains1]

Could you add 9.12 to the README in the GHC compatibility section as part of this PR?

[DigitalBrains1]

As far as I'm concerned, I'd just put "1.8" there, not the minor. The minor version isn't all that important, and so far we've only indicated the major version. I feel it's kinda implied you pick the latest minor unless there's a strong reason not to.

I also feel a check mark for something we haven't actually tested (Windows and macOS) is a bit too optimistic.
I'm inclined to keep stuff we haven't tested crossed out. If you think crossed out is too negative, maybe we need to add a question mark emoji to indicate "might or might not work, why don't you try".