Skip to content

Substitution invariant failure arising from OptCoercion

When built with a debugging compiler, the following snippet fails because of the substitution invariant.

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UndecidableInstances #-}
module StoreBug () where

import Data.Foldable (foldl')
import Data.Proxy
import Data.Word
import Foreign.Storable (Storable, sizeOf)
import GHC.Generics
import GHC.Types (Int(..))
import GHC.TypeLits

newtype Type = VarT Name
  deriving Generic

data Name = Name OccName NameFlavour
  deriving Generic

data NameFlavour
   = NameS
   | NameQ ModName
   | NameU !Int
   | NameL !Int
   | NameG PkgName ModName
   deriving Generic

newtype ModName = ModName String
  deriving Generic

newtype PkgName = PkgName String
  deriving Generic

newtype OccName = OccName String
  deriving Generic

instance Store Type
instance Store Name
instance Store NameFlavour
instance Store ModName
instance Store OccName
instance Store PkgName

instance Store Char where
  {-# INLINE size #-}
  size = sizeStorableTy "Foreign.Storable.Storable GHC.Types.Char"

instance Store Int where
  {-# INLINE size #-}
  size = undefined

instance Store a => Store [a] where
    size = sizeSequence
    {-# INLINE size #-}

sizeSequence :: forall a. Store a => Size [a]
sizeSequence = VarSize $ \t ->
    case size :: Size a of
        ConstSize n -> n * (length t) + sizeOf (undefined :: Int)
        VarSize f -> foldl' (\acc x -> acc + f x) (sizeOf (undefined :: Int)) t
{-# INLINE sizeSequence #-}

class Store a where
    size :: Size a

    default size :: (Generic a, GStoreSize (Rep a)) => Size a
    size = genericSize
    {-# INLINE size #-}

data Size a
    = VarSize (a -> Int)
    | ConstSize !Int

getSizeWith :: Size a -> a -> Int
getSizeWith (VarSize f) x = f x
getSizeWith (ConstSize n) _ = n
{-# INLINE getSizeWith #-}

contramapSize :: (a -> b) -> Size b -> Size a
contramapSize f (VarSize g) = VarSize (g . f)
contramapSize _ (ConstSize n) = ConstSize n
{-# INLINE contramapSize #-}

combineSizeWith :: forall a b c. (c -> a) -> (c -> b) -> Size a -> Size b -> Size c
combineSizeWith toA toB sizeA sizeB =
    case (sizeA, sizeB) of
        (VarSize f, VarSize g) -> VarSize (\x -> f (toA x) + g (toB x))
        (VarSize f, ConstSize m) -> VarSize (\x -> f (toA x) + m)
        (ConstSize n, VarSize g) -> VarSize (\x -> n + g (toB x))
        (ConstSize n, ConstSize m) -> ConstSize (n + m)
{-# INLINE combineSizeWith #-}

sizeStorableTy :: forall a. Storable a => String -> Size a
sizeStorableTy ty = ConstSize (sizeOf (error msg :: a))
  where
    msg = "In Data.Store.storableSize: " ++ ty ++ "'s sizeOf evaluated its argument."
{-# INLINE sizeStorableTy #-}

genericSize :: (Generic a, GStoreSize (Rep a)) => Size a
genericSize = contramapSize from gsize
{-# INLINE genericSize #-}

type family SumArity (a :: * -> *) :: Nat where
    SumArity (C1 c a) = 1
    SumArity (x :+: y) = SumArity x + SumArity y

class GStoreSize f where gsize :: Size (f a)

instance GStoreSize f => GStoreSize (M1 i c f) where
    gsize = contramapSize unM1 gsize
    {-# INLINE gsize #-}

instance Store a => GStoreSize (K1 i a) where
    gsize = contramapSize unK1 size
    {-# INLINE gsize #-}

instance GStoreSize U1 where
    gsize = ConstSize 0
    {-# INLINE gsize #-}

instance GStoreSize V1 where
    gsize = ConstSize 0
    {-# INLINE gsize #-}

instance (GStoreSize a, GStoreSize b) => GStoreSize (a :*: b) where
    gsize = combineSizeWith (\(x :*: _) -> x) (\(_ :*: y) -> y) gsize gsize
    {-# INLINE gsize #-}

instance (SumArity (a :+: b) <= 255, GStoreSizeSum 0 (a :+: b))
         => GStoreSize (a :+: b) where
    gsize = VarSize $ \x -> sizeOf (undefined :: Word8) + gsizeSum x (Proxy :: Proxy 0)
    {-# INLINE gsize #-}

class KnownNat n => GStoreSizeSum (n :: Nat) (f :: * -> *) where gsizeSum :: f a -> Proxy n -> Int

instance (GStoreSizeSum n a, GStoreSizeSum (n + SumArity a) b, KnownNat n)
         => GStoreSizeSum n (a :+: b) where
    gsizeSum (L1 l) _ = gsizeSum l (Proxy :: Proxy n)
    gsizeSum (R1 r) _ = gsizeSum r (Proxy :: Proxy (n + SumArity a))
    {-# INLINE gsizeSum #-}

instance (GStoreSize a, KnownNat n) => GStoreSizeSum n (C1 c a) where
    gsizeSum x _ = getSizeWith gsize x
    {-# INLINE gsizeSum #-}

The assertion failure is

$ ~/Software/ghc5/inplace/bin/ghc-stage2 -fforce-recomp -O2 StoreBug.hs
[1 of 1] Compiling StoreBug         ( StoreBug.hs, StoreBug.o )
WARNING: file compiler/simplCore/SimplCore.hs, line 666
  Simplifier bailing out after 4 iterations [3866, 755, 220, 8]
    Size = {terms: 1,490, types: 7,176, coercions: 4,808}
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20170121 for x86_64-unknown-linux):
        ASSERT failed!
  in_scope InScope {wild_00 wild_X25 g1_a33l g2_a33m $cfrom_a47d
                    $cto_a47F $cfrom_a48a $cto_a48C $cfrom_a496 $cto_a4bk $cfrom_a4dA
                    $cto_a4e2 $cfrom_a4ew $cto_a4fb $cfrom_a4fS $cto_a4gk
                    $cp1GStoreSizeSum_a4gV $cgsizeSum_a4gX $cp1GStoreSizeSum_a4hh
                    $cgsizeSum_a4hj $cgsize_a4hV $cgsize_a4ix $csize_a4iU $csize_a4j2
                    $csize_a4jb $csize_a4jj $csize_a4jw $csize_a4jJ $csize_a4jW
                    $csize_a4k9 $csize_a4km $cgsize_a4kD $cgsize_a4kY $cgsize_a4l6
                    $cgsize_a4li $dGStoreSize_a4qQ $dGStoreSize_a4qW $dGStoreSize_a4r2
                    $dGStoreSize_a4r8 $dGStoreSize_a4BJ $dGStoreSize_a4BS ww2_a5CX
                    sizeSequence genericSize $tc'ModName $tcModName $tc'PkgName
                    $tcPkgName $tc'NameS $tc'NameQ $tc'NameU $tc'NameL $tc'NameG
                    $tcNameFlavour $tc'OccName $tcOccName $tc'Name $tcName $tc'VarT
                    $tcType $tc'VarSize $tc'ConstSize $tcSize $tcGStoreSize
                    $tc'C:GStoreSize $fGStoreSize:*: $fGStoreSizeV1 $fGStoreSizeU1
                    $fGStoreSizeM1 $tcStore $dmsize $tc'C:Store $fGStoreSizeK1
                    $fStore[] $fStoreInt $fStoreChar $fStorePkgName $fStoreOccName
                    $fStoreModName $fStoreNameFlavour $fStoreName $fStoreType
                    $tcGStoreSizeSum $tc'C:GStoreSizeSum $fGStoreSizeSumnM1
                    $fGStoreSizeSumn:+: $fGStoreSize:+: $fGenericModName
                    $fGenericPkgName $fGenericNameFlavour $fGenericOccName
                    $fGenericName $fGenericType $trModule $cto_s4Pr $cfrom_s4Ps
                    $cfrom_s4Pv $cto_s4Pw $cfrom_s4Px $cfrom_s4PF $cto_s4PG $cfrom_s4PH
                    $cto_s4PI $cfrom_s4PJ $trModule_s50k $trModule_s50l $trModule_s50m
                    $trModule_s50n $tc'ModName_s50o $tc'ModName_s50p $tcModName_s50q
                    $tcModName_s50r $tc'PkgName_s50s $tc'PkgName_s50t $tcPkgName_s50u
                    $tcPkgName_s50v $tc'NameG_s50w $tc'NameG_s50x $tc'NameL_s50y
                    $tc'NameL_s50z $tc'NameU_s50A $tc'NameU_s50B $tc'NameQ_s50C
                    $tc'NameQ_s50D $tc'NameS_s50E $tc'NameS_s50F $tcNameFlavour_s50G
                    $tcNameFlavour_s50H $tc'OccName_s50I $tc'OccName_s50J
                    $tcOccName_s50K $tcOccName_s50L $tc'Name_s50M $tc'Name_s50N
                    $tcName_s50O $tcName_s50P $tc'VarT_s50Q $tc'VarT_s50R $tcType_s50S
                    $tcType_s50T $tc'ConstSize_s50U $tc'ConstSize_s50V $tc'VarSize_s50W
                    $tc'VarSize_s50X $tcSize_s50Y $tcSize_s50Z $tc'C:GStoreSize_s510
                    $tc'C:GStoreSize_s511 $tcGStoreSize_s512 $tcGStoreSize_s513
                    $tc'C:Store_s514 $tc'C:Store_s515 $tcStore_s516 $tcStore_s517
                    $tc'C:GStoreSizeSum_s518 $tc'C:GStoreSizeSum_s519
                    $tcGStoreSizeSum_s51a $tcGStoreSizeSum_s51b $sgenericSize_s59c
                    $sgenericSize_s59f $sgenericSize_s59i $sgenericSize_s59l
                    $sgenericSize_s59o $sgenericSize_s59r $sgsize_s59B $sgsize_s59D
                    $sgsize_s59F $sgsize_s59H $sgsize_s59J $sgsize_s59L lvl_s5bw
                    lvl_s5bx $csize_s5i3 $dGStoreSize_s5jy $dGStoreSize_s5jM
                    $dGStoreSize_s5k0 $dGStoreSize_s5kc $dGStoreSize_s5lQ
                    $dGStoreSize_s5od $dGStoreSize_s5rC g_s5tx g_s5tA g_s5tD
                    $dGStoreSize_s5u4 g_s5u5 $dGStoreSize_s5uv $dGStoreSize_s5uZ
                    $sgenericSize_s5v0 $csize_s5v2 g_s5vy $sgenericSize_s5vA
                    $csize_s5vF $w$j_s5Wr a_s5Ws ww_s5Ww ww_s5Wx $wg_s5WC
                    $w$dGStoreSize_s5WI $wg_s5WT lvl_s65L lvl_s65M lvl_s65N lvl_s65O
                    lvl_s65P lvl_s65Q lvl_s65R lvl_s65S lvl_s65T lvl_s65U lvl_s65W
                    lvl_s65X lvl_s65Y lvl_s65Z lvl_s660 lvl_s661 lvl_s662 lvl_s663
                    lvl_s664 lvl_s665 lvl_s666 lvl_s667 lvl_s66c lvl_s66d lvl_s66e
                    lvl_s66f lvl_s66g lvl_s66h lvl_s66i lvl_s66j lvl_s66k lvl_s66l
                    lvl_s66m lvl_s66n lvl_s66s lvl_s66t lvl_s66u lvl_s66v lvl_s66w
                    lvl_s66x lvl_s66y lvl_s66z lvl_s66A lvl_s66B lvl_s66C lvl_s66D
                    lvl_s66I lvl_s66J lvl_s66K lvl_s66L $s$w$j_s69S $s$w$j_s69T
                    $s$w$j_s69U}
  tenv []
  tenvFVs []
  cenv [s69R :-> sg_s69R]
  cenvFVs [s69R :-> sg_s69R]
  tys [R]
  cos []
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1166:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1215:22 in ghc:Outputable
        assertPprPanic, called at compiler/types/TyCoRep.hs:2078:56 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:2111:17 in ghc:TyCoRep
        substTy, called at compiler/types/OptCoercion.hs:345:12 in ghc:OptCoercion
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1166:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1170:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1213:5 in ghc:Outputable
        assertPprPanic, called at compiler/types/TyCoRep.hs:2078:56 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:2111:17 in ghc:TyCoRep
        substTy, called at compiler/types/OptCoercion.hs:345:12 in ghc:OptCoercion
Edited by Matthew Pickering
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information