Skip to content

Commit

Permalink
Don't look for offsets from constants
Browse files Browse the repository at this point in the history
This introduces an infinite loop with the solver pipeline.
i.e. when we have:

[G] x :: KnownNat 10
[W] KnownNat 4

we would produce

solved: x - y :: KnownNat 4
New wanted: y :: KnownNat 6

Then we would go to:

[G] x :: KnownNat 10
[W] KnownNat 6

and solve as:

solved: x - y :: KnownNat 6
new wanted: y :: KnownNat 4

And cycle....

Found when upgrading https://github.com/bittide/bittide-hardware/
to GHC 9.4. But it's hard to create a small reproducer, so there is
no regression test.
  • Loading branch information
christiaanb committed Mar 21, 2024
1 parent 8277741 commit 9397e75
Show file tree
Hide file tree
Showing 4 changed files with 6 additions and 1 deletion.
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
# Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package

## 0.7.11
* Fix infinite loop between plugin and solver pipeline

## 0.7.10 *November 14th 2023*
* Work around [GHC issue 23109](https://gitlab.haskell.org/ghc/ghc/-/issues/23109)

Expand Down
2 changes: 1 addition & 1 deletion ghc-typelits-knownnat.cabal
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
name: ghc-typelits-knownnat
version: 0.7.10
version: 0.7.11
synopsis: Derive KnownNat constraints from other KnownNat constraints
description:
A type checker plugin for GHC that can derive \"complex\" @KnownNat@
Expand Down
1 change: 1 addition & 0 deletions src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
Original file line number Diff line number Diff line change
Expand Up @@ -493,6 +493,7 @@ constraintToEvTerm defs givens (ct,cls,op,orig) = do
-- Find a known constraint for a wanted, so that (modulo normalization)
-- the two are a constant offset apart.
offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))
offset LitTy{} = pure Nothing
offset want = runMaybeT $ do
let -- Get the knownnat contraints
unKn ty' = case classifyPredType ty' of
Expand Down
1 change: 1 addition & 0 deletions src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
Original file line number Diff line number Diff line change
Expand Up @@ -579,6 +579,7 @@ constraintToEvTerm defs givens (ct,cls,op,orig) = do
-- Find a known constraint for a wanted, so that (modulo normalization)
-- the two are a constant offset apart.
offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))
offset LitTy{} = pure Nothing
offset want = runMaybeT $ do
let -- Get the knownnat contraints
unKn ty' = case classifyPredType ty' of
Expand Down

0 comments on commit 9397e75

Please sign in to comment.