Assertion failure for comfort-array-0.5.2.3 with GHC 9.4

Which exact GHC version?

9.4.6 and 9.4.7 at least.

mentioned in issue #23865 (closed)

I did some research and this might be caused by #23865 (closed), but I haven't confirmed for sure.

mentioned in issue #23877 (moved)

mentioned in issue head.hackage#91

added CPR/boxity analysis Pnormal Tbug assertion failure labels

@monoidal @wz1000 Which module is this in? What is the suspect code?

Data.Array.Comfort.Shape

Here's a standalone testcase. To reproduce: ghc -O Shape with a debug compiler. It crashes 9.4 as well as master.

The assertion failure happens during CPR so my earlier suspicion about 23865 was wrong - this is about Core. cc @sgraf812.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
module Shape where

data Checked
data Unchecked

data family Result check a
data instance Result Checked a = CheckedResult a
newtype instance Result Unchecked a = UncheckedResult a

data CheckSingleton check where
   Checked :: CheckSingleton Checked
   Unchecked :: CheckSingleton Unchecked

und :: Bool -> Bool
und x = und x

app :: forall check. (() -> CheckSingleton check) -> Result check Bool
app m = let f :: Result check (Bool -> Bool)
            f = case m () of
                   Checked -> CheckedResult und
                   Unchecked -> UncheckedResult und
        in case m () of
             Checked -> case f of
                          CheckedResult x -> CheckedResult (x True)
             Unchecked -> UncheckedResult True

I've cleaned it up further.

mentioned in issue #23819 (closed)

@sgraf812 any thoughts? This is in CPR

Oh, seems this went under my radar. Thanks for the small reproducer, @monoidal!

We get this Core for app:

app
  = \ (@check_aEL)
      (m_awL [Dmd=SC(S,L)] :: () -> CheckSingleton check_aEL) ->
      case m_awL GHC.Tuple.Prim.() of {
        Checked co_aFn [Dmd=S] ->
          case m_awL GHC.Tuple.Prim.() of {
            Checked co_aF3 [Dmd=B] ->
              (T23862.CheckedResult @Bool (und GHC.Types.True))
              `cast` ((Sym (T23862.D:R:ResultCheckeda0[0])
                       ; (Result (Sym co_aFn))_R) <Bool>_N
                      :: T23862.R:ResultCheckeda Bool ~R# Result check_aEL Bool);
            Unchecked co_aFb [Dmd=S] ->
              case und
                   `cast` (Sym (T23862.N:R:ResultUncheckeda[0] <Bool -> Bool>_N)
                           ; (Sym (T23862.D:R:ResultUncheckeda0[0])
                              ; (Result
                                   (Sym co_aFb
                                    ; co_aFn))_R
                              ; T23862.D:R:ResultCheckeda0[0]) <Bool -> Bool>_N
                           :: (Bool -> Bool) ~R# T23862.R:ResultCheckeda (Bool -> Bool))
              of
              { CheckedResult x_awN [Dmd=MC(1,L)] ->
              (T23862.CheckedResult @Bool (x_awN GHC.Types.True))
              `cast` ((Sym (T23862.D:R:ResultCheckeda0[0])
                       ; (Result (Sym co_aFn))_R) <Bool>_N
                      :: T23862.R:ResultCheckeda Bool ~R# Result check_aEL Bool)
              }
          };
        Unchecked co_aFC [Dmd=S] ->
          GHC.Types.True
          `cast` (Sym (T23862.N:R:ResultUncheckeda[0] <Bool>_N)
                  ; (Sym (T23862.D:R:ResultUncheckeda0[0])
                     ; (Result (Sym co_aFC))_R) <Bool>_N
                  :: Bool ~R# Result check_aEL Bool)
      }

Take note of the dead case und |> co of CheckedResult x -> rhs expression after we matched m () both for Checked and then for Unchecked. The two coercions co_aFn and co_aFb should be contradictory! Furthermore, it is an absolute mystery to me where that Case alternative comes from. Certainly it's not part of the original program!

The resilient solution here is to turn the arity assertion into a check and produce top. But I find this kind of code a bit troublesome, dead as it may be.

Here's an even smaller reproducer with the problematic bits and the Note I drafted to explain what goes wrong in CPR:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

module T23862 where

data family Result (check :: Bool) a
data instance Result True a = CheckedResult a
newtype instance Result False a = UncheckedResult a

data CheckSingleton (check :: Bool) where
   Checked :: CheckSingleton True
   Unchecked :: CheckSingleton False

app :: (() -> CheckSingleton check) -> Result check Bool
app m = case (m (), m ()) of
 (Checked, Unchecked)
   | CheckedResult x <- UncheckedResult (\_ -> True)
   -> CheckedResult (x True)

Note [Dead code may contain type confusions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In T23862, we have a nested case match that looks like this

  data CheckSingleton (check :: Bool) where
    Checked :: CheckSingleton True
    Unchecked :: CheckSingleton False
  data family Result (check :: Bool) a
  data instance Result True a = CheckedResult a
  newtype instance Result True a = UncheckedResult a

  case m () of Checked co1 ->
    case m () of Unchecked co2 ->
      case ((\_ -> True)
             |> .. UncheckedResult ..
             |> sym co2
             |> co1) :: Result True (Bool -> Bool) of
        CheckedResult f -> CheckedResult (f True)

Clearly, the innermost case is dead code, because the `Checked` and `Unchecked`
cases are apart.
However, both constructors introduce mutually contradictory coercions `co1` and
`co2` along which GHC generates a type confusion:

  1. (\_ -> True) :: Bool -> Bool
  2. newtype coercion UncheckedResult (\_ -> True) :: Result False (Bool -> Bool)
  3. |> ... sym co1 ... :: Result check (Bool -> Bool)
  4. |> ... co2 ... :: Result True (Bool -> Bool)

Note that we started with a function, injected into `Result` via a newtype
instance and then match on it with a datatype instance.

We have to handle this case gracefully in `cprAnalAlt`, where for the innermost
case we see a `DataAlt` for `CheckedResult`, yet have a scrutinee type that
abstracts the function `(\_ -> True)` with arity 1.
In this case, don't pretend we know anything about the fields of `CheckedResult`!

It was surprising to me that this even type-checks. I suppose the dead code nature is obscured by the need to CSE m ().

Furthermore, it is an absolute mystery to me where that Case alternative comes from.

Well, it was in the original program, and you make it even clearer in your repro case. So no mystery here?

CSE should sort this out. And it does -- but CSE doesn't run before CPR analysis. And in any case CPR should cope with whatever comes.

Great Note.

mentioned in commit b21d4c1a

mentioned in merge request !11717 (closed)

Fix is in !11717 (closed)

mentioned in commit 2a90dd5e

mentioned in commit 7fe95d45

mentioned in commit 49a3e2ad

mentioned in commit 84477c36

mentioned in commit 5a009236

closed with commit 57c391c4

mentioned in commit 57c391c4

mentioned in commit 1405682a

mentioned in commit 69f5714c

mentioned in commit bb0ef5e7

mentioned in commit 5293edd0

mentioned in commit 6a78bcc1

Assertion failure for comfort-array-0.5.2.3 with GHC 9.4

Child items ...

Activity