Errors with Natural

[martyall]

I was using to the plug-in, and part of my program involved an (==) expression on this type. The plug-in threw the following exception:

ghc: panic! (the 'impossible' happened)
  (GHC version 9.0.2:
    Categorifier failed to categorify the following expression:
\ (ds_dIjG :: (F_BN128, F_BN128)) ->
  case ds_dIjG of { (x, y) ->
  let {
    x_sIkK
      :: Prime
           21888242871839275222246405745257275088548364400416034343698204186575808495617
    [LclId,
     Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
             WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 350 0}]
    x_sIkK
      = let {
          $dKnownNat_sIkE :: Natural
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
          $dKnownNat_sIkE
            = 21888242871839275222246405745257275088548364400416034343698204186575808495617 } in
        let {
          $dNum_aIiq :: Num F_BN128
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=True,
                   WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
          $dNum_aIiq
            = $fNumPrime
                @21888242871839275222246405745257275088548364400416034343698204186575808495617
                ($dKnownNat_sIkE
                 `cast` (Sym (N:SNat[0]
                                  <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P) ; Sym (N:KnownNat[0]) <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N
                         :: Coercible
                              Natural
                              (KnownNat
                                 21888242871839275222246405745257275088548364400416034343698204186575808495617))) } in
        - @F_BN128
          $dNum_aIiq
          (+ @F_BN128 $dNum_aIiq x (fromInteger @F_BN128 $dNum_aIiq 7))
          y } in
  let {
    y_sIkL
      :: Prime
           21888242871839275222246405745257275088548364400416034343698204186575808495617
    [LclId,
     Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
             WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 130 0}]
    y_sIkL = fromInteger @F_BN128 $dNum_aIhK 0 } in
  case case x_sIkK
            `cast` (N:Prime[0] <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N ; N:Mod[0]
                                                                                                                       <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P
                    :: Coercible
                         (Prime
                            21888242871839275222246405745257275088548364400416034343698204186575808495617)
                         Natural)
       of x1
       { __DEFAULT ->
       case y_sIkL
            `cast` (N:Prime[0] <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N ; N:Mod[0]
                                                                                                                       <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P
                    :: Coercible
                         (Prime
                            21888242871839275222246405745257275088548364400416034343698204186575808495617)
                         Natural)
       of y1
       { __DEFAULT ->
       case naturalEq# x1 y1 of wild { __DEFAULT ->
       tagToEnum# @Bool wild
       }
       }
       }
  of {
    False -> fromInteger @F_BN128 $dNum_aIhK 0;
    True -> fromInteger @F_BN128 $dNum_aIhK 42
  }
  }
  - The Categorifier plugin was unable to inline naturalEq#

My understanding from the discord thread is that the expression had been optimized to the underlying Natural type by the time it hit the plug-in, and there is apparently no support for Natural.

I guess I either need (1) to add support for Natural to the plugin or (2) better understand what classes need to be implemented in order to compile the Prime p type. It is also a supported object in my target category.

You can find the offending program here: https://github.com/martyall/straw/blob/snarkl-json-update/examples/Examples/Arithmetic.hs#L50-L64

[sellout]

@martyall Can you try this with the branch from #102? I’m having trouble getting your fork of straw to build. You’ll need to add the extra flags, etc. mentioned in the commend on that PR.

[martyall]

So I think I'm including everything, but I'm still getting the same error. I see that you have added support for naturalEq in that branch, so I don't really understand.

here is the diff and commit you can try to build from: https://github.com/torsion-labs/straw/commit/2894049def14cd05037d8a825742e32a2eb14fed

(NOTE: the github org on that url is no longer martyall, we moved everything over. however, curious why the build failed for you. If you are using the flake shell (nix develop) and building with cabal, it would hopefully work...)

[sellout]

I’m not too surprised. If you look at the error, you see naturalEq#, not naturalEq. The former has the type Natural# -> Natural# -> Bool – those # means the type is “unlifted” and they actually have a different kind than Type.

For a few reasons (which I’m happy to get into) the plugin doesn’t support unlifted types (I need to document that). But most operations on unlifted types have a lifted equivalent. And it’s a matter of catching the operation before it’s been inlined far enough to get down to unlifted types.

That PR has the initial work for Natural support, but I basically crossed my fingers that it’d work without any additional changes to manage the inlining.

Re: building Straw, I don’t know why I didn’t try that. I had only tried nix build …. But I’ll go back to it now, and probably I can replicate the issue.

