Skip to content

Commit

Permalink
Don't look for offsets from constants (#49)
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 authored Mar 26, 2024
1 parent 8277741 commit 30b72d5
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 30b72d5

Please sign in to comment.