GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:37Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11391TypeError is fragile2019-07-07T18:30:37ZBen GamariTypeError is fragileConsider this use of the new `TypeError` feature,
```hs
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type fami...Consider this use of the new `TypeError` feature,
```hs
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type family Resolve (t :: Type -> Type) :: Type -> Type where
Resolve _ = TypeError (Text "ERROR")
```
#### The okay case
Given something like,
```hs
testOK :: Resolve [] Int
testOK = []
```
we find that things work as expected,
```
• ERROR
• In the expression: [] :: Resolve [] Int
In an equation for ‘testOK’: testOK = [] :: Resolve [] Int
```
#### The bad case
However, it is very easy to fool GHC into not yielding the desired error message. For instance,
```hs
testNOTOK1 :: Resolve [] Int
testNOTOK1 = ()
```
gives us this a unification error,
```
• Couldn't match type ‘()’ with ‘(TypeError ...)’
Expected type: Resolve [] Int
Actual type: ()
```
This clearly isn't what we expected.
#### The tricky case
Another way we can fool the typechecker is to make it attempt instance resolution on our `TypeError`,
```hs
testNOTOK2 :: Resolve [] Int
testNOTOK2 = 1
```
Which results in,
```
• No instance for (Num (TypeError ...))
arising from the literal ‘1’
• In the expression: 1
In an equation for ‘testNOTOK2’: testNOTOK2 = 1
```8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/10348HEAD: `KnownNat` does not imply `Typeable` any more2019-07-07T18:36:27ZGabor GreifHEAD: `KnownNat` does not imply `Typeable` any moreAs Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:
```hs
{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKin...As Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:
```hs
{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}
import GHC.TypeLits
import Data.Typeable
data Foo (n :: Nat) where
Hey :: KnownNat n => Foo n
deriving instance Show (Foo n)
data T t where
T :: (Show t, Typeable t) => t -> T t
deriving instance Show (T n)
```
With ghci-7.11.20150407 I now see more constraints
```
*Main> :t T Hey
T Hey :: (Typeable n, KnownNat n) => T (Foo n)
```
OTOH ghci-7.11.20150215 only wanted `KnownNat`:
```
*Main> :t T Hey
T Hey :: KnownNat n => T (Foo n)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| 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":"HEAD: `KnownNat` does not imply `Typeable` any more","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:\r\n\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}\r\n\r\nimport GHC.TypeLits\r\nimport Data.Typeable\r\n\r\ndata Foo (n :: Nat) where\r\n Hey :: KnownNat n => Foo n\r\n\r\nderiving instance Show (Foo n)\r\n\r\ndata T t where\r\n T :: (Show t, Typeable t) => t -> T t\r\n\r\nderiving instance Show (T n)\r\n}}}\r\nWith ghci-7.11.20150407 I now see more constraints\r\n{{{\r\n*Main> :t T Hey\r\nT Hey :: (Typeable n, KnownNat n) => T (Foo n)\r\n}}}\r\n\r\nOTOH ghci-7.11.20150215 only wanted `KnownNat`:\r\n{{{\r\n*Main> :t T Hey\r\nT Hey :: KnownNat n => T (Foo n)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/9260Unnecessary error using GHC.TypeLits2019-07-07T18:41:09ZIcelandjackUnnecessary error using GHC.TypeLitsCompiling:
```
{-# LANGUAGE DataKinds, TypeOperators, GADTs #-}
module Error where
import GHC.TypeLits
data Fin n where
Fzero :: Fin (n + 1)
Fsucc :: Fin n -> Fin (n + 1)
test :: Fin 1
test = Fsucc Fzero
```
gives a strange (un...Compiling:
```
{-# LANGUAGE DataKinds, TypeOperators, GADTs #-}
module Error where
import GHC.TypeLits
data Fin n where
Fzero :: Fin (n + 1)
Fsucc :: Fin n -> Fin (n + 1)
test :: Fin 1
test = Fsucc Fzero
```
gives a strange (unnecessary) error message claiming that `Fin 1` doesn't match the expected type `Fin (0 + 1)`:
```
% ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.8.2
% ghc -ignore-dot-ghci /tmp/Error.hs
[1 of 1] Compiling Error ( /tmp/Error.hs, /tmp/Error.o )
/tmp/Error.hs:12:8:
Couldn't match type ‘0’ with ‘1’
Expected type: Fin 1
Actual type: Fin (0 + 1)
In the expression: Fsucc Fzero
In an equation for ‘test’: test = Fsucc Fzero
/tmp/Error.hs:12:14:
Couldn't match type ‘1’ with ‘0’
Expected type: Fin 0
Actual type: Fin (0 + 1)
In the first argument of ‘Fsucc’, namely ‘Fzero’
In the expression: Fsucc Fzero
%
```8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/4385Type-level natural numbers2019-07-07T18:59:14ZIavor S. DiatchkiType-level natural numbersNatural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time ...Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, BlueSpec, Cryptol, Habit).
Existing features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!
Indeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).
Supporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:
- a standard implementation,
- a better notation,
- better error messages,
- a more efficient implementation,
- more complete support for numeric operations.
I have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:
```
http://code.galois.com/darcs/ghc-type-naturals/
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | |
| Type | FeatureRequest |
| 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":"Type-level natural numbers","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"diatchki"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, BlueSpec, Cryptol, Habit).\r\n\r\nExisting features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!\r\n\r\nIndeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).\r\n\r\nSupporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:\r\n * a standard implementation,\r\n * a better notation,\r\n * better error messages,\r\n * a more efficient implementation,\r\n * more complete support for numeric operations.\r\n\r\nI have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:\r\n{{{\r\nhttp://code.galois.com/darcs/ghc-type-naturals/\r\n}}}\r\n\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Iavor S. DiatchkiIavor S. Diatchki