GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:00:22Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/16362Deriving a class via an instance that has a TypeError constraint using standa...2019-07-07T18:00:22Zj9794Deriving a class via an instance that has a TypeError constraint using standalone deriving fails during compilation.This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving.
This is the shortest example I was a...This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving.
This is the shortest example I was able to come up with:
```
{-# Language DataKinds, UndecidableInstances, StandaloneDeriving, DerivingVia #-}
import GHC.TypeLits
newtype NotNum a = NotNum a
instance (TypeError (Text "Not a num")) => Num (NotNum a) where
data Foo = Foo
deriving via (NotNum Foo) instance Num Foo
```
In this case, it'll fail in compilation with 'Not a Num'.
This only seems to happen when combining deriving via with standalone deriving, because if I derive the class like:
```
data Foo = Foo deriving Num via (NotNum Foo)
```
It works as expected (doesn't fail with my custom error until I actually try to use a Foo where I should use a Num)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Deriving a class via an instance that has a TypeError constraint using standalone deriving fails during compilation.","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving.\r\nThis is the shortest example I was able to come up with:\r\n\r\n{{{\r\n{-# Language DataKinds, UndecidableInstances, StandaloneDeriving, DerivingVia #-} \r\n\r\nimport GHC.TypeLits\r\n\r\nnewtype NotNum a = NotNum a\r\n\r\ninstance (TypeError (Text \"Not a num\")) => Num (NotNum a) where\r\n\r\ndata Foo = Foo\r\nderiving via (NotNum Foo) instance Num Foo\r\n}}}\r\n\r\nIn this case, it'll fail in compilation with 'Not a Num'.\r\n\r\nThis only seems to happen when combining deriving via with standalone deriving, because if I derive the class like:\r\n\r\n{{{\r\ndata Foo = Foo deriving Num via (NotNum Foo)\r\n}}}\r\n\r\nIt works as expected (doesn't fail with my custom error until I actually try to use a Foo where I should use a Num)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15232TypeError is reported as "redundant constraint" starting with GHC 8.22019-07-07T18:13:41ZfsoikinTypeError is reported as "redundant constraint" starting with GHC 8.2The following program compiles fine on GHC 8.0.2, but GHC 8.2.2 issues a warning, complaining that `TypeError` is a redundant constraint. This makes it very inconvenient to use `TypeError` with type classes.
```hs
{-# OPTIONS_GHC -Wredu...The following program compiles fine on GHC 8.0.2, but GHC 8.2.2 issues a warning, complaining that `TypeError` is a redundant constraint. This makes it very inconvenient to use `TypeError` with type classes.
```hs
{-# OPTIONS_GHC -Wredundant-constraints -Wall -Werror #-}
import GHC.TypeLits (TypeError, ErrorMessage(..))
class C a where f :: a -> a
instance {-# OVERLAPPING #-} C Int where f _ = 42
instance {-# OVERLAPPABLE #-} TypeError ( 'Text "Only Int is supported" ) => C a where f = undefined
main :: IO ()
main = print $ f (42::Int)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| 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":"TypeError is reported as \"redundant constraint\" starting with GHC 8.2","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["CustomTypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program compiles fine on GHC 8.0.2, but GHC 8.2.2 issues a warning, complaining that `TypeError` is a redundant constraint. This makes it very inconvenient to use `TypeError` with type classes.\r\n\r\n{{{#!hs\r\n{-# OPTIONS_GHC -Wredundant-constraints -Wall -Werror #-}\r\nimport GHC.TypeLits (TypeError, ErrorMessage(..))\r\n\r\nclass C a where f :: a -> a\r\ninstance {-# OVERLAPPING #-} C Int where f _ = 42\r\ninstance {-# OVERLAPPABLE #-} TypeError ( 'Text \"Only Int is supported\" ) => C a where f = undefined\r\n\r\nmain :: IO ()\r\nmain = print $ f (42::Int)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15052DeriveAnyClass instances may skip TypeError constraints2019-07-07T18:14:32ZDaniel GorínDeriveAnyClass instances may skip TypeError constraintsIn the presence of `TypeError`, one can derive instances with `DeriveAnyClass` that would be rejected otherwise. A simplistic example would be:
```haskell
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DataKinds #-}
{-# L...In the presence of `TypeError`, one can derive instances with `DeriveAnyClass` that would be rejected otherwise. A simplistic example would be:
```haskell
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T
where
import GHC.TypeLits(TypeError, ErrorMessage(..))
class TypeError ('Text "BOOM") => C a where
f :: a -> ()
f _ = ()
data T = T
deriving(C)
```
Of course, any attempt to use the instance leads to a type-error. However, the instance is rejected right away using a normal instance declaration or StandaloneDeriving.
While this is a toy example, it can actually happen when using `Generics` and default-signatures, where one would puts a `TypeError` in an instance head for one of the `Generics` constructors to give a better error message.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| 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":"DeriveAnyClass instances may skip TypeError constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the presence of `TypeError`, one can derive instances with `DeriveAnyClass` that would be rejected otherwise. A simplistic example would be:\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE DeriveAnyClass #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# LANGUAGE UndecidableSuperClasses #-}\r\nmodule T\r\n\r\nwhere\r\n\r\nimport GHC.TypeLits(TypeError, ErrorMessage(..))\r\n\r\n\r\nclass TypeError ('Text \"BOOM\") => C a where\r\n f :: a -> ()\r\n f _ = ()\r\n\r\n\r\ndata T = T\r\n deriving(C)\r\n\r\n}}}\r\n\r\nOf course, any attempt to use the instance leads to a type-error. However, the instance is rejected right away using a normal instance declaration or StandaloneDeriving.\r\n\r\nWhile this is a toy example, it can actually happen when using `Generics` and default-signatures, where one would puts a `TypeError` in an instance head for one of the `Generics` constructors to give a better error message.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/12237Constraint resolution vs. type family resolution vs. TypeErrors2019-07-07T18:27:01ZGergő ÉrdiConstraint resolution vs. type family resolution vs. TypeErrorsVia http://stackoverflow.com/q/37769351/477476, given the following setup:
```hs
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}
import Data.Proxy
i...Via http://stackoverflow.com/q/37769351/477476, given the following setup:
```hs
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}
import Data.Proxy
import GHC.TypeLits
type family TEq a b where
TEq a a = a
TEq a b = TypeError (Text "TEq error")
type family F a where
F () = ()
F (a, b) = TEq (F a) (F b)
F a = TypeError (Text "Unsupported type: " :<>: ShowType a)
```
and the following usages of `F` and `TEq`:
```hs
class (repr ~ F a) => C repr a
foo :: (C (F a) a) => proxy a -> ()
foo _ = ()
main :: IO ()
main = print $ foo (Proxy :: Proxy (Int, ()))
```
This results in
```
* No instance for (C (TEq (TypeError ...) ()) (Int, ()))
arising from a use of `foo'
* In the second argument of `($)', namely
`foo (Proxy :: Proxy (Int, ()))'
In the expression: print $ foo (Proxy :: Proxy (Int, ()))
In an equation for `main':
main = print $ foo (Proxy :: Proxy (Int, ()))
```
but it would be preferable to bail out earlier when `F Int` is resolved to `TypeError ...` instead of propagating that all the way to the `C` constraint.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Constraint resolution vs. type family resolution vs. TypeErrors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["CustomTypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Via http://stackoverflow.com/q/37769351/477476, given the following setup:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}\r\n{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}\r\n\r\nimport Data.Proxy\r\nimport GHC.TypeLits\r\n\r\ntype family TEq a b where\r\n TEq a a = a\r\n TEq a b = TypeError (Text \"TEq error\")\r\n\r\ntype family F a where\r\n F () = ()\r\n F (a, b) = TEq (F a) (F b)\r\n F a = TypeError (Text \"Unsupported type: \" :<>: ShowType a)\r\n}}}\r\n\r\nand the following usages of `F` and `TEq`:\r\n\r\n{{{#!hs\r\nclass (repr ~ F a) => C repr a\r\n\r\nfoo :: (C (F a) a) => proxy a -> ()\r\nfoo _ = ()\r\n\r\nmain :: IO ()\r\nmain = print $ foo (Proxy :: Proxy (Int, ()))\r\n}}}\r\n\r\nThis results in\r\n\r\n{{{\r\n * No instance for (C (TEq (TypeError ...) ()) (Int, ()))\r\n arising from a use of `foo'\r\n * In the second argument of `($)', namely\r\n `foo (Proxy :: Proxy (Int, ()))'\r\n In the expression: print $ foo (Proxy :: Proxy (Int, ()))\r\n In an equation for `main':\r\n main = print $ foo (Proxy :: Proxy (Int, ()))\r\n}}}\r\n\r\nbut it would be preferable to bail out earlier when `F Int` is resolved to `TypeError ...` instead of propagating that all the way to the `C` constraint.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12104Type families, `TypeError`, and `-fdefer-type-errors` cause "opt_univ fell in...2019-07-07T18:27:38ZantalszType families, `TypeError`, and `-fdefer-type-errors` cause "opt_univ fell into a hole"If I create a type family – open or closed – with a case that evaluates to a `TypeError`, and define a top-level binding with this type, loading the file with `-fdefer-type-errors` enabled (or via `:load!`/`:reload!`) panics GHC with "op...If I create a type family – open or closed – with a case that evaluates to a `TypeError`, and define a top-level binding with this type, loading the file with `-fdefer-type-errors` enabled (or via `:load!`/`:reload!`) panics GHC with "opt_univ fell into a hole". (And if I used `:load!` or `:reload!`, `-fdefer-type-errors` doesn't get unset.)
A minimal example:
```hs
{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
module T12104 where
import GHC.TypeLits
type family F a where
F a = TypeError (Text "error")
err :: F ()
err = ()
```
results in the panic
```
….hs:9:7: warning: [-Wdeferred-type-errors]
• error
• In the expression: ()
In an equation for ‘err’: err = ()
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.1 for x86_64-apple-darwin):
opt_univ fell into a hole {a4Va}
```
Adding more cases to the type family, or making it open, still cause the crash. This holds whether the error case is a final catch-all case, or something more like
```hs
type family F a where
F () = TypeError (Text "error")
F a = ()
```
Just using a type synonym for `F` doesn't cause a panic, however, and nor does giving `err` the type `TypeError (Text "error")` directly.8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/12049`OverloadedStrings` for types2019-07-07T18:27:51ZIcelandjack`OverloadedStrings` for typesIs there any sense in adding
```hs
class IsSymbol a where
type FromSymbol (str :: Symbol) :: a
instance IsSymbol ErrorMessage where
type FromSymbol str = GHC.TypeLits.Text str
instance IsSymbol ErrorMessage where
type FromSymbol...Is there any sense in adding
```hs
class IsSymbol a where
type FromSymbol (str :: Symbol) :: a
instance IsSymbol ErrorMessage where
type FromSymbol str = GHC.TypeLits.Text str
instance IsSymbol ErrorMessage where
type FromSymbol str = str
```
where `FromSymbol` gets placed before type-level string literals:
```hs
TypeError ("Warning: ":<>:ShowType ty:<>:" is odd.")
```
analogous to `Data.String.IsString`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"`OverloadedStrings` for types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["CustomTypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Is there any sense in adding\r\n\r\n{{{#!hs\r\nclass IsSymbol a where\r\n type FromSymbol (str :: Symbol) :: a\r\n\r\ninstance IsSymbol ErrorMessage where\r\n type FromSymbol str = GHC.TypeLits.Text str\r\n\r\ninstance IsSymbol ErrorMessage where\r\n type FromSymbol str = str\r\n}}}\r\n\r\nwhere `FromSymbol` gets placed before type-level string literals:\r\n\r\n{{{#!hs\r\nTypeError (\"Warning: \":<>:ShowType ty:<>:\" is odd.\")\r\n}}}\r\n\r\nanalogous to `Data.String.IsString`.","type_of_failure":"OtherFailure","blocking":[]} -->https://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/11099Incorrect warning about redundant constraints2019-07-07T18:32:07ZIavor S. DiatchkiIncorrect warning about redundant constraintsThe following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
...The following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
```
Redundant constraint: SomeFun i ~ [a]
In the type signature for:
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
```
I tried it on GHC version 7.11.20151029
<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":"Incorrect warning about redundant constraints","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":"The following program results in an incorrect warning about a redundant constraint:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family SomeFun a \r\n\r\nf :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\nf _ = read \"HELLO\"\r\n}}}\r\n\r\nThis is the warning:\r\n{{{\r\nRedundant constraint: SomeFun i ~ [a]\r\n In the type signature for:\r\n f :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\n}}}\r\n\r\nI tried it on GHC version 7.11.20151029\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16894TypeError hides a second error message2020-01-23T19:40:11ZJoey HessTypeError hides a second error message# Summary
Using TypeError seems to hide other type error messages due to eg, bad arguments passed to a function.
# Steps to reproduce
Load into ghci:
```
{-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies #-}
import...# Summary
Using TypeError seems to hide other type error messages due to eg, bad arguments passed to a function.
# Steps to reproduce
Load into ghci:
```
{-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies #-}
import GHC.TypeLits
type family Check x :: Bool where
Check 'True = 'True
Check x = 'False
foo :: Check 'False ~ 'True => Int -> String
foo n = "never reached"
type family Check2 x :: Bool where
Check2 'True = 'True
Check2 x = TypeError ('Text "no")
foo2 :: Check2 'False ~ 'True => Int -> String
foo2 n = "never reached"
```
```
ghci> foo "bar"
<interactive>:69:1: error:
• Couldn't match type ‘'False’ with ‘'True’
arising from a use of ‘foo’
• In the expression: foo "bar"
In an equation for ‘it’: it = foo "bar"
<interactive>:69:5: error:
• Couldn't match expected type ‘Int’ with actual type ‘[Char]’
• In the first argument of ‘foo’, namely ‘"bar"’
In the expression: foo "bar"
In an equation for ‘it’: it = foo "bar"
ghci> foo2 "bar"
<interactive>:70:1: error:
• no
• In the expression: foo2 "bar"
In an equation for ‘it’: it = foo2 "bar"
```
# Expected behavior
I expected to see the same error about Int vs [Char] for foo2 as is shown for foo, as well as the custom TypeError. However, the use of TypeError somehow prevents the Int vs [Char] error from being displayed.
This is preventing me from using TypeError in situations where there might be another, more basic
type error in the same code.
This may be related to https://gitlab.haskell.org/ghc/ghc/issues/14771
# Environment
* GHC version used: 8.4.4, 8.6.5https://gitlab.haskell.org/ghc/ghc/-/issues/17168Custom TypeError should include "arising from" clause2020-01-23T19:43:04ZAdam GundryCustom TypeError should include "arising from" clauseWhen a class constraint cannot be solved, the "No instance" message includes "arising from..." to specify the source of the constraint. However, if a custom type error is used to change the message, there is no "arising from..." clause. ...When a class constraint cannot be solved, the "No instance" message includes "arising from..." to specify the source of the constraint. However, if a custom type error is used to change the message, there is no "arising from..." clause. In complicated cases where the expression is large, this clause is useful in pinpointing the source of the error, so it would be helpful to include it.
For example, consider the following module:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module CustomTypeError where
import GHC.TypeLits
class C a where
(%) :: a -> a -> a
instance TypeError (Text "No, Int cannot be a C") => C Int
foo = 2 % 3 :: Int
bar = 'a' % 'b' :: Char
```
This results in the following output:
```hs
CustomTypeError.hs:13:7: error:
• No, Int cannot be a C
• In the expression: 2 % 3 :: Int
In an equation for ‘foo’: foo = 2 % 3 :: Int
|
13 | foo = 2 % 3 :: Int
| ^^^^^
CustomTypeError.hs:15:7: error:
• No instance for (C Char) arising from a use of ‘%’
• In the expression: 'a' % 'b' :: Char
In an equation for ‘bar’: bar = 'a' % 'b' :: Char
|
15 | bar = 'a' % 'b' :: Char
| ^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/18978Allow users to define an error message that is displayed when a constraint ca...2021-08-03T21:53:40Zsheafsam.derbyshire@gmail.comAllow users to define an error message that is displayed when a constraint can't be solvedI would like to enable users to annotate constraints with custom error messages; such a message would be displayed by GHC in the case that an annotated constraint could not be satisfied.
That is, I propose a special type family:
``...I would like to enable users to annotate constraints with custom error messages; such a message would be displayed by GHC in the case that an annotated constraint could not be satisfied.
That is, I propose a special type family:
```haskell
type Annotate :: ErrorMessage -> Constraint -> Constraint
```
Minimal illustration of the functionality:
```haskell
type F :: Type -> Constraint
type family F x where
F (a,b) = Annotate ( Text "F needs pair components to have the same type" ) ( a ~ b )
f :: F a => ()
f = ()
g :: ()
g = f @(Int, Bool)
```
would produce the error message:
```
* F needs pair components to have the same type
* Arising from a use of `f'
* In the expression: f @(Int, Bool)
In an equation for `g': g = f @(Int, Bool)
|
13 | g = f @(Int, Bool)
| ^^^^^^^^^^^^^^
````
instead of the decidably less helpful:
```
* Couldn't match type `Int' with `Bool' arising from a use of `f'
* In the expression: f @(Int, Bool)
In an equation for `g': g = f @(Int, Bool)
|
13 | g = f @(Int, Bool)
| ^^^^^^^^^^^^^^
```
I think this would be generally useful. For instance, one of my use cases is as follows: I have written a graphics shader library which uses type families to validate programs. When a user tries to read from an image or sample from a texture, we validate the operation using the image properties (available at the type level) as well as the arguments to the image operation that the user has provided (see [here](https://gitlab.com/sheaf/fir/-/blob/a6cb637f33b58653f6eb767c6964bab619472a73/src/FIR/Validation/Images.hs#L116)). This works well when the type family computation directly hits an error message, but can result in confusing messages when the type family application computes to another constraint. For instance, I have a constraint of the form
```haskell
type family TypeMatchesFormat (fmt :: ImageFormat) (a :: Type) :: Constraint where
MatchesFormat IntegralFormat a = Integral a
MatchesFormat FloatingFormat a = Floating a
MatchesFormat UnknownFormat _ = TypeError (Text "Unknown image format")
```
This leads to error messages of the form `Could not deduce Floating Word32` that are rather inscrutable, whereas with `Annotate` I could write:
```haskell
type family TypeMatchesFormat (fmt :: ImageFormat) (a :: Type) :: Constraint where
MatchesFormat IntegralFormat a = Annotate ( Text "Cannot use non-integral type " :<>: ShowType a :<>: Text " with an integral image format" ) ( Integral a )
MatchesFormat FloatingFormat a = Annotate ( Text "Cannot use non-float type " :<>: ShowType a :<>: Text " with a floating-point image format" ) ( Floating a )
MatchesFormat UnknownFormat _ = TypeError (Text "Unknown image format")
```https://gitlab.haskell.org/ghc/ghc/-/issues/11581TypeError requires UndecidableInstances unnecessarily2021-08-03T22:02:50ZrwbartonTypeError requires UndecidableInstances unnecessarilyThe example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
...The example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
```
requires `UndecidableInstances`:
```
BS.hs:11:5: error:
• The type family application ‘(TypeError ...)’
is no smaller than the instance head
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘ByteSize’
In the type family declaration for ‘ByteSize’
```
Obviously there's no real danger of undecidability here.
I tried changing the declaration of `TypeError` to
```hs
type family TypeError :: ErrorMessage -> b where
```
but it didn't help. Same error. Is that a bug?https://gitlab.haskell.org/ghc/ghc/-/issues/12048Allow CustomTypeErrors in type synonyms (+ evaluate nested type family?)2021-08-14T20:16:35ZIcelandjackAllow CustomTypeErrors in type synonyms (+ evaluate nested type family?)I didn't find a ticket with this, but with wiki:Proposal/CustomTypeErrors you can't define a type synonym without it erroring:
```hs
-- error: …
-- • onetwothree
-- • In the type synonym declaration for ‘ERROR’
-- Compilation fa...I didn't find a ticket with this, but with wiki:Proposal/CustomTypeErrors you can't define a type synonym without it erroring:
```hs
-- error: …
-- • onetwothree
-- • In the type synonym declaration for ‘ERROR’
-- Compilation failed.
type ERROR = TypeError (Text "onetwothree")
```
but I often want to factor out error messages, they are clunky to write at the type level and I often want to reuse message in many different type families, especially when they can be determined by a type family. Here's a hypothetical example:
```hs
type family
Whoami (ty :: Type) :: Symbol where
Whoami Int = "a number"
Whoami Float = "a number"
Whoami [_] = "a list of things"
Whoami _ = "something else"
```
I would like to write
```hs
type Error ty =
TypeError (Text "Expected a <...> but got ":<>: Text (Whoami ty))
```
----
Even when ‘inlined’, it displays `Expected a GRUE but got 'Text (Whoami Int)` and not `• Expected a GRUE but got a number.`:
```hs
a :: TypeError (Text "Expected a GRUE but got ":<>: Text (Whoami Int))
a = 'a'
```Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/11503TypeError woes (incl. pattern match checker)2021-08-15T13:19:00ZRichard Eisenbergrae@richarde.devTypeError woes (incl. pattern match checker)When I say
```
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,
UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Bug where
import GHC.TypeLits
import GHC.Exts ( Constraint )
type...When I say
```
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,
UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Bug where
import GHC.TypeLits
import GHC.Exts ( Constraint )
type family NotInt a where
NotInt Int = TypeError (Text "That's Int, silly.")
NotInt _ = (() :: Constraint)
data T a where
MkT1 :: a -> T a
MkT2 :: NotInt a => T a
foo :: T Int -> Int
foo (MkT1 x) = x
```
I get
```
Bug.hs:19:1: warning:
Pattern match(es) are non-exhaustive
In an equation for ‘foo’: Patterns not matched: MkT2
```
But I shouldn't.
Even worse, perhaps, GHC accepts my pattern-match against `MkT2` if I add it. If I change the `TypeError` to `False ~ True`, I get the correct behavior.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.1 |
| 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":"TypeError woes (incl. pattern match checker)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,\r\n UndecidableInstances #-}\r\n{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}\r\n\r\nmodule Bug where\r\n\r\nimport GHC.TypeLits\r\nimport GHC.Exts ( Constraint )\r\n\r\ntype family NotInt a where\r\n NotInt Int = TypeError (Text \"That's Int, silly.\")\r\n NotInt _ = (() :: Constraint)\r\n\r\ndata T a where\r\n MkT1 :: a -> T a\r\n MkT2 :: NotInt a => T a\r\n\r\nfoo :: T Int -> Int\r\nfoo (MkT1 x) = x\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:19:1: warning:\r\n Pattern match(es) are non-exhaustive\r\n In an equation for ‘foo’: Patterns not matched: MkT2\r\n}}}\r\n\r\nBut I shouldn't.\r\n\r\nEven worse, perhaps, GHC accepts my pattern-match against `MkT2` if I add it. If I change the `TypeError` to `False ~ True`, I get the correct behavior.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14141Custom type errors don't trigger when matching on a GADT constructor with an ...2021-08-15T13:19:00ZDarwin226Custom type errors don't trigger when matching on a GADT constructor with an error in the constraintThe following code fails to compile (as it should)
```hs
data D where
A :: C => D
type family C :: Constraint where
C = 'True ~ 'False
f :: D -> ()
f A = ()
```
with the error "Couldn't match type 'True with 'False".
This co...The following code fails to compile (as it should)
```hs
data D where
A :: C => D
type family C :: Constraint where
C = 'True ~ 'False
f :: D -> ()
f A = ()
```
with the error "Couldn't match type 'True with 'False".
This code, however, does compile without an issue:
```hs
data D where
A :: C => D
type family C :: Constraint where
C = TypeError ('Text "error")
f :: D -> ()
f A = ()
```
I feel that this is a bug.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Windows |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Custom type errors don't trigger when matching on a GADT constructor with an error in the constraint","status":"New","operating_system":"Windows","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code fails to compile (as it should)\r\n\r\n{{{#!hs\r\ndata D where\r\n A :: C => D\r\n\r\ntype family C :: Constraint where\r\n C = 'True ~ 'False\r\n\r\nf :: D -> ()\r\nf A = ()\r\n}}}\r\n\r\nwith the error \"Couldn't match type 'True with 'False\".\r\n\r\nThis code, however, does compile without an issue:\r\n\r\n{{{#!hs\r\ndata D where\r\n A :: C => D\r\n\r\ntype family C :: Constraint where\r\n C = TypeError ('Text \"error\")\r\n\r\nf :: D -> ()\r\nf A = ()\r\n}}}\r\n\r\nI feel that this is a bug.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16377`TypeError` in a pattern should flag inaccessible code2021-08-15T13:19:00ZIavor S. Diatchki`TypeError` in a pattern should flag inaccessible codeWhen we pattern match, if the context ends up having a custom `TypeError`, we should probably report it, as we've essentially found some inaccessible code. At present this doesn't happen and the custom error is only triggered if the func...When we pattern match, if the context ends up having a custom `TypeError`, we should probably report it, as we've essentially found some inaccessible code. At present this doesn't happen and the custom error is only triggered if the function is applied to an invalid argument. Here is an example to illustrate the issue:
```
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
module Test where
import GHC.TypeLits
import Data.Kind(Constraint)
type family F a :: Constraint
type instance F Int = ()
type instance F Char = TypeError ('Text "Nope")
type instance F Bool = (Int ~ Char)
data T where
A :: F Int => T
B :: F Char => T
C :: F Bool => T
exhaustive :: T -> ()
exhaustive A = ()
exhaustive B = () -- this is not flagged as inaccessible, but it should
-- exhaustive C = () -- this is flagged as inaccessible, as expected
```
If the match with constructor `C` is added to the program, GHC detects that this equation is inaccessible because `Int` will never match `Char`. I think that we'd like the same to happen in the second equation when we match on `B`, except we should report the custom type error, instead of GHC's message about unreachable code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.3 |
| 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":"`TypeError` in a pattern should flag inaccessible code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When we pattern match, if the context ends up having a custom `TypeError`, we should probably report it, as we've essentially found some inaccessible code. At present this doesn't happen and the custom error is only triggered if the function is applied to an invalid argument. Here is an example to illustrate the issue:\r\n\r\n{{{\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n\r\nmodule Test where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Kind(Constraint)\r\n\r\ntype family F a :: Constraint\r\ntype instance F Int = ()\r\ntype instance F Char = TypeError ('Text \"Nope\")\r\ntype instance F Bool = (Int ~ Char)\r\n\r\ndata T where\r\n A :: F Int => T\r\n B :: F Char => T\r\n C :: F Bool => T\r\n\r\nexhaustive :: T -> ()\r\nexhaustive A = ()\r\nexhaustive B = () -- this is not flagged as inaccessible, but it should\r\n-- exhaustive C = () -- this is flagged as inaccessible, as expected\r\n}}}\r\n\r\n\r\nIf the match with constructor `C` is added to the program, GHC detects that this equation is inaccessible because `Int` will never match `Char`. I think that we'd like the same to happen in the second equation when we match on `B`, except we should report the custom type error, instead of GHC's message about unreachable code.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/18766TypeError and GADT pattern matching exhaustiveness2021-08-16T14:04:29ZZiyang Liuunsafefixio@gmail.comTypeError and GADT pattern matching exhaustiveness```haskell
data D a where
C1 :: D Int
C2 :: D Char
type family Elem x list where
Elem x '[] = 'False
Elem x (x ': as) = 'True
Elem x (y ': as) = Elem x as
foo :: Elem a '[Int] ~ 'True => D a -> ()
foo C1 = ()
```
Here...```haskell
data D a where
C1 :: D Int
C2 :: D Char
type family Elem x list where
Elem x '[] = 'False
Elem x (x ': as) = 'True
Elem x (y ': as) = Elem x as
foo :: Elem a '[Int] ~ 'True => D a -> ()
foo C1 = ()
```
Here GHC correctly determines that the pattern matching is exhaustive.
But if the first case of the type family is changed to
```haskell
Elem x '[] = TypeError ('Text "oops")
```
then GHC no longer thinks it's exhaustive.
This seems to be the case with any empty type family, not just `TypeError`.
This makes it hard if not impossible to customize type error messages.
## Environment
* GHC version used: 8.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/20180Pattern match checker should treat TypeError as unsatisfiable2021-08-17T11:51:29ZSimon Peyton JonesPattern match checker should treat TypeError as unsatisfiableConsider this code from !6066
```
type (<=?) :: Int -> Int -> Bool
type (<=) x y = Assert (x <=? y) (TypeError blah-blah)
type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
Assert 'True _errMsg = (...Consider this code from !6066
```
type (<=?) :: Int -> Int -> Bool
type (<=) x y = Assert (x <=? y) (TypeError blah-blah)
type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
Assert 'True _errMsg = ()
Assert _check errMsg = errMsg
```
and this use:
```
data List n t where
Nil :: List 0 t
(:-) :: t -> List n t -> List (n+1) t
head' :: (1 <= n) => List n t -> t
head' (x :- _) = x -- No need for a Nil case!
```
The pattern match checker will want to check that the Nil case is unreachable.
In the Nil case, the `(1 <= n)` constraint becomes `1 <= 0`, which simplifies
(via `Assert`) to `TypeError blah-blah`.
**And that `TypeError @Constraint blahblah` should be treated as unsatisfiable by the pattern match checker!**
NB: there is [some discussion here](https://gitlab.haskell.org/ghc/ghc/-/issues/18310#note_295410)
about having an explicit `Unsatisfiable` constraint, a more
principled cousin of `TypeError`.
Actually this all came up in #11503, five years ago. Let's nail it!Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/-/issues/20181TypeError should be ok in a synonym2021-08-17T11:51:29ZSimon Peyton JonesTypeError should be ok in a synonymIf you write
```
type Foo = TypeError (Text "foo")
```
you get the perplexing message
```
Foo.hs:21:1: error:
• foo
• In the type synonym declaration for ‘Foo’
|
21 | type Foo a = TypeError (Text "foo")
| ^^^^^^^^^^^^^^^^^^...If you write
```
type Foo = TypeError (Text "foo")
```
you get the perplexing message
```
Foo.hs:21:1: error:
• foo
• In the type synonym declaration for ‘Foo’
|
21 | type Foo a = TypeError (Text "foo")
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But there is nothing wrong here! We just wanted to abbreviate the `TypeError` call -- this becomes jolly useful when the message is long.
The error comes from the call to `checkUserTypeError` in `checkValidType`, which is applied to the RHS of type synonyms.
My conclusion: don't call `checkUserTypeError` on the RHS of type synonyms
------------------------------------
See #18310, #20180, #12048, !6066https://gitlab.haskell.org/ghc/ghc/-/issues/20241TypeError reporting is too aggressive2021-08-18T22:29:09ZSimon Peyton JonesTypeError reporting is too aggressiveSummary: we are reporting `TypeError` calls too aggressively. This is blocking !6066. An easy fix is available.
Consider this, [derived from an ongoing MR](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066/diffs#note_371704).
`...Summary: we are reporting `TypeError` calls too aggressively. This is blocking !6066. An easy fix is available.
Consider this, [derived from an ongoing MR](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066/diffs#note_371704).
```
type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
Assert 'True _ = ()
Assert _ errMsg = errMsg
foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
foo_sym Proxy = ()
```
We get
```
T6066.hs:14:12: error:
• Boom
• In the type signature:
foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
|
14 | foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But this is silly: the `Assert` call is going to discard that `TypeError`. And not only is it silly, it actually prevents some useful applications of `TypeError`. Here is a less contrived signature:
```
foo_sym :: forall a. (Assert (IsInt a) ErrSyn) => Proxy a -> ()
```
We want to blow up on *calls* of `foo_sym` where `IsInt a` turns out to be False.
You can hide the `TypeError` inside a nullary type family like this:
```
type family HiddenTypeError where
HiddenTypeError = TypeError (Text "Boom")
foo_sym :: Assert 'True HiddenTypeError => Proxy a -> ()
```
but that is obviously grotesque.
## Proposed solution
When checking the validity of a user-written type signature (in `GHC.Tc.Validity.checkValidType`), we currently complain if `TypeError` occurs anywhere. Proposed solution:
* `checkValidType` complains of `TypeError`, *ignoring occurrences in the argument of a type family*
So it would not look at the arguments of `Assert` above.
Any views? This is closely related to #20180 and #20181.