ghc-typelits-natnormalise

ghc-typelits-natnormalise copied to clipboard

Possible unsoundness (the plugin seems to claim that 77 ~ 0)

2

The issue and the repro are described around this comment in the GHC bug tracker: https://gitlab.haskell.org/ghc/ghc/-/issues/23923#note_536386 I'm cloning it here in hopes that perhaps here it'd be easier for the...

Mikolaj

Soundness violation around subtraction

1

```hs {- cabal: build-depends: base, ghc-typelits-natnormalise -} {-# LANGUAGE AllowAmbiguousTypes, DataKinds, ExplicitForAll, TypeApplications, TypeFamilies, TypeOperators #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} import Data.Type.Equality import GHC.TypeNats urk :: False :~: True...

mniip

`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1

6

This ticket is moved here from https://gitlab.haskell.org/ghc/ghc/-/issues/23763. Repro with GHC 9.8.1-alpha1 and head.hackage (http://ghc.gitlab.haskell.org/head.hackage/): * clone https://github.com/Mikolaj/horde-ad/commit/e76ff6c2f2b1fc53a00c6b78f74cb1ab8b94790d * `cabal build` * you get ``` src/HordeAd/Core/AstSimplify.hs:1192:9: error: [GHC-64725] • Cannot satisfy:...

Mikolaj

The plugin can't solve: `Expected: ShapeInt (((m6 + k1) + n14) + (n + k3)) Actual: ShapeInt ((((m6 + k1) + n14) + n) + k3)`. A longer fragment of...

Mikolaj

"Could not deduce ... from the context ...", but if the context removed, deduced outright

1

I don't know if this is related to #65. Tested with ghc-9.4.3 and ghc-9.0.2 and with newest plugin in both cases. This snippet of larger code ``` build1VectorizeIndexVar :: forall...

Mikolaj

Could not deduce n~0 from the context n<=0

4

Since we're dealing with natural numbers, which are by definition non-negative, we must be able to conclude `n~0` from `n

int-index

The constraint 0 < d+1 does not seem to resolve?

3

In the following little code snippet I have to functions, function "libFunc", which has a constraint i < d for two Typelits (e.g. indexing with an index i into some...

noinia

Using intermediate type variables prevents deducing (1 <= 2^n)

2

Using an intermediate type variable in your function and binding it to ` 2^n` prevents the deduction that it is greater or equal to 1. This reproducer: ```Haskell {-# LANGUAGE...

lmbollen

Regression when solving inequalities

2

https://github.com/clash-lang/ghc-typelits-natnormalise/commit/2414721729a1f49dc4f7391433771138eeddd48d introduces a regression. I don't have a small reproducer but this is essentially what happens: If we have the following givens: fsk_akFr + fsk_akEb ~ fsk_akFt fsk_akDn - 1...

rowanG077

Could not deduce: (n0 + 1) ~ m from the context: 1 <= m

3

The code below: ```Haskell {- OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -} import Clash.Prelude f :: forall n m. m ~ (n + 1) => Vec m Bool -> Bool f = undefined...

adamwalker