Specialiser creates specialisation assuming local equality
Carrying on from #23109
I have extracted a reproducer for that issue which doesn't depend on anything in horde-ad so it's much simpler. It still needs to depend on the plugins though but I suspect that the plugin dependencies can also be removed.
https://github.com/mpickering/crispy-computing-machine
If you compile with ghc-9.6.1 you get
32
repro: Bad runtime result
CallStack (from HasCallStack):
error, called at Main.hs:11:57 in main:Main
The problem is along the lines of:
- In the call to
specwe specialisetbuild'for@33and@0. - In the body of
$stbuild'(in the recursive call to the specialiser), in the binding ofbuildSh, there is a call totypeRep (Proxy @ix), the specialiser creates a bogus specialisation here.
"SPEC/TestHighRankSimplified typeNatTypeRep @_"
forall (@(ipv_i1oF :: GHC.TypeNats.Nat))
($dKnownNat_s1HG :: GHC.TypeNats.KnownNat ipv_i1oF).
base:Data.Typeable.Internal.typeNatTypeRep @ipv_i1oF
$dKnownNat_s1HG
= $stypeNatTypeRep_s1HJ @ipv_i1oF- Then
spec3rewrites using this specialisation giving a bogus result.
Perhaps someone can help either removing the dependency on the plugins or further minimising it.
Relates to
Activity
mentioned in issue #23109
assigned to @mpickering
You can replace
Main.hswith the following{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} module Main where import GHC.TypeNats import Type.Reflection m :: (KnownNat 10, k + 1 ~ 10) => TypeRep k m = typeRep spec :: TypeRep 9 spec = m main :: IO () main = print (typeRep @3)This prints 9 while it should print 3.
Edited by Krzysztof GogolewskiGreat minimisation work @mpickering and @monoidal! CC @christiaanb
This seems to be the crucial step:
tcPluginSolve start ghc-typelits-knownnat given = [[G] $d~_a18a {0}:: 10 ~ 10 (CDictCan), [G] $dKnownNat_a17O {0}:: KnownNat 10 (CDictCan), [G] co_a189 {0}:: (k_a17N[sk:1] + 1) ghc-prim:GHC.Prim.~# 10 (CEqCan)] wanted = [[W] $dKnownNat_a18b {1}:: KnownNat k_a17N[sk:1] (CDictCan)] tcPluginSolve ok ghc-typelits-knownnat solved = [((GHC.TypeLits.KnownNat.$fKnownNat2"GHC.TypeNats.-"ab @(k_a17N[sk:1] + 1) @1 $dKnownNat_a199 $dKnownNat_a19a $d~_a19b) `cast` (GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <k_a17N[sk:1] + 1>_N <1>_N ; GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (GHC.TypeNats.N:KnownNat[0] <k_a17N[sk:1]>_N ; GHC.TypeNats.N:SNat[0] <k_a17N[sk:1]>_P) :: GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.-" (k_a17N[sk:1] + 1) 1 ~R# KnownNat k_a17N[sk:1]), [W] $dKnownNat_a18b {1}:: KnownNat k_a17N[sk:1] (CDictCan))] new = [[W] $dKnownNat_a199 {1}:: KnownNat (k_a17N[sk:1] + 1) (CNonCanonical), [W] $dKnownNat_a19a {1}:: KnownNat 1 (CNonCanonical), [W] $d~_a19b {1}:: (1 <= (k_a17N[sk:1] + 1)) ~ (() :: Constraint) (CNonCanonical)]So the plugin has
[G] co_a189 :: (k_a17N + 1) ~# 10 [W] $dKnownNat_a18b :: KnownNat k_a17Nand it proceeds to emit new wanteds
[W] $dKnownNat_a199 :: KnownNat (k_a17N + 1) [W] $dKnownNat_a19a :: KnownNat 1 [W] $d~_a19b :: (1 <= (k_a17N + 1)) ~ (() :: Constraint)and solve the original wanted with an expression that depends on the three new dictionaries, but not
co_a189. And that is unsound, because the optimiser can then float the solution toKnownNat k_a17Npast the (unused) given and use it as a specialisation for arbitraryKnownNats. So we end up withmdiscarding the evidence fork_a17N + 1 ~ 10:Main.$stypeNatTypeRep :: forall {k :: Natural}. TypeRep k -- obviously bogus! Main.$stypeNatTypeRep = ... -- piles of stuff that is effectively `show 9` m :: forall (k :: Natural). (KnownNat 10, (k + 1) ~ 10) => TypeRep k m = \ (@(k_a17N :: Natural)) _ [Occ=Dead] ($d~_a17P :: (k_a17N + 1) ~ 10) -> case ghc-prim:GHC.Types.eq_sel @Natural @(k_a17N + 1) @10 $d~_a17P of co_a189 [Dmd=A] { __DEFAULT -> Main.$stypeNatTypeRep @k_a17N } Main.main3 = base:Data.Typeable.Internal.$fShowSomeTypeRep_$sshowTypeable @Natural @3 0# (Main.$stypeNatTypeRep @3)But solving
[W] $dKnownNat_k :: KnownNat kusing$dKnownNat_k1 :: KnownNat (k + 1)alone is fine; it doesn't need any Givens.The question is then how we solve
$dKnownNat_k1 :: KnownNat (k + 1); it seems GHC does that on its own by usingco :: (k + 1) ~# 10;KnownNat co :: KnownNat (k + 1) ~ KnownNat 10. I'm seeing:$dKnownNat_k1 :: KnownNat (k + 1) = ($dKnownNat_10 :: KnownNat 10) `cast` (Sub (Sym (KnownNat co))which seems fine as well.
Alright, I now have got a hacked together version of the plugin that generates the following instead:
tcPluginSolve start ghc-typelits-knownnat given = [[G] $d~_a18h {0}:: 10 ~ 10 (CDictCan), [G] $dKnownNat_a17V {0}:: KnownNat 10 (CDictCan), [G] co_a18g {0}:: (k_a17U[sk:1] + 1) GHC.Prim.~# 10 (CEqCan)] wanted = [[W] $dKnownNat_a18i {1}:: KnownNat k_a17U[sk:1] (CDictCan)] tcPluginSolve ok ghc-typelits-knownnat solved = [((GHC.TypeLits.KnownNat.$fKnownNat2"GHC.TypeNats.-"ab @10 @1 $dKnownNat_a17V $dKnownNat_a19g $d~_a19h) `cast` (GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <10>_N <1>_N ; GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (GHC.TypeNats.N:KnownNat[0] <10 - 1>_N ; GHC.TypeNats.N:SNat[0] <10 - 1>_P) ; Sym (KnownNat (co_a18g - <1>_N)_N)_R ; Univ(representational plugin "ghc-typelits-knownnat" :: KnownNat ((k_a17U[sk:1] + 1) - 1), KnownNat k_a17U[sk:1]) :: GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.-" 10 1 ~R# KnownNat k_a17U[sk:1]), [W] $dKnownNat_a18i {1}:: KnownNat k_a17U[sk:1] (CDictCan))] new = [[W] $dKnownNat_a19g {1}:: KnownNat 1 (CNonCanonical), [W] $d~_a19h {1}:: (1 <= 10) ~ (() :: Constraint) (CNonCanonical)]As a result we only have valid specialisations:
------ Local rules for imported ids -------- "SPEC/Main typeNatTypeRep @3" forall ($dKnownNat_X1E :: KnownNat 3). base:Data.Typeable.Internal.typeNatTypeRep @3 $dKnownNat_X1E = Main.$stypeNatTypeRep "SPEC/Main typeNatTypeRep @9" forall ($dKnownNat_s1Xk :: KnownNat 9). base:Data.Typeable.Internal.typeNatTypeRep @9 $dKnownNat_s1Xk = specand
mlooks like this after simplification:m = \ (@(k_a17U :: Natural)) ($dKnownNat_a17V :: KnownNat 10) ($d~_a17W :: (k_a17U + 1) ~ 10) -> case GHC.Types.eq_sel @Natural @(k_a17U + 1) @10 $d~_a17W of co_a18g { __DEFAULT -> base:Data.Typeable.Internal.typeNatTypeRep @k_a17U ((GHC.Num.Natural.naturalSubThrow ($dKnownNat_a17V `cast` (GHC.TypeNats.N:KnownNat[0] <10>_N ; GHC.TypeNats.N:SNat[0] <10>_P :: KnownNat 10 ~R# Natural)) Main.m1) `cast` (Sym (GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P) ; Sym (GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <10>_N <1>_N) ; GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <10>_N <1>_N ; GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (GHC.TypeNats.N:KnownNat[0] <10 - 1>_N ; GHC.TypeNats.N:SNat[0] <10 - 1>_P) ; Sym (KnownNat (co_a18g - <1>_N)_N)_R ; Univ(representational plugin "ghc-typelits-knownnat" :: KnownNat ((k_a17U + 1) - 1), KnownNat k_a17U) :: Natural ~R# KnownNat k_a17U)) }And as we can see from the occurance of
GHC.Num.Natural.naturalSubThrow, the followinginstance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b)) {-# INLINE natSing2 #-}was allowed to keep its
INLINEpragma without breaking things.Next step will be to clean it all up and see whether it also works for original test case in #23109
However, @mpickering has a gnawing suspicion this can be reproduced without the plugin.
Oh, I missed the fact that the remaining plugin is the less complex one: GHC.TypeLits.KnownNat.Solver.
Splendid job minimizing indeed, @monoidal.
Who would have thought that the smaller plugin is to blame.
It seems the simplifier transforms
-- -ddump-ds m :: forall (k :: Nat). ((k + 1) ~ 10) => TypeRep k m = \ @k $d~ -> case eq_sel $d~ of co -> typeRep @Nat @k $ typeNatTypeRep @k $ GHC.TypeLits.KnownNat.$fKnownNat2"GHC.TypeNats.-"ab @(k+1) @1 ($dKnownNat10 |> Sub (Sym (KnownNat co)) :: KnownNat 10 ~R# KnownNat (k+1)) (NS 1## |> axiom_co1 :: Natural ~R# KnownNat 1)into
-- result of first pass in -dverbose-core2core m :: forall (k :: Nat). ((k + 1) ~ 10) => TypeRep k m = \ @k $d~ -> case eq_sel $d~ of co -> typeRep @Nat @k $ typeNatTypeRep @k (NS 9## |> axiom_co2 :: Natural ~R# KnownNat k)Here
axiom_co{1,2}are compositions of things like newtype axioms, and don't mention any coercion variables.This means that
cois no longer mentioned in the body, and we're in trouble.Edited by sheafSo changing the plugin like this is a work-around for the issue, and sufficient to make the original test case in #23109 pass.
diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs index 0fbe8fc..814245e 100644 --- a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs +++ b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs @@ -193,7 +193,7 @@ instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-' instance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b)) - {-# INLINE natSing2 #-} + {-# NOINLINE natSing2 #-} instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))As it prevents the transformation which drops the
co
simplExprF in_expr: \ (@(a_a1iu :: Nat)) (@(b_a1iv :: Nat)) ($dKnownNat_a1iw [Occ=Once1] :: KnownNat a_a1iu) ($dKnownNat1_a1ix [Occ=Once1] :: KnownNat b_a1iv) -> naturalSubThrow ($dKnownNat_a1iw `cast` (N:KnownNat[0] <a_a1iu>_N ; N:SNat[0] <a_a1iu>_P :: (KnownNat a_a1iu :: Constraint) ~R# (Natural :: Type))) ($dKnownNat1_a1ix `cast` (N:KnownNat[0] <b_a1iv>_N ; N:SNat[0] <b_a1iv>_P :: (KnownNat b_a1iv :: Constraint) ~R# (Natural :: Type))) cont: ApplyToTy (k_a16J + 1) ApplyToTy 1 ApplyToVal nodup hole (KnownNat (k_a16J + 1), KnownNat 1, ((<=) @{Nat} 1 (k_a16J + 1) :: Constraint) ~ (() :: Constraint :: Constraint)) => Natural ($dKnownNat_a16U `cast` (Sub (Sym (KnownNat co_a177)_N) :: (KnownNat 10 :: Constraint) ~R# (KnownNat (k_a16J + 1) :: Constraint))) ApplyToVal nodup hole (KnownNat 1, ((<=) @{Nat} 1 (k_a16J + 1) :: Constraint) ~ (() :: Constraint :: Constraint)) => Natural ((NS 1##) `cast` (Sym (N:KnownNat[0] <1>_N ; N:SNat[0] <1>_N) :: (Natural :: Type) ~R# (KnownNat 1 :: Constraint))) CastIt (Sym (N:SNatKn[0] <"GHC.TypeNats.-">_P) ; Sym (N:KnownNat2[0] <"GHC.TypeNats.-">_N <k_a16J + 1>_N <1>_N) ; N:KnownNat2[0] <"GHC.TypeNats.-">_N <k_a16J + 1>_N <1>_N ; N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (N:KnownNat[0] <k_a16J>_N ; N:SNat[0] <k_a16J>_N) :: (Natural :: Type) ~R# (KnownNat k_a16J :: Constraint)) Stop[BoringCtxt] KnownNat k_a16J out_expr: (NS 9##) `cast` (Sym (N:SNatKn[0] <"GHC.TypeNats.-">_P) ; Sym (N:KnownNat2[0] <"GHC.TypeNats.-">_N <k_a16J + 1>_N <1>_N) ; N:KnownNat2[0] <"GHC.TypeNats.-">_N <k_a16J + 1>_N <1>_N ; N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (N:KnownNat[0] <k_a16J>_N ; N:SNat[0] <k_a16J>_N) :: (Natural :: Type) ~R# (KnownNat k_a16J :: Constraint))The phantom roles are definitely wrong, per #23454 (closed), but even with a nominal role we still have
KnownNat k ~R SNat k ~R Naturaland that seems to be enough.
https://github.com/clash-lang/ghc-typelits-knownnat/pull/45 fixes this issue by generating the correct evidence:
tcPluginSolve start ghc-typelits-knownnat given = [[G] $d~_a17T {0}:: 10 ~ 10 (CDictCan), [G] $dKnownNat_a17x {0}:: KnownNat 10 (CDictCan), [G] co_a17S {0}:: (k_a17w[sk:1] + 1) GHC.Prim.~# 10 (CEqCan)] wanted = [[W] $dKnownNat_a17U {1}:: KnownNat k_a17w[sk:1] (CDictCan)] tcPluginSolve ok ghc-typelits-knownnat solved = [((GHC.TypeLits.KnownNat.$fKnownNat2"GHC.TypeNats.-"ab @10 @1 $dKnownNat_a17x $dKnownNat_a18S $d~_a18T) `cast` (GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <10>_N <1>_N ; GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (GHC.TypeNats.N:KnownNat[0] <10 - 1>_N ; GHC.TypeNats.N:SNat[0] <10 - 1>_P) ; (KnownNat (Sym co_a17S - <1>_N)_N)_R ; Univ(representational plugin "ghc-typelits-knownnat" :: KnownNat ((k_a17w[sk:1] + 1) - 1), KnownNat k_a17w[sk:1]) :: GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.-" 10 1 ~R# KnownNat k_a17w[sk:1]), [W] $dKnownNat_a17U {1}:: KnownNat k_a17w[sk:1] (CDictCan))] new = [[W] $dKnownNat_a18S {1}:: KnownNat 1 (CNonCanonical), [W] $d~_a18T {1}:: (1 <= 10) ~ (() :: Constraint) (CNonCanonical)]The simplifier output also looks good:
-- RHS size: {terms: 11, types: 22, coercions: 50, joins: 0/0} m :: forall (k :: Natural). (KnownNat 10, (k + 1) ~ 10) => TypeRep k [GblId, Arity=2, Str=<ML><1P(1L)>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [0 30] 80 0}] m = \ (@(k_a17w :: Natural)) ($dKnownNat_a17x :: KnownNat 10) ($d~_a17y :: (k_a17w + 1) ~ 10) -> case GHC.Types.eq_sel @Natural @(k_a17w + 1) @10 $d~_a17y of co_a17S { __DEFAULT -> base:Data.Typeable.Internal.typeNatTypeRep @k_a17w ((GHC.Num.Natural.naturalSubThrow ($dKnownNat_a17x `cast` (GHC.TypeNats.N:KnownNat[0] <10>_N ; GHC.TypeNats.N:SNat[0] <10>_P :: KnownNat 10 ~R# Natural)) Main.m1) `cast` (Sym (GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P) ; Sym (GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <10>_N <1>_N) ; GHC.TypeLits.KnownNat.N:KnownNat2[0] <"GHC.TypeNats.-">_N <10>_N <1>_N ; GHC.TypeLits.KnownNat.N:SNatKn[0] <"GHC.TypeNats.-">_P ; Sym (GHC.TypeNats.N:KnownNat[0] <10 - 1>_N ; GHC.TypeNats.N:SNat[0] <10 - 1>_P) ; (KnownNat (Sym co_a17S - <1>_N)_N)_R ; Univ(representational plugin "ghc-typelits-knownnat" :: KnownNat ((k_a17w + 1) - 1), KnownNat k_a17w) :: Natural ~R# KnownNat k_a17w)) } ------ Local rules for imported ids -------- "SPEC/Main typeNatTypeRep @3" forall ($dKnownNat_X1E :: KnownNat 3). base:Data.Typeable.Internal.typeNatTypeRep @3 $dKnownNat_X1E = Main.$stypeNatTypeRep "SPEC/Main typeNatTypeRep @9" forall ($dKnownNat_s1WY :: KnownNat 9). base:Data.Typeable.Internal.typeNatTypeRep @9 $dKnownNat_s1WY = specSadly, the original test in #23109 still fails, so that will require further investigation.
@christiaanb points out that the bad specialisation looks like:
"SPEC/TestHighRankSimplified $w$ctbuild2 @'ADModeGradient @(ipv + 0)" [2] forall ($d(%,,,,,,,,,,,,,,%)_s59x :: ADModeAndNum ADModeGradient Double) (@(ipv_a589 :: Nat)) (eta_s59y :: KnownNat (ipv_a589 + 0)). HordeAd.Core.ADValTensor.$w$ctbuild2 @ADModeGradient $d(%,,,,,,,,,,,,,,%)_s59x @(ipv_a589 + 0) eta_s59y = $s$w$ctbuild2_s5ax @ipv_a589I am minimising now.
mentioned in issue #23478 (closed)
marked this issue as related to #23109
-
@monoidal I put up my progress here https://github.com/mpickering/horde-ad/tree/wip/minimised
If you run
cabal --store-dir=$PWD/store test simplifiedOnlyTest --test-options='-p 3concatBuild' --allow-newer --enable-optimization --ghc-options=''then you can look at the
dump-specfile and search for "Local" and find this specialisation which looks bad to me."SPEC/TestHighRankSimplified $fTensorADVal_$stbuild1R @(ipv + 0)" forall (@(ipv_ivrb :: Nat)) ($dKnownNat_svsT :: KnownNat (ipv_ivrb + 0)). HordeAd.Core.ADValTensor.$fTensorADVal_$stbuild1R @(ipv_ivrb + 0) $dKnownNat_svsT = $s$fTensorADVal_$stbuild1R_svsY @ipv_ivrb I am getting compilation errors:
test/SimplifiedOnlyTest.hs:21:60: error: [GHC-76037] Not in scope: type constructor or class ‘EqEpsilon’ | 21 | ingredients = includingOptions [Option (Proxy :: Proxy EqEpsilon)] | ^^^^^^^^^ test/SimplifiedOnlyTest.hs:25:3: error: [GHC-76037] Not in scope: ‘TestHighRankSimplified.testTrees’ NB: the module ‘TestHighRankSimplified’ does not export ‘testTrees’. Suggested fix: Perhaps use one of these: ‘TestHighRankSimplified.spec1’ (imported from TestHighRankSimplified), ‘TestHighRankSimplified.spec2’ (imported from TestHighRankSimplified) | 25 | TestHighRankSimplified.testTrees | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@adamgundry and I had a good conversation about this last night. I still have to write it up. But meanwhile I have pushed changes to !10479 that may do the trick.
Can you give that MR a try @mpickering?
Maybe I did something stupid
In fact I did. CI on !10479 is looking promising. Some regressions I need to look into. Plus documenting properly etc
How urgent is this?
How urgent is this?
From the single known affected user's perspective: medium urgent. I can still use GHC 9.2 and 9.4, so I'm not blocked.
Edited by Mikolaj KonarskiFrom the single known affected user's perspective: medium urgent. I can still use GHC 8.2 and 8.4, so I'm not blocked.
A correction: this is now extremely urgent for the said hapless user, because GHC 9.4 stopped being able to compile horde-ad (#23553 (closed))
and GHC 9.2.7 now hangs when running the test suite(and GHCs older tha 9.2 OOM when compiling large constraint lists).Alarmingly, no GHC version can currently compile horde-ad and pass most of its basic 20min testsuite with optimization on (with optimization off it probably OOMs after many hours).Edit2: the cross-out part above and below was (mostly) my fault and is now fixed, so GHC 9.2 is workable, though it produces many spurious warnings due its different (better) handling of Nat exhaustiveness checking.
Edit: and the binary produced with -O0 (but not -O1) in GHC 9.6.2 now consistently hangs in tests and the same with GHC 9.4.5. The affected commit is https://github.com/Mikolaj/horde-ad/commit/f36c90180b663119727c48db271749582188cf10Edited by Mikolaj Konarski