[martyall]

Re: building Straw, I don’t know why I didn’t try that. I had only tried nix build …. But I’ll go back to it now, and probably I can replicate the issue.

Also in case it helps you can use this binary cache which has all the stuff martyall.cachix.org-1:CrJFPxvYeNEFevcbWAD/Hj1NYu9mtGbLh6Bojvc9TBE=

[zliu41]

The plugin needs to have the ability to output something similar to a stack trace, which will make it a lot easier to figure out where naturalEq# is introduced. Showing just the last CoreExpr is rarely helpful.

[sellout]

Sorry, this was not fixed by #102 (as discussed above). I just forgot to fix the description of that PR before merging.

[martyall]

@sellout Just wanted to check in on this one. After thinking about it a little bit, I could also change the underlying representation of Prime to be Integer instead of Mod, which AFAIK the plugin supports. This would require some amount of work on my fork, but maybe it's easier than making this change for the plugin ?

[sellout]

I don’t think Integer will be any better. Both it and Natural changed the same way with GHC 9.0. GHC 8.10 shouldn’t have this issue, if your code would work with that for the time being. However, I really want to fix this in the plugin.

I did manage to replicate the issue locally, and I think I know what needs to change. I can try to make those changes today. In parallel, I also want to write more documentation on how to debug this and how to extend the plugin properly (took long enough to get it back in my head that there clearly needs to be more explanation if anyone else is going to have a chance).

[martyall]

I didn't try it with raw Integer, but I did just swap out the implementation of galois-fields to use this instead

https://hackage.haskell.org/package/modular-arithmetic-2.0.0.3/docs/Data-Modular.html

instantiating newtype Prime p = Prime (Mod Integer p)

which resulted in an even stranger error message

