GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-12-07T20:32:53Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24245Term-reflection of TypeLits/Nats type-families2023-12-07T20:32:53ZOleg GrenrusTerm-reflection of TypeLits/Nats type-familiesNow as there are `SNat`, `SSymbol`, `SChar` in the `base` it has ingredients to also define term-reflections, e.g.
```haskell
(+) :: SNat n -> SNat m -> SNat (n + m) -- or plusSNat
```
E.g. constraints has [`plusNat :: forall n m. (Kno...Now as there are `SNat`, `SSymbol`, `SChar` in the `base` it has ingredients to also define term-reflections, e.g.
```haskell
(+) :: SNat n -> SNat m -> SNat (n + m) -- or plusSNat
```
E.g. constraints has [`plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)`](https://hackage.haskell.org/package/constraints-0.14/docs/Data-Constraint-Nat.html#v:plusNat), which could be *safely* defined using `plusSNat`.
It would be great to constraint the "trusted" source to the `base` (i.e. library defining the magic type-families).
---
The https://gitlab.haskell.org/ghc/ghc/-/issues/23478 issue is related. I cannot defined `plusSNat` without doing `unsafeCoerce` magic outside `base`. But, if `plusSNat` were defined, I'd not care about `SNat` constructor being exported too much (it would be nice, anyway).https://gitlab.haskell.org/ghc/ghc/-/issues/23763`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1:...2023-09-11T13:21:22ZMikolaj Konarski`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1Repro 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/As...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: OS.Rank sh2 <= 1 + OS.Rank sh1
• In the first argument of ‘($)’, namely ‘astTransposeS @zsuccPerm’
In the second argument of ‘($)’, namely
‘astTransposeS @zsuccPerm $ astReplicateS @n v’
In the second argument of ‘($)’, namely
‘trustMeThisIsAPermutation @zsuccPerm
$ astTransposeS @zsuccPerm $ astReplicateS @n v’
|
1192 | $ astTransposeS @zsuccPerm $ astReplicateS @n v
```
It works fine with GHC <= 9.6 and also after patching it in the following way:
https://github.com/Mikolaj/horde-ad/commit/0417f413051f1739fe32cfaf7869755276171449
My guess is that previously GHC could deduce:
OS.Rank zsuccPerm <= 1 + OS.Rank sh1
from (note that `sh2` that GHC invents here in just `zsuccPerm` -- this obfuscation in error messages is already reported in one of my older tickets)
OS.Rank zsuccPerm :~: 1 + OS.Rank perm
and
OS.Rank perm <= OS.Rank sh1
but now it can't.
The issue may be in GHC itself or in how plugin `GHC.TypeLits.Normalise` has been updated to 9.8.1-alpha1, but I doubt the latter, because it's been updated on head.hackage by people that know what they are doing.
I haven't tried with HEAD of the github repo of `GHC.TypeLits.Normalise` and GHC 9.6, but I don't think `GHC.TypeLits.Normalise` has been modified vs the version on Hackage (`GHC.TypeLits.KnownNat.Solver` has been, but it seem unrelated).
CC: @christiaanbhttps://gitlab.haskell.org/ghc/ghc/-/issues/23127Undocumented 9.4 TypeNats breaking change2023-03-21T15:32:31ZBen PriceUndocumented 9.4 TypeNats breaking change## Summary
Location of documentation issue: the GHC user's guide / `base`'s changelog
In GHC 9.4, more specifically https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066, the implementation of (at least) `Data.Type.Ord.(<=)` changed...## Summary
Location of documentation issue: the GHC user's guide / `base`'s changelog
In GHC 9.4, more specifically https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066, the implementation of (at least) `Data.Type.Ord.(<=)` changed so the following code no longer compiles
```haskell
import GHC.TypeNats
newtype A (l :: Nat) (u :: Nat) = Finite ()
class E1 (x :: *) where
instance x <= y => E1 (A x y) where
```
The error is
```
Bug.hs:13:10: error:
• Variables ‘x, y’ occur more often
in the constraint ‘x <= y’ than in the instance head ‘E1 (A x y)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘E1 (A x y)’
|
13 | instance x <= y => E1 (A x y) where
```
Whilst the suggestion to add `UndecidableInstances` works,
- This breakage is undocumented afaict
- The error is really confusing, since it is not obvious that `<=` actually expands into a more complex type synonym
## Proposed improvements or changes
We should document this somewhere. I suggest the user's guide, since that is where I went looking for information about the breakage. However, I don't know if this is reasonable, given that 9.6 has now come out.
## Background
The need for documentation was briefly mentioned in https://gitlab.haskell.org/ghc/ghc/-/issues/21935#note_446169, but appears to have slipped through the cracks.
For reference, GHC 9.2 had
```haskell
type x <= y = (x <=? y) ~ 'True
```
whereas GHC 9.4 had:
```haskell
type x <= y = Assert (x <=? y) (LeErrMsg x y)
```sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21935Implementation of GHC.TypeLits.<= is still not quite right2023-03-21T15:21:25ZChristiaan BaaijImplementation of GHC.TypeLits.<= is still not quite right`base-4.6` (GHC 7.6) introduced:
```haskell
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
where both `<=` and `<=?` had hard-coded resolution rules.
Then in `base-4.7` (GHC ...`base-4.6` (GHC 7.6) introduced:
```haskell
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
where both `<=` and `<=?` had hard-coded resolution rules.
Then in `base-4.7` (GHC 7.8) we got:
```haskell
type x <= y = (x <=? y) ~ True
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
Where only `<=?` had hard-coded resolution rules.
And for a very long time all was right with the world.
Then, in `base-4.16` (GHC 9.2) we suddenly got:
```haskell
type x <= y = (x <=? y) ~ True
type (<=?) :: k -> k -> Bool
type m <=? n = OrdCond (Compare m n) 'True 'True 'False
type OrdCond :: Ordering -> k -> k -> k -> k
type family OrdCond o lt eq gt where
OrdCond 'LT lt eq gt = lt
OrdCond 'EQ lt eq gt = eq
OrdCond 'GT lt eq gt = gt
type Compare :: k -> k -> Ordering
type family Compare a b
type instance Compare (a :: Natural) b = CmpNat a b
type family CmpNat (m :: Natural) (n :: Natural) :: Ordering
```
Where only `CmpNat` has hard-coded resolution rules.
This new implementation of `<=` had error messages of much porer quality than previous implementations, which was reported in #20009.
For the following code:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where
import Data.Proxy
import GHC.TypeLits
proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()
proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
```
we went from this error message in GHC 9.0:
```
$ ghci TestInEq.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
```
to this error message in GHC 9.2:
```
$ ghci TestInEq.hs
GHCi, version 9.2.0.20210422: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘Data.Type.Ord.OrdCond
(CmpNat a (a + 1)) 'True 'True 'False’
with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
```
The quality of the error message was fixed in !6066, which is currently included to be part of the GHC 9.4.1 release.
In !6066 the implementation of `<=` was changed to:
```haskell
type x <= y = Assert (x <=? y) (LeErrMsg x y)
type LeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " <= " ':<>: 'ShowType y)
type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
Assert 'True _ = ()
Assert _ errMsg = errMsg
```
which would create error messages of the following shape instead:
```
• Cannot satisfy: a <= a + 1
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
```
## Remaining issue
The problem with the !6066 implementation is that the following code:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies #-}
module KnownNat2 where
import GHC.TypeLits
class KnownNat2 (name :: Symbol) (a :: Nat) (b :: Nat) where {}
instance (b <= a) => KnownNat2 "-" a b
```
that used to compile without errors, now gives the following error (this is with the GHC 9.4.1-rc1 release):
```
GHCi, version 9.4.0.20220721: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling KnownNat2 ( KnownNat2.hs, interpreted )
KnownNat2.hs:9:10: error:
* Variables `b, a' occur more often
in the constraint `b <= a'
than in the instance head `KnownNat2 "-" a b'
(Use UndecidableInstances to permit this)
* In the instance declaration for `KnownNat2 "-" a b'
|
9 | instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 "-" a b
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
```https://gitlab.haskell.org/ghc/ghc/-/issues/18407Type-Level floats2021-02-19T17:41:23ZLeanderKType-Level floats## Motivation
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583 motivates me to actually write a feature request. Currently, there are type-level *Nats*, but I would like to have actual type-level floats. I am currently writing a...## Motivation
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583 motivates me to actually write a feature request. Currently, there are type-level *Nats*, but I would like to have actual type-level floats. I am currently writing a linear-algebra library where I want to track certain things like the basis on the type-level and I would need to cross the type/term or term/type boundary (and the term-representation is via floats).
## Proposal
Some relevant discussion can be found on https://gitlab.haskell.org/ghc/ghc/-/issues/8697, where the focus is on rationals and not on floats, but I think both can go hand in hand. I think to implement such a feature one would need to figure out the parsing and adding floats to type-lits, but i am not a ghc-developer so I am not sure.
Ideally, I would imagine something like:
```
data Blah (num:: Float) = Blah
f :: forall num. KnownFloat num => Blah num -> Float
f = ...
g = f @1.3
```https://gitlab.haskell.org/ghc/ghc/-/issues/8422type nats solver is too weak!2019-07-07T18:45:08ZCarter Schonwaldtype nats solver is too weak!I just built ghc HEAD today, and the type nat solver can't handle the attached program, which \*should\* be simple to check! (and while I could use unsafeCoerce to "prove" it correct, that defeats the purpose of having the type nat solve...I just built ghc HEAD today, and the type nat solver can't handle the attached program, which \*should\* be simple to check! (and while I could use unsafeCoerce to "prove" it correct, that defeats the purpose of having the type nat solver!)
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Fancy where
import GHC.TypeLits
infixr 3 :*
data Shape (rank :: Nat) where
Nil :: Shape 0
(:*) :: {-# UNPACK #-} !(Int :: *) -> !(Shape r) -> Shape (1 + r)
reverseShape :: Shape r -> Shape r
reverseShape Nil = Nil
reverseShape shs = go shs Nil
where
go :: Shape a -> Shape b -> Shape (a+b)
go Nil res = res
go (ix :* more ) res = go more (ix :* res)
```8.0.1