Do not pass `deps` to `mkUnivCo` #88

martijnbastiaan · 2025-04-26T11:12:15Z

Causes GHC load issues for Clash, while seemingly not contributing to anything else?

Before this I got an error when upgrading Clash to GHC 9.12:

                /home/martijn/code/clash-compiler/dist-newstyle/build/x86_64-linux/ghc-9.12.2/clash-prelude-1.9.0/build/Clash/Sized/Vector.hi
                Declaration for select
                Unfolding of select:
                  Iface id out of scope:  ipv
                  env: [ESg3Y :-> ds, ESg3Z :-> wild, ESgcH :-> wild1,
                        ESgep :-> ipv1, ESgAw :-> ipv2, ESgGI :-> co, ESgL5 :-> n1,
                        ESgLf :-> xs, ESgPD :-> irred, ESgPF :-> irred1, EShqy :-> s1,
                        EShvV :-> m1, EShxS :-> f1, ESjIm :-> vs, ESjIJ :-> select']
                <no location info>: error:
                    Other error:
                    Failed to load module 'VACC'.
                    
                    Tried to load it from precompiled sources, error was:
                    
                      Internal error: found  module, but could not load it
                    
                    Tried to load it from local sources, error was:
                    
                      Cannot continue after interface file error

After digging a little deeper this was "caused" by the introduction of ipv in select:

https://gist.github.com/martijnbastiaan/8c4d6a753487417f3eefaaca388cc403#file-ghc-9-12-2-hs

Note that I have no idea whether this patch is correct, but it does seem to "solve" my issues on clash-compiler. I did try to remove either (but not both) of the deps passing, but they both cause the same error.

Causes GHC load issues for Clash, while seemingly not contributing to anything else?

christiaanb

These dependencies are critical for type soundness, without them, equalities that only hold locally would be lifted to a global level.

christiaanb · 2025-04-26T12:37:04Z

Perhaps we can be more diligent as to what givens we add as dependencies. Currently we add all the ones that are in scope when we solve a wanted. We should track perhaps which one of those givens are local and which one are global and only add the local givens as dependencies.

christiaanb · 2025-04-26T12:48:02Z

See also:

martijnbastiaan · 2025-04-26T13:42:37Z

Clear! Thanks for your comments!

martijnbastiaan · 2025-04-26T13:49:19Z

Aren't both co and ipv local though?

christiaanb · 2025-04-26T13:57:48Z

They do seem to be local, yeah… could you get GHC debug info with the uniques printed? Because now we only see names, which could be misleading

martijnbastiaan · 2025-04-26T17:18:47Z

It's kind of difficult to reliably reproduce the exact output I got earlier, but it looks like I'm having a similar issue in my current run. I'm getting the same error (Iface id out of scope: ipv), though much earlier in the compile pipeline that prevents me from running showPpr and friends at all. However, when I do -ddump-simpl, I see something interesting (the uniques are represented by _XXXX):

select [InlPrag=OPAQUE]
  :: forall (i :: GHC.Num.Natural.Natural)
            (s :: GHC.Num.Natural.Natural) (n :: GHC.Num.Natural.Natural)
            (f :: Nat) a.
     (((s * n) + 1) <= (i + s)) =>
     SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
[GblId,
 Arity=5,
 Str=<A><MP(SL)><LP(SL)><1P(SL)><L>,
 Unf=Unf{Src=<vanilla>, TopLvl=True,
         Value=True, ConLike=True, WorkFree=True, Expandable=True,
         Guidance=IF_ARGS [0 0 0 0 0] 320 0}]
select
  = \ (@(i_amBw :: GHC.Num.Natural.Natural))
      (@(s_amBx :: GHC.Num.Natural.Natural))
      (@(n_amBy :: GHC.Num.Natural.Natural))
      (@(f_amBz :: Nat))
      (@a_amBA)
      (irred_amBB :: ((s_amBx * n_amBy) + 1) <= (i_amBw + s_amBx))
      (f1_ako5 :: SNat f_amBz)
      (s1_ako6 :: SNat s_amBx)
      (n1_ako7 :: SNat n_amBy)
      (xs_ako8 :: Vec (f_amBz + i_amBw) a_amBA) ->
      letrec {
        select'_ssaT [Occ=LoopBreaker, Dmd=SC(S,C(1,C(1,L)))]
          :: forall (m :: GHC.Num.Natural.Natural)
                    (j :: GHC.Num.Natural.Natural) b.
             (((s_amBx * m) + 1) <= (j + s_amBx)) =>
             UNat m -> Vec j b -> Vec m b
        [LclId, Arity=3, Str=<A><1L><L>, Unf=OtherCon []]
        select'_ssaT
          = \ (@(m_amCW :: GHC.Num.Natural.Natural))
              (@(j_amCX :: GHC.Num.Natural.Natural))
              (@b_amCY)
              _ [Occ=Dead]
              (m1_akoh [OS=OneShot] :: UNat m_amCW)
              (vs_akoi [OS=OneShot] :: Vec j_amCX b_amCY) ->
              case m1_akoh of {
                UZero co_amD4 [Dmd=S] ->
                  (Clash.Sized.Vector.$WNil @b_amCY)
                  `cast` ((Vec (Sym co_amD4) <b_amCY>_R)_R
                          :: Vec 0 b_amCY ~R# Vec m_amCW b_amCY);
                USucc @n2_amDa co_amDb [Dmd=S] ds_drki ->
                  case ds_drki of wild1_X2 {
                    UZero co1_amDd [Dmd=S] ->
                      (Clash.Sized.Vector.Cons
                         @(0 + 1)
                         @b_amCY
                         @0
                         @~(<0 + 1>_N :: (0 + 1) GHC.Prim.~# (0 + 1))
                         (head
                            @(j_amCX - 1)
                            @b_amCY
                            (vs_akoi
                             `cast` ((Vec
                                        Univ(nominal (plugin [ghc-typelits-natnormalise])[Sym (Add0L
                                                                                                   <1>_N)
                                                                                          ; (Sym co_amDd
                                                                                             + <1>_N)_N
                                                                                          ; Sym co_amDb,
                                                                                          Sym co_amDd]
                                             :: j_amCX, (j_amCX - 1) + 1)
                                        <b_amCY>_R)_R
                                     :: Vec j_amCX b_amCY ~R# Vec ((j_amCX - 1) + 1) b_amCY)))
                         (Clash.Sized.Vector.$WNil @b_amCY))
                      `cast` ((Vec
                                 ((Sym co1_amDd + <1>_N)_N
                                  ; Sym co_amDb)
                                 <b_amCY>_R)_R
                              :: Vec (0 + 1) b_amCY ~R# Vec m_amCW b_amCY);
                    USucc @ipv_srWD ipv1_srWE ipv2_srWF ->
                      (Clash.Sized.Vector.Cons
                         @(n2_amDa + 1)
                         @b_amCY
                         @n2_amDa
                         @~(<n2_amDa + 1>_N :: (n2_amDa + 1) GHC.Prim.~# (n2_amDa + 1))
                         (head
                            @(j_amCX - 1)
                            @b_amCY
                            (vs_akoi
                             `cast` ((Vec
                                        Univ(nominal (plugin [ghc-typelits-natnormalise])[ipv_srWE,
                                                                                          co_amDb]
                                             :: j_amCX, (j_amCX - 1) + 1)
                                        <b_amCY>_R)_R
                                     :: Vec j_amCX b_amCY ~R# Vec ((j_amCX - 1) + 1) b_amCY)))
                         (select'_ssaT
                            @n2_amDa
                            @(j_amCX - s_amBx)
                            @b_amCY
                            (GHC.Classes.CUnit
                             `cast` (Univ(representational (plugin [ghc-typelits-natnormalise])[Sym ipv_srWE,
                                                                                                Sym co_amDb]
                                          :: () :: Constraint, ghc-internal:GHC.Internal.TypeError.Assert
                                                                 (ghc-internal:GHC.Internal.Data.Type.Ord.OrdCond
                                                                    (ghc-internal:GHC.Internal.TypeNats.Internal.CmpNat
                                                                       ((s_amBx * n2_amDa) + 1)
                                                                       ((j_amCX - s_amBx) + s_amBx))
                                                                    True
                                                                    True
                                                                    False)
                                                                 (TypeError ...))
                                     ; (ghc-internal:GHC.Internal.TypeError.Assert
                                          (ghc-internal:GHC.Internal.Data.Type.Ord.OrdCond
                                             <Bool>_N
                                             (Sym (ghc-internal:GHC.Internal.Data.Type.Ord.D:R:CompareNaturalab
                                                       <(s_amBx * n2_amDa) + 1>_N
                                                       <(j_amCX - s_amBx) + s_amBx>_N))
                                             <True>_N
                                             <True>_N
                                             <False>_N)_N
                                          <(TypeError ...)>_N)_R
                                     :: (() :: Constraint)
                                        ~R# ghc-internal:GHC.Internal.TypeError.Assert
                                              (ghc-internal:GHC.Internal.Data.Type.Ord.OrdCond
                                                 (ghc-internal:GHC.Internal.Data.Type.Ord.Compare
                                                    ((s_amBx * n2_amDa) + 1)
                                                    ((j_amCX - s_amBx) + s_amBx))
                                                 True
                                                 True
                                                 False)
                                              (TypeError ...)))
                            wild1_X2
                            (case splitAt
                                    @s_amBx
                                    @(j_amCX - s_amBx)
                                    @b_amCY
                                    s1_ako6
                                    (vs_akoi
                                     `cast` ((Vec
                                                Univ(nominal (plugin [ghc-typelits-natnormalise])[ipv_srWE,
                                                                                                  co_amDb]
                                                     :: j_amCX, s_amBx + (j_amCX - s_amBx))
                                                <b_amCY>_R)_R
                                             :: Vec j_amCX b_amCY
                                                ~R# Vec (s_amBx + (j_amCX - s_amBx)) b_amCY))
                             of
                             { (_ [Occ=Dead], y_irV1) ->
                             y_irV1
                             })))
                      `cast` ((Vec (Sym co_amDb) <b_amCY>_R)_R
                              :: Vec (n2_amDa + 1) b_amCY ~R# Vec m_amCW b_amCY)
                  }
              }; } in
      select'_ssaT
        @n_amBy
        @i_amBw
        @a_amBA
        irred_amBB
        (toUNat @n_amBy n1_ako7)
        (case splitAt @f_amBz @i_amBw @a_amBA f1_ako5 xs_ako8 of
         { (_ [Occ=Dead], y_irV1) ->
         y_irV1
         })

Note that the plugin inserts:

                                        Univ(nominal (plugin [ghc-typelits-natnormalise])[ipv_srWE,
                                                                                          co_amDb]

but ipv_srWE isn't in scope. I haven't been able to print whether it is a global or local id.

martijnbastiaan · 2025-04-27T13:06:58Z

@christiaanb Is this something you'd like to look into? If not that's fine of course, but I don't have a good idea on how to debug this. Are there some flags I can feed to GHC/the plugin to make it output more debug info?

christiaanb · 2025-04-27T13:25:18Z

I’ll look into it

martijnbastiaan · 2025-05-26T11:10:57Z

Is this still something you're interested in looking into @christiaanb?

christiaanb · 2025-07-07T14:30:55Z

I think it's fixed in GHC master by ghc/ghc@9f02dfb; it doesn't seem to be back-ported to the 9.12 branch though: https://github.com/ghc/ghc/blame/ghc-9.12/compiler/GHC/Core/TyCo/Tidy.hs#L346-L348

martijnbastiaan · 2025-07-09T14:20:38Z

Thanks. I'll close this issue. Let's wait for https://gitlab.haskell.org/ghc/ghc/-/issues/26185.

Do not pass deps to mkUnivCo

57cb1d0

Causes GHC load issues for Clash, while seemingly not contributing to anything else?

martijnbastiaan mentioned this pull request Apr 26, 2025

Add support for GHC 9.12 clash-lang/clash-compiler#2941

Open

9 tasks

martijnbastiaan requested review from christiaanb and rowanG077 April 26, 2025 11:19

christiaanb requested changes Apr 26, 2025

View reviewed changes

martijnbastiaan closed this Jul 9, 2025

martijnbastiaan deleted the no-deps branch July 9, 2025 14:23

Do not pass deps to mkUnivCo #88

Do not pass deps to mkUnivCo #88

Uh oh!

Conversation

martijnbastiaan commented Apr 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

christiaanb left a comment

Choose a reason for hiding this comment

Uh oh!

christiaanb commented Apr 26, 2025

Uh oh!

christiaanb commented Apr 26, 2025

Uh oh!

martijnbastiaan commented Apr 26, 2025

Uh oh!

martijnbastiaan commented Apr 26, 2025

Uh oh!

christiaanb commented Apr 26, 2025

Uh oh!

martijnbastiaan commented Apr 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

martijnbastiaan commented Apr 27, 2025

Uh oh!

christiaanb commented Apr 27, 2025

Uh oh!

martijnbastiaan commented May 26, 2025

Uh oh!

christiaanb commented Jul 7, 2025

Uh oh!

martijnbastiaan commented Jul 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Do not pass `deps` to `mkUnivCo` #88

Do not pass `deps` to `mkUnivCo` #88

martijnbastiaan commented Apr 26, 2025 •

edited

Loading

martijnbastiaan commented Apr 26, 2025 •

edited

Loading