GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210621T08:41:07Zhttps://gitlab.haskell.org/ghc/ghc//issues/20009Degradation in error message clarity for ` GHC.TypeNats.<=?`20210621T08:41:07ZChristiaan BaaijDegradation in error message clarity for ` GHC.TypeNats.<=?`## Summary
With the introduction of https://gitlab.haskell.org/ghc/ghc//commit/eea96042f1e8682605ae68db10f2bcdd7dab923e the clarity of error messages involving `GHC.TypeNats.<=?` has degraded compared to GHC 9.0.1 or earlier.
## Steps to reproduce
Given this code `TestInEq.hs`:
```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
```
## Expected behavior
On GHC 9.0.1 and prior, one would get the error message:
```
$ 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.
ghci>
```
But on GHC 9.2.0.20210422, which includes https://gitlab.haskell.org/ghc/ghc//commit/eea96042f1e8682605ae68db10f2bcdd7dab923e, one gets the following error message
```
$ 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>
```
which I feel is far less clear.
At the least, I hope we can recover the error message of GHC 9.0.1 or earlier. And it would be even nicer if this could be fixed before the GHC 9.2.1 release. I can envision at least three possible solutions:
1. Reinstate `(GHC.TypeNats.<=?) :: Nat > Nat > Bool` as a builtin type family
2. Somehow add a custom typeerror to `Data.Type.Ord.OrdCond`
3. Don't expand type aliases in type errors
Following up on 3, it would be even nicer if we could actually get an error along the lines of:
```
TestInEq.hs:11:14: error:
• Couldn't satisfy ‘a <= (a + 1)’
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
 ^^^^^^^^^
```
where the type synonym `(GHC.TypeNats.<=) :: Nat > Nat > Constraint` isn't expanded either.
This issue was/is also discussed at: https://mail.haskell.org/pipermail/ghcdevs/2021June/019992.html
## Environment
* GHC version used: 9.2.0.20210422## Summary
With the introduction of https://gitlab.haskell.org/ghc/ghc//commit/eea96042f1e8682605ae68db10f2bcdd7dab923e the clarity of error messages involving `GHC.TypeNats.<=?` has degraded compared to GHC 9.0.1 or earlier.
## Steps to reproduce
Given this code `TestInEq.hs`:
```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
```
## Expected behavior
On GHC 9.0.1 and prior, one would get the error message:
```
$ 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.
ghci>
```
But on GHC 9.2.0.20210422, which includes https://gitlab.haskell.org/ghc/ghc//commit/eea96042f1e8682605ae68db10f2bcdd7dab923e, one gets the following error message
```
$ 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>
```
which I feel is far less clear.
At the least, I hope we can recover the error message of GHC 9.0.1 or earlier. And it would be even nicer if this could be fixed before the GHC 9.2.1 release. I can envision at least three possible solutions:
1. Reinstate `(GHC.TypeNats.<=?) :: Nat > Nat > Bool` as a builtin type family
2. Somehow add a custom typeerror to `Data.Type.Ord.OrdCond`
3. Don't expand type aliases in type errors
Following up on 3, it would be even nicer if we could actually get an error along the lines of:
```
TestInEq.hs:11:14: error:
• Couldn't satisfy ‘a <= (a + 1)’
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
 ^^^^^^^^^
```
where the type synonym `(GHC.TypeNats.<=) :: Nat > Nat > Constraint` isn't expanded either.
This issue was/is also discussed at: https://mail.haskell.org/pipermail/ghcdevs/2021June/019992.html
## Environment
* GHC version used: 9.2.0.20210422https://gitlab.haskell.org/ghc/ghc//issues/18407TypeLevel floats20210219T17:41:23ZLeanderKTypeLevel floats## Motivation
https://gitlab.haskell.org/ghc/ghc//merge_requests/3583 motivates me to actually write a feature request. Currently, there are typelevel *Nats*, but I would like to have actual typelevel floats. I am currently writing a linearalgebra library where I want to track certain things like the basis on the typelevel and I would need to cross the type/term or term/type boundary (and the termrepresentation 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 typelits, but i am not a ghcdeveloper 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
```## Motivation
https://gitlab.haskell.org/ghc/ghc//merge_requests/3583 motivates me to actually write a feature request. Currently, there are typelevel *Nats*, but I would like to have actual typelevel floats. I am currently writing a linearalgebra library where I want to track certain things like the basis on the typelevel and I would need to cross the type/term or term/type boundary (and the termrepresentation 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 typelits, but i am not a ghcdeveloper 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!20190707T18: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 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)
```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