ghc: panic! (the 'impossible' happened)
  (GHC version 9.0.2:
    Categorifier failed to categorify the following expression:
\ (ds_db4C :: (F_BN128, F_BN128)) ->
  case ds_db4C of { (x, y) ->
  let {
    x_sdV6
      :: Prime
           21888242871839275222246405745257275088548364400416034343698204186575808495617
    [LclId,
     Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
             WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 380 0}]
    x_sdV6
      = let {
          $dKnownNat_sdU4 :: Natural
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
          $dKnownNat_sdU4
            = 21888242871839275222246405745257275088548364400416034343698204186575808495617 } in
        let {
          $d~_aalD :: 'True ~ 'True
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 0 10}]
          $d~_aalD
            = Eq# @Bool @'True @'True @~(<'True>_N :: 'True ~ 'True) } in
        let {
          $d(%,%)_aalB
            :: (KnownNat
                  21888242871839275222246405745257275088548364400416034343698204186575808495617,
                'True ~ 'True)
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
          $d(%,%)_aalB
            = ($dKnownNat_sdU4
               `cast` (Sym (N:SNat[0]
                                <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P) ; Sym (N:KnownNat[0]) <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N
                       :: Coercible
                            Natural
                            (KnownNat
                               21888242871839275222246405745257275088548364400416034343698204186575808495617)),
               $d~_aalD) } in
        let {
          $dNum_aals :: Num F_BN128
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=True,
                   WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
          $dNum_aals
            = $fNumPrime
                @21888242871839275222246405745257275088548364400416034343698204186575808495617
                ($d(%,%)_aalB
                 `cast` (((%,%)
                            <KnownNat
                               21888242871839275222246405745257275088548364400416034343698204186575808495617>_N
                            ((~)
                               <Bool>_N
                               (Sym (LeqDef (<1>_N,
                                             <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N)))
                               <'True>_N)_N)_R
                         :: Coercible
                              (KnownNat
                                 21888242871839275222246405745257275088548364400416034343698204186575808495617,
                               'True ~ 'True)
                              (KnownNat
                                 21888242871839275222246405745257275088548364400416034343698204186575808495617,
                               (1
                                <=? 21888242871839275222246405745257275088548364400416034343698204186575808495617)
                               ~ 'True))) } in
        - @F_BN128
          $dNum_aals
          (+ @F_BN128 $dNum_aals x (fromInteger @F_BN128 $dNum_aals 7))
          y } in
  let {
    y_sdV7
      :: Prime
           21888242871839275222246405745257275088548364400416034343698204186575808495617
    [LclId,
     Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
             WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 130 0}]
    y_sdV7 = fromInteger @F_BN128 $dNum_aa9f 0 } in
  case case x_sdV6
            `cast` (N:Prime[0] <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N ; N:Mod[0]
                                                                                                                       <Integer>_R
                                                                                                                       <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P
                    :: Coercible
                         (Prime
                            21888242871839275222246405745257275088548364400416034343698204186575808495617)
                         Integer)
       of x1
       { __DEFAULT ->
       case y_sdV7
            `cast` (N:Prime[0] <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N ; N:Mod[0]
                                                                                                                       <Integer>_R
                                                                                                                       <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P
                    :: Coercible
                         (Prime
                            21888242871839275222246405745257275088548364400416034343698204186575808495617)
                         Integer)
       of y1
       { __DEFAULT ->
       case integerEq# x1 y1 of wild { __DEFAULT ->
       tagToEnum# @Bool wild
       }
       }
       }
  of {
    False -> fromInteger @F_BN128 $dNum_aa9f 0;
    True -> fromInteger @F_BN128 $dNum_aa9f 42
  }
  }
  - Categorifier encountered a primop-related expression it can't handle at 'replacePrimOps':
        CO: <'True>_N
    (seen 1 time)

Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

Error: cabal: Failed to build test:examples from straw-0.1.0.0.

My GHC Core skills aren't strong enough to know exactly what this means, but it seems like it doesn't like the value level witness for some kind of type equality check

let {
          $d~_aalD :: 'True ~ 'True
          [LclId,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 0 10}]
          $d~_aalD
            = Eq# @Bool @'True @'True @~(<'True>_N :: 'True ~ 'True) } in

FWIW I am using GHC 9.0.2

Thanks for tracking this down, I look forward to whatever solution ends up working. I am also eager to learn more, so it's interesting to me to see these changes coming in :)

[martyall]

I don’t think Integer will be any better. Both it and Natural changed the same way with GHC 9.0. GHC 8.10 shouldn’t have this issue, if your code would work with that for the time being. However, I really want to fix this in the plugin.

Are you saying that this should JustWork™ (with the Natural based galois-fields implementation) if I switch to 8.10 ?

[sellout]

Are you saying that this should JustWork™ (with the Natural based galois-fields implementation) if I switch to 8.10 ?

Well, I think at least this particular problem should go away. I.e., == should work the way + and * do in the simpleArith example.

[martyall]

I don’t think Integer will be any better. Both it and Natural changed the same way with GHC 9.0. GHC 8.10 shouldn’t have this issue, if your code would work with that for the time being. However, I really want to fix this in the plugin.

What you're saying tracks with my experience. I ripped out all of this type witness nonsense from the Integer based implementation in modular-arithmetic and got a similar error as before:

  - The Categorifier plugin was unable to inline integerEq#
  ((let {
      $dKnownNat_sdSS :: Natural
      [LclId]
      $dKnownNat_sdSS
        = 21888242871839275222246405745257275088548364400416034343698204186575808495617 } in
    let {
      $dNum_aakk :: Num F_BN128
      [LclId]
      $dNum_aakk
        = $fNumPrime
            @21888242871839275222246405745257275088548364400416034343698204186575808495617
            ($dKnownNat_sdSS
             `cast` (Sym (N:SNat[0]
                              <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P) ; Sym (N:KnownNat[0]) <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N
                     :: Coercible
                          Natural
                          (KnownNat
                             21888242871839275222246405745257275088548364400416034343698204186575808495617))) } in
    - @F_BN128
      $dNum_aakk
      (+ @F_BN128
         $dNum_aakk
         (fst @F_BN128 @F_BN128 ds_db3l)
         (fromInteger @F_BN128 $dNum_aakk 7))
      (snd @F_BN128 @F_BN128 ds_db3l))
   `cast` (N:Prime[0] <21888242871839275222246405745257275088548364400416034343698204186575808495617>_N ; N:Mod[0]
                                                                                                              <Integer>_R
                                                                                                              <21888242871839275222246405745257275088548364400416034343698204186575808495617>_P
           :: Coercible
                (Prime
                   21888242871839275222246405745257275088548364400416034343698204186575808495617)
                Integer))
  y1.
    There is no unfolding available for the identifier. It's possible that the
    identifier is an unspecialized type class method (methods never have
    unfoldings), a name used for `RebindableSyntax`, or that the unfolding
    somehow didn't get from the definition point to the module that called
   `categorify`.