GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-07-28T21:32:40Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20009Degradation in error message clarity for ` GHC.TypeNats.<=?`2022-07-28T21:32:40ZChristiaan 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...## 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 type-error 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/ghc-devs/2021-June/019992.html
## Environment
* GHC version used: 9.2.0.20210422https://gitlab.haskell.org/ghc/ghc/-/issues/18562`CmpSymbol` treats "\0" as bigger than expected2022-06-04T18:02:11ZTheMatten`CmpSymbol` treats "\0" as bigger than expected## Summary
Compared to behaviour of e.g. `Ord String` or `Ord ByteString`, `CmpSymbol` treats string `"\0"` as bigger than e.g. `"a"`, even though null character appears as first in ASCII ordering.
## Steps to reproduce
```
$ ghci
GHC...## Summary
Compared to behaviour of e.g. `Ord String` or `Ord ByteString`, `CmpSymbol` treats string `"\0"` as bigger than e.g. `"a"`, even though null character appears as first in ASCII ordering.
## Steps to reproduce
```
$ ghci
GHCi, version 8.10.1: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/matej/.ghci
λ> import GHC.TypeLits
λ> :set -XDataKinds
λ> :k! CmpSymbol "a" "\0"
CmpSymbol "a" "\0" :: Ordering
= 'LT
λ> compare "a" "\0"
GT
```
Same with `CmpSymbol "a" "\NUL"`.
## Expected behavior
I expected `CmpSymbol "a" "\0"` to return `'GT`, which is what is returned with characters immediately following
`\0` in ASCII.
## Environment
* GHC version used: 8.10.1
Optional:
* Operating System: `Arch Linux`
* System Architecture: `x64`https://gitlab.haskell.org/ghc/ghc/-/issues/21087KnownNat and friends are derivable2022-02-22T21:31:03ZJosh PriceKnownNat and friends are derivable## Summary
Using polymorphic data families, `DerivingVia`, and `StandaloneDeriving` it is possible to create new instances of `KnownNat`, `KnownSymbol`, and `KnownChar`. This breaks the safety of `sameNat`, `sameSybol`, and `sameChar`, ...## Summary
Using polymorphic data families, `DerivingVia`, and `StandaloneDeriving` it is possible to create new instances of `KnownNat`, `KnownSymbol`, and `KnownChar`. This breaks the safety of `sameNat`, `sameSybol`, and `sameChar`, as well as `eqTypeRep` and `testEquality`.
## Steps to reproduce
```
{-# language DataKinds #-}
{-# language DerivingVia #-}
{-# language TypeFamilies #-}
import GHC.TypeLits
data family Z :: k
deriving via 0 instance KnownNat Z
```
And essentially the same thing for `KnownSymbol` and `KnownChar`.
## Expected behavior
It seems `DerivingVia` allows deriving via not representationally equal types as long as the types of the methods involved end up being representationally equal. This can be useful, but the `KnownX` type classes should not be derivable this way as it breaks the assumption that `KnownX` instances correspond 1-to-1 with types.
## Environment
* GHC version used: 9.2.1 and HEADsheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/10321GHC.TypeLits.Nat types no longer fully simplified.2022-01-21T11:04:14ZdarchonGHC.TypeLits.Nat types no longer fully simplified.The following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a ...The following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n + 1) a
infixr 5 :>
```
when loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:
```
$ ghci example/vec.hs
GHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a
```
while in GHCi 7.10.1 it gives:
```
$ ghci example/vec.hs
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
That is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.
The same still happens in HEAD (20150417)
```
$ ghci example/vec.hs
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC.TypeLits.Nat types no longer fully simplified.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["TypeLits"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport GHC.TypeLits\r\n\r\ndata Vec :: Nat -> * -> * where\r\n Nil :: Vec 0 a\r\n (:>) :: a -> Vec n a -> Vec (n + 1) a\r\n\r\ninfixr 5 :>\r\n}}}\r\n\r\nwhen loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec 3 a\r\n}}}\r\n\r\nwhile in GHCi 7.10.1 it gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nThat is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.\r\n\r\nThe same still happens in HEAD (20150417)\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nI strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/9036ghc: panic! Binder's type (SingI Symbol <a String>) /= RHS type (String)2019-07-07T18:42:12ZNathan Collinsghc: panic! Binder's type (SingI Symbol <a String>) /= RHS type (String)Compilation error message:
```
ghc: panic! (the 'impossible' happened)
(GHC version 7.6.3 for i386-unknown-linux):
cgLookupPanic (probably invalid Core; try -dcore-lint)
cobox{v a212} [lid]
static binds for:
local binds f...Compilation error message:
```
ghc: panic! (the 'impossible' happened)
(GHC version 7.6.3 for i386-unknown-linux):
cgLookupPanic (probably invalid Core; try -dcore-lint)
cobox{v a212} [lid]
static binds for:
local binds for:
main:Debug.Trace.LogTree.Test.$p1AllShow{v r1pg} [gid[ClassOp]]
main:Debug.Trace.LogTree.Test.$p2AllShow{v r1ph} [gid[ClassOp]]
main:Debug.Trace.LogTree.Test.$p3AllShow{v r1pi} [gid[ClassOp]]
main:Debug.Trace.LogTree.Test.$p4AllShow{v r1pj} [gid[ClassOp]]
main:Debug.Trace.LogTree.Test.$p5AllShow{v r1pk} [gid[ClassOp]]
main:Debug.Trace.LogTree.Test.$p6AllShow{v r1pl} [gid[ClassOp]]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Error in -dcore-lint:
```
[10 of 10] Compiling Debug.Trace.LogTree.Test ( src/Debug/Trace/LogTree/Test.hs, tmp/Debug/Trace/LogTree/Test.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
{-# LINE 122 "src/Debug/Trace/LogTree/Test.hs #-}: Warning:
[RHS of $dSingI_a20r :: GHC.TypeLits.SingI GHC.TypeLits.Symbol "h"]
The type of this binder doesn't match the type of its RHS: $dSingI_a20r
Binder's type: GHC.TypeLits.SingI GHC.TypeLits.Symbol "h"
Rhs type: [GHC.Types.Char]
```
So, it looks like it's related to !TypeLits. The full -dcore-lint output is attached.
To reproduce:
1. git clone https://github.com/ntc2/haskell-call-trace.git
1. cd haskell-call-trace
1. git checkout break-ghc
1. \<install dependencies; see below\>
1. make
The dependencies from the .cabal file are:
```
build-depends: base >=4.6 && <4.7
, template-haskell >=2.8 && <2.9
, ghc-prim >=0.3 && <0.4
, parsec >=3.1 && <3.2
, tagged >=0.7 && <0.8
, transformers >=0.3 && <0.4
, mtl >=2.1 && <2.2
```
The problematic file is https://github.com/ntc2/haskell-call-trace/blob/break-ghc/src/Debug/Trace/LogTree/Test.hs . I was in the middle of a program-wide change when I ran into this GHC panic; I was using the type errors to guide my fixes. The Test.hs is not type correct, but I don't see how the stuff I changed as anything to do with my use of type-level strings (!TypeLits). The code in the previous commit compiles.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"ghc: panic! (the 'impossible' happened) (Binder's type (SingI Symbol <a String>) /= RHS type (String))","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":["GHC.TypeLits"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compilation error message:\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 7.6.3 for i386-unknown-linux):\r\n\tcgLookupPanic (probably invalid Core; try -dcore-lint)\r\n cobox{v a212} [lid]\r\n static binds for:\r\n local binds for:\r\n main:Debug.Trace.LogTree.Test.$p1AllShow{v r1pg} [gid[ClassOp]]\r\n main:Debug.Trace.LogTree.Test.$p2AllShow{v r1ph} [gid[ClassOp]]\r\n main:Debug.Trace.LogTree.Test.$p3AllShow{v r1pi} [gid[ClassOp]]\r\n main:Debug.Trace.LogTree.Test.$p4AllShow{v r1pj} [gid[ClassOp]]\r\n main:Debug.Trace.LogTree.Test.$p5AllShow{v r1pk} [gid[ClassOp]]\r\n main:Debug.Trace.LogTree.Test.$p6AllShow{v r1pl} [gid[ClassOp]]\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nError in -dcore-lint:\r\n{{{\r\n[10 of 10] Compiling Debug.Trace.LogTree.Test ( src/Debug/Trace/LogTree/Test.hs, tmp/Debug/Trace/LogTree/Test.o )\r\n*** Core Lint errors : in result of Desugar (after optimization) ***\r\n{-# LINE 122 \"src/Debug/Trace/LogTree/Test.hs #-}: Warning:\r\n [RHS of $dSingI_a20r :: GHC.TypeLits.SingI GHC.TypeLits.Symbol \"h\"]\r\n The type of this binder doesn't match the type of its RHS: $dSingI_a20r\r\n Binder's type: GHC.TypeLits.SingI GHC.TypeLits.Symbol \"h\"\r\n Rhs type: [GHC.Types.Char]\r\n}}}\r\n\r\nSo, it looks like it's related to !TypeLits. The full -dcore-lint output is attached.\r\n\r\nTo reproduce:\r\n1. git clone https://github.com/ntc2/haskell-call-trace.git\r\n2. cd haskell-call-trace\r\n3. git checkout break-ghc\r\n3. <install dependencies; see below>\r\n4. make\r\n\r\nThe dependencies from the .cabal file are:\r\n{{{\r\n build-depends: base >=4.6 && <4.7\r\n , template-haskell >=2.8 && <2.9\r\n , ghc-prim >=0.3 && <0.4\r\n , parsec >=3.1 && <3.2\r\n , tagged >=0.7 && <0.8\r\n , transformers >=0.3 && <0.4\r\n , mtl >=2.1 && <2.2\r\n}}}\r\n\r\nThe problematic file is https://github.com/ntc2/haskell-call-trace/blob/break-ghc/src/Debug/Trace/LogTree/Test.hs . I was in the middle of a program-wide change when I ran into this GHC panic; I was using the type errors to guide my fixes. The Test.hs is not type correct, but I don't see how the stuff I changed as anything to do with my use of type-level strings (!TypeLits). The code in the previous commit compiles.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10742GHC cannot deduce (irrelevant) reflexive type equality.2019-07-07T18:34:14ZNathan CollinsGHC cannot deduce (irrelevant) reflexive type equality.GHC is creating an irrelevant reflexive type equality and then failing to deduce it. The problem seems to be related to transitivity for `GHC.TypeLits.Nat`, as the example will make clear.
Example:
```hs
{-# LANGUAGE GADTs #-}
{-# LANG...GHC is creating an irrelevant reflexive type equality and then failing to deduce it. The problem seems to be related to transitivity for `GHC.TypeLits.Nat`, as the example will make clear.
Example:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
module TypeLitsBug where
import GHC.TypeLits
data T a where MkT :: T Int
test :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True)
=> proxy x y z -> ()
test _ = case MkT of MkT -> ()
```
Error message:
```
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.10.2
$ ghc -c TypeLitsBug.hs
TypeLitsBug.hs:11:9:
Could not deduce ((x <=? z) ~ (x <=? z))
from the context ((x <=? y) ~ 'True, (y <=? z) ~ 'True)
bound by the type signature for
test :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True) => proxy x y z -> ()
at TypeLitsBug.hs:(11,9)-(12,25)
NB: ‘<=?’ is a type function, and may not be injective
```
Notice the `x <=? z` relating `x` to `z`. I only mention `x <=? y` and `y <=? z` in the program, so it seems transitivity of `<=` is implicitly involved. Also, the problem goes away if I remove the GADT pattern match.
I asked Iavor about this and he suspected the ambiguity check.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Linux |
| Architecture | x86_64 (amd64) |
</details>
<!-- {"blocked_by":[],"summary":"GHC cannot deduce (irrelevant) reflexive type equality.","status":"New","operating_system":"Linux","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":["GADTs","TypeLits"],"differentials":[],"test_case":"","architecture":"x86_64 (amd64)","cc":[""],"type":"Bug","description":"GHC is creating an irrelevant reflexive type equality and then failing to deduce it. The problem seems to be related to transitivity for `GHC.TypeLits.Nat`, as the example will make clear.\r\n\r\nExample:\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule TypeLitsBug where\r\n\r\nimport GHC.TypeLits\r\n\r\ndata T a where MkT :: T Int\r\n\r\ntest :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True)\r\n => proxy x y z -> ()\r\ntest _ = case MkT of MkT -> ()\r\n}}}\r\n\r\nError message:\r\n{{{\r\n$ ghc --version\r\nThe Glorious Glasgow Haskell Compilation System, version 7.10.2\r\n\r\n$ ghc -c TypeLitsBug.hs \r\n\r\nTypeLitsBug.hs:11:9:\r\n Could not deduce ((x <=? z) ~ (x <=? z))\r\n from the context ((x <=? y) ~ 'True, (y <=? z) ~ 'True)\r\n bound by the type signature for\r\n test :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True) => proxy x y z -> ()\r\n at TypeLitsBug.hs:(11,9)-(12,25)\r\n NB: ‘<=?’ is a type function, and may not be injective\r\n}}}\r\n\r\nNotice the `x <=? z` relating `x` to `z`. I only mention `x <=? y` and `y <=? z` in the program, so it seems transitivity of `<=` is implicitly involved. Also, the problem goes away if I remove the GADT pattern match.\r\n\r\nI asked Iavor about this and he suspected the ambiguity check.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/10774Use `Natural` rather than `Integer` in `GHC.TypeLits`2019-07-07T18:33:56ZHerbert Valerio Riedelhvr@gnu.orgUse `Natural` rather than `Integer` in `GHC.TypeLits`When the numeric type-literals were implement via `GHC.TypeLits` there was no `Natural` type in `base` yet. But since GHC 7.10 we finally have `Natural` available in base!
Specifically, the following 3 type-signatures in `GHC.TypeLits` ...When the numeric type-literals were implement via `GHC.TypeLits` there was no `Natural` type in `base` yet. But since GHC 7.10 we finally have `Natural` available in base!
Specifically, the following 3 type-signatures in `GHC.TypeLits` contain `Integer`s that ought rather be `Natural`s:
```hs
someNatVal :: Integer -> Maybe SomeNat
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
natVal' :: forall n. KnownNat n => Proxy# n -> Integer
```8.0.1