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.

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

primitive-unlifted-1.0.0.0 fails Core Lint on GHC 9.0 and later #24

Open
RyanGlScott opened this issue Mar 9, 2021 · 5 comments
Open

Comments

@RyanGlScott
Copy link

If you compile primitive-unlifted-1.0.0.0 using the -dcore-lint flag with GHC 9.0 or later, Core Lint will fail on the tryTakeUnliftedMVar# function in Data.Primitive.Unlifted.MVar.Primops. Here is a minimized example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnliftedNewtypes #-}
{-# OPTIONS_GHC -dcore-lint #-}
module Bug where

import GHC.Exts
import GHC.Types

newtype UnliftedMVar# s (a :: TYPE UnliftedRep) = UnliftedMVar# (MVar# s Any)

tryTakeUnliftedMVar# :: UnliftedMVar# s a -> State# s -> (# State# s, (# (##) | a #) #)
{-# NOINLINE tryTakeUnliftedMVar# #-}
tryTakeUnliftedMVar# (UnliftedMVar# mv) s =
  case unsafeCoerce# (tryTakeMVar# mv s) of
    (# s', 0#, _ #) -> (# s', (#(##)| #)#)
    (# s', _, a #) -> (# s', (#|a #) #)
$ /opt/ghc/9.0.1/bin/ghc Bug.hs -dcore-lint -dno-typeable-binds -fprint-explicit-kinds
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:17:41: warning:
    This argument does not satisfy the let/app invariant:
      ipv_szM
      `cast` (Nth:5
                  (GRefl representational (# State# s_ax4, Int#, Any @(*) #)
                       (TYPE v1_azo)_N ; Sub v2_azr)
              :: (Any @(*) :: *) ~R# (a_ax5 :: TYPE 'UnliftedRep))
    In the RHS of tryTakeUnliftedMVar# :: forall s
                                                 (a :: TYPE 'UnliftedRep).
                                          UnliftedMVar# s a
                                          -> State# s -> (# State# s, (# (# #) | a #) #)
    In the body of lambda with binder s_ax4 :: *
    In the body of lambda with binder a_ax5 :: TYPE 'UnliftedRep
    In the body of lambda with binder ds_dz9 :: UnliftedMVar#
                                                  s_ax4 a_ax5
    In the body of lambda with binder s_avZ :: State# s_ax4
    In a case alternative: ((#,,#) ipv_szK :: State# s_ax4,
                                   ipv_szL :: Int#,
                                   ipv_szM :: Any @(*))
    In a case alternative: (UnsafeRefl v1_azo :: ('TupleRep
                                                    ((':)
                                                       @RuntimeRep
                                                       ('TupleRep ('[] @RuntimeRep))
                                                       ((':)
                                                          @RuntimeRep
                                                          'IntRep
                                                          ((':)
                                                             @RuntimeRep
                                                             'LiftedRep
                                                             ('[] @RuntimeRep)))) :: RuntimeRep)
                                                 ~# ('TupleRep
                                                       ((':)
                                                          @RuntimeRep
                                                          ('TupleRep ('[] @RuntimeRep))
                                                          ((':)
                                                             @RuntimeRep
                                                             'IntRep
                                                             ((':)
                                                                @RuntimeRep
                                                                'UnliftedRep
                                                                ('[] @RuntimeRep)))) :: RuntimeRep))
    In a case alternative: (UnsafeRefl v2_azr :: (((# State# s_ax4,
                                                      Int#, Any @(*) #) |> (TYPE v1_azo)_N) :: TYPE
                                                                                                 ('TupleRep
                                                                                                    ((':)
                                                                                                       @RuntimeRep
                                                                                                       ('TupleRep
                                                                                                          ('[]
                                                                                                             @RuntimeRep))
                                                                                                       ((':)
                                                                                                          @RuntimeRep
                                                                                                          'IntRep
                                                                                                          ((':)
                                                                                                             @RuntimeRep
                                                                                                             'UnliftedRep
                                                                                                             ('[]
                                                                                                                @RuntimeRep))))))
                                                 ~# ((# State# s_ax4, Int#, a_ax5 #) :: TYPE
                                                                                          ('TupleRep
                                                                                             ((':)
                                                                                                @RuntimeRep
                                                                                                ('TupleRep
                                                                                                   ('[]
                                                                                                      @RuntimeRep))
                                                                                                ((':)
                                                                                                   @RuntimeRep
                                                                                                   'IntRep
                                                                                                   ((':)
                                                                                                      @RuntimeRep
                                                                                                      'UnliftedRep
                                                                                                      ('[]
                                                                                                         @RuntimeRep)))))))
    Substitution: [TCvSubst
                     In scope: InScope {s_ax4 a_ax5 v1_azo v2_azr}
                     Type env: [ax4 :-> s_ax4, ax5 :-> a_ax5]
                     Co env: [azo :-> v1_azo, azr :-> v2_azr]]
*** Offending Program ***
tryTakeUnliftedMVar# [InlPrag=NOINLINE]
  :: forall s (a :: TYPE 'UnliftedRep).
     UnliftedMVar# s a -> State# s -> (# State# s, (# (# #) | a #) #)
[LclIdX,
 Arity=2,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [0 0] 73 20}]
tryTakeUnliftedMVar#
  = \ (@s_ax4)
      (@(a_ax5 :: TYPE 'UnliftedRep))
      (ds_dz9 :: UnliftedMVar# s_ax4 a_ax5)
      (s_avZ :: State# s_ax4) ->
      case tryTakeMVar#
             @s_ax4
             @(Any @(*))
             (ds_dz9
              `cast` (N:UnliftedMVar#[0] <s_ax4>_N <a_ax5>_P
                      :: (UnliftedMVar# s_ax4 a_ax5 :: TYPE 'UnliftedRep)
                         ~R# (MVar# s_ax4 (Any @(*)) :: TYPE 'UnliftedRep)))
             s_avZ
      of wild_X1
      { (# ipv_szK, ipv_szL, ipv_szM #) ->
      case unsafeEqualityProof
             @RuntimeRep
             @('TupleRep
                 ((':)
                    @RuntimeRep
                    ('TupleRep ('[] @RuntimeRep))
                    ((':)
                       @RuntimeRep
                       'IntRep
                       ((':) @RuntimeRep 'UnliftedRep ('[] @RuntimeRep)))))
             @('TupleRep
                 ((':)
                    @RuntimeRep
                    ('TupleRep ('[] @RuntimeRep))
                    ((':)
                       @RuntimeRep
                       'IntRep
                       ((':) @RuntimeRep 'LiftedRep ('[] @RuntimeRep)))))
      of
      { UnsafeRefl v1_azo ->
      case unsafeEqualityProof
             @(TYPE
                 ('TupleRep
                    ((':)
                       @RuntimeRep
                       ('TupleRep ('[] @RuntimeRep))
                       ((':)
                          @RuntimeRep
                          'IntRep
                          ((':) @RuntimeRep 'UnliftedRep ('[] @RuntimeRep))))))
             @(# State# s_ax4, Int#, a_ax5 #)
             @((# State# s_ax4, Int#, Any @(*) #) |> (TYPE v1_azo)_N)
      of
      { UnsafeRefl v2_azr ->
      case ipv_szL of {
        __DEFAULT ->
          (# ipv_szK,
             (#|_#)
               @('TupleRep ('[] @RuntimeRep))
               @'UnliftedRep
               @(# #)
               @a_ax5
               (ipv_szM
                `cast` (Nth:5
                            (GRefl representational (# State# s_ax4, Int#, Any @(*) #)
                                 (TYPE v1_azo)_N ; Sub v2_azr)
                        :: (Any @(*) :: *) ~R# (a_ax5 :: TYPE 'UnliftedRep))) #);
        0# ->
          (# ipv_szK,
             (#_|#)
               @('TupleRep ('[] @RuntimeRep)) @'UnliftedRep @(# #) @a_ax5 (##) #)
      }
      }
      }
      }

*** End of Offense ***


<no location info>: error: 
Compilation had errors

It's unclear to me if this is a GHC bug or an unsound use of unsafeCoerce# (in particular, I'm not sure if the coercion from Any @(*) :: * to a_ax5 :: TYPE 'UnliftedRep is sound), so I thought I'd raise an issue here first.

@andrewthad
Copy link
Collaborator

@treeowl has written most of the current incantation of primitive-unlifted, so he would be more likely to know the answer. I'm not too concerned about this though. Since boxed rep recently made it into GHC head and unlifted data types looks like it's about to land, the whole primitive-unlifted library feels much less useful to me than it once has.

At the least, it's probably doing a hackage revision to clarify that this is not expected to work with GHC 9.0. @treeowl What do you think?

@treeowl
Copy link
Contributor

treeowl commented Mar 9, 2021 via email

@RyanGlScott
Copy link
Author

Do you know if the primop updates will happen in that version?

The BoxedRep commit, as far as I can see, has only updated RuntimeRep itself, not only primops. I'm not aware of any work done towards updating primops to use BoxedRep yet, which is being tracked in GHC#18080.

@treeowl
Copy link
Contributor

treeowl commented Mar 9, 2021 via email

@andrewthad
Copy link
Collaborator

I'm working on that at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5218

It doesn't seem like it's going to be difficult. Once I figure out what I messed up with Array#, I think nearly all the others should fall into place.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants