GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:33:56Zhttps://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` 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
```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.1https://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 #-}
{-# 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":[]} -->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/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 